Leibniz filters and the strong version of a protoalgebraic logic

A filter of a sentential logic ? is Leibniz when it is the smallest one among all the ?-filters on the same algebra having the same Leibniz congruence. This paper studies these filters and the sentential logic ?⁺ defined by the class of all ?-matrices whose filter is Leibniz, which is called the strong version of ?, in the context of protoalgebraic logics with theorems. Topics studied include an enhanced Correspondence Theorem, characterizations of the weak algebraizability of ?⁺ and of the explicit definability of Leibniz filters, and several theorems of transfer of metalogical properties from ? to ?⁺. For finitely equivalential logics stronger results are obtained. Besides the general theory, the paper examines the examples of modal logics, quantum logics and Łukasiewicz's finitely-valued logics. One finds that in some cases the existence of a weak and a strong version of a logic corresponds to well-known situations in the literature, such as the local and the global consequences for normal modal logics; while in others these constructions give an independent interest to the study of other lesser-known logics, such as the lattice-based many-valued logics. Received: 30 October 1998 /?Published online: 15 June 2001     

On the complexity of the Leibniz hierarchy

We prove that the problem of determining whether a finite logical matrix determines an algebraizable logic is complete for EXPTIME. The same result holds for the classes of order algebraizable, weakly algebraizable, equivalential and protoalgebraic logics. Finally, the same problem for the class of truth-equational logic is shown to be hard for EXPTIME.     

Abstract Logics, Logic Maps, and Logic Homomorphisms

What is a logic? Which properties are preserved by maps between logics? What is the right notion for equivalence of logics? In order to give satisfactory answers we generalize and further develop the topological approach of [4] and present the foundations of a general theory of abstract logics which is based on the abstract concept of a theory. Each abstract logic determines a topology on the set of theories. We develop a theory of logic maps and show in what way they induce (continuous, open) functions on the corresponding topological spaces. We also establish connections to well-known notions such as translations of logics and the satisfaction axiom of institutions [5]. Logic homomorphisms are maps that behave in some sense like continuous functions and preserve more topological structure than logic maps in general. We introduce the notion of a logic isomorphism as a (not necessarily bijective) function on the sets of formulas that induces a homeomorphism between the respective topological spaces and gives rise to an equivalence relation on abstract logics. Therefore, we propose logic isomorphisms as an adequate and precise notion for equivalence of logics. Finally, we compare this concept with another recent proposal presented in [2]. This research was supported by the grant CNPq/FAPESB 350092/2006-0.     

Proof complexity of intuitionistic implicational formulas

We study implicational formulas in the context of proof complexity of intuitionistic propositional logic (IPC). On the one hand, we give an efficient transformation of tautologies to implicational tautologies that preserves the lengths of intuitionistic extended Frege (EF) or substitution Frege (SF) proofs up to a polynomial. On the other hand, EF proofs in the implicational fragment of IPC polynomially simulate full intuitionistic logic for implicational tautologies. The results also apply to other fragments of other superintuitionistic logics under certain conditions.In particular, the exponential lower bounds on the length of intuitionistic EF proofs by Hrube? (2007), generalized to exponential separation between EF and SF systems in superintuitionistic logics of unbounded branching by Je?ábek (2009), can be realized by implicational tautologies.     

The simplest protoalgebraic logic

The logic is the sentential logic defined in the language with just implication → by the axiom of reflexivity or identity “” and the rule of Modus Ponens “from φ and to infer ψ”. The theorems of this logic are exactly all formulas of the form . We argue that this is the simplest protoalgebraic logic, and that in it every set of assumptions encodes in itself not only all its consequences but also their proofs. In this paper we study this logic from the point of view of abstract algebraic logic, and in particular we use it as a relatively natural counterexample to settle some open problems in this theory. It appears that this logic has almost no properties: it is neither equivalential nor weakly algebraizable; it does not have an algebraic semantics; it does not satisfy any form of the Deduction Theorem, other than the most general parameterized and local one that all protoalgebraic logics satisfy; it is not filter‐distributive; and so on. It satisfies some forms of the interpolation property but in a rather trivial way. Very few things are known about its algebraic counterpart, save that its intrinsic variety is the class of all algebras of the similarity type.     

On the rules of intermediate logics

If the Visser rules are admissible for an intermediate logic, they form a basis for the admissible rules of the logic. How to characterize the admissible rules of intermediate logics for which not all of the Visser rules are admissible is not known. In this paper we give a brief overview of results on admissible rules in the context of intermediate logics. We apply these results to some well-known intermediate logics. We provide natural examples of logics for which the Visser rule are derivable, admissible but nonderivable, or not admissible. Supported by the Austrian Science Fund FWF under projects P16264 and P16539.     

Structuring the Universe of Universal Logic

How, why and what for we should combine logics is perfectly well explained in a number of works concerning this issue. But the interesting question seems to be the nature and the structure of the general universe of possible combinations of logical systems. Adopting the point of view of universal logic in the paper the categorical constructions are introduced which along with the coproducts underlying the fibring of logics describe the inner structure of the category of logical systems. It is shown that categorically the universe of universal logic turns out to be a topos and a paraconsistent complement topos. This work was supported by Russian Foundation for Humanities via the Project ”The structure of Universal Logics”, grant No 06-03-00195a.     

Inclusion and exclusion dependencies in team semantics — On some logics of imperfect information

We introduce some new logics of imperfect information by adding atomic formulas corresponding to inclusion and exclusion dependencies to the language of first order logic. The properties of these logics and their relationships with other logics of imperfect information are then studied. As a corollary of these results, we characterize the expressive power of independence logic, thus answering an open problem posed in Grädel and Väänänen, 2010 [9].     

A Universal Logic Approach to Adaptive Logics

In this paper, adaptive logics are studied from the viewpoint of universal logic (in the sense of the study of common structures of logics). The common structure of a large set of adaptive logics is described. It is shown that this structure determines the proof theory as well as the semantics of the adaptive logics, and moreover that most properties of the logics can be proved by relying solely on the structure, viz. without invoking any specific properties of the logics themselves.     

A modal logic framework for reasoning about comparative distances and topology

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s S4 for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances (i.e., between minimum and infimum). Due to its greater expressive power, this logic turns out to behave quite differently from both S4 and conditional logics. We provide finite (Hilbert-style) axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line (and various other important metric spaces) is not recursively enumerable. This result is proved by an encoding of Diophantine equations.     

All finitely axiomatizable subframe logics containing the provability logic CSM_{0} are decidable

In this paper we investigate those extensions of the bimodal provability logic (alias or which are subframe logics, i.e. whose general frames are closed under a certain type of substructures. Most bimodal provability logics are in this class. The main result states that all finitely axiomatizable subframe logics containing are decidable. We note that, as a rule, interesting systems in this class do not have the finite model property and are not even complete with respect to Kripke semantics. Received July 15, 1997     

Proof internalization in generalized Frege systems for classical logic

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.     

Modules over quantaloids: Applications to the isomorphism problem in algebraic logic and π-institutions

We solve the isomorphism problem in the context of abstract algebraic logic and of π-institutions, namely the problem of when the notions of syntactic and semantic equivalence among logics coincide. The problem is solved in the general setting of categories of modules over quantaloids. We introduce closure operators on modules over quantaloids and their associated morphisms. We show that, up to isomorphism, epis are morphisms associated with closure operators. The notions of (semi-)interpretability and (semi-)representability are introduced and studied. We introduce cyclic modules, and provide a characterization for cyclic projective modules as those having a g-variable. Finally, we explain how every π-institution induces a module over a quantaloid, and thus the theory of modules over quantaloids can be considered as an abstraction of the theory of π-institutions.     

Axiomatizations of team logics

In a modular approach, we lift Hilbert-style proof systems for propositional, modal and first-order logic to generalized systems for their respective team-based extensions. We obtain sound and complete axiomatizations for the dependence-free fragment FO(～) of Väänänen's first-order team logic TL, for propositional team logic PTL, quantified propositional team logic QPTL, modal team logic MTL, and for the corresponding logics of dependence, independence, inclusion and exclusion.As a crucial step in the completeness proof, we show that the above logics admit, in a particular sense, a semantics-preserving elimination of modalities and quantifiers from formulas.     

Evidence and plausibility in neighborhood structures

The intuitive notion of evidence has both semantic and syntactic features. In this paper, we develop an evidence logic for epistemic agents faced with possibly contradictory evidence from different sources. The logic is based on a neighborhood semantics, where a neighborhood N indicates that the agent has reason to believe that the true state of the world lies in N. Further notions of relative plausibility between worlds and beliefs based on the latter ordering are then defined in terms of this evidence structure, yielding our intended models for evidence-based beliefs. In addition, we also consider a second more general flavor, where belief and plausibility are modeled using additional primitive relations, and we prove a representation theorem showing that each such general model is a p-morphic image of an intended one. This semantics invites a number of natural special cases, depending on how uniform we make the evidence sets, and how coherent their total structure. We give a structural study of the resulting ‘uniform’ and ‘flat’ models. Our main result are sound and complete axiomatizations for the logics of all four major model classes with respect to the modal language of evidence, belief and safe belief. We conclude with an outlook toward logics for the dynamics of changing evidence, and the resulting language extensions and connections with logics of plausibility change.     

The equational theory of a nontrivial discriminator variety is co-NP-hard

Discriminator varieties play a central role in the classification of decidable varieties; and they arise naturally in the study of algebraic logics. There are also important connections with the reduction of theorem proving to equational logic. In this paper we show, for any nontrivial discriminator variety, that the problem of determining if an equation holds in the variety is co-NP-hard.Received August 24, 2002; accepted in final form August 5, 2004.     

Effectiveness in RPL, with applications to continuous logic

In this paper, we introduce a foundation for computable model theory of rational Pavelka logic (an extension of ?ukasiewicz logic) and continuous logic, and prove effective versions of some related theorems in model theory. We show how to reduce continuous logic to rational Pavelka logic. We also define notions of computability and decidability of a model for logics with computable, but uncountable, set of truth values; we show that provability degree of a formula with respect to a linear theory is computable, and use this to carry out an effective Henkin construction. Therefore, for any effectively given consistent linear theory in continuous logic, we effectively produce its decidable model. This is the best possible, since we show that the computable model theory of continuous logic is an extension of computable model theory of classical logic. We conclude with noting that the unique separable model of a separably categorical and computably axiomatizable theory (such as that of a probability space or an L^p Banach lattice) is decidable.     

Implicational (semilinear) logics I: a new hierarchy

In abstract algebraic logic, the general study of propositional non-classical logics has been traditionally based on the abstraction of the Lindenbaum-Tarski process. In this process one considers the Leibniz relation of indiscernible formulae. Such approach has resulted in a classification of logics partly based on generalizations of equivalence connectives: the Leibniz hierarchy. This paper performs an analogous abstract study of non-classical logics based on the kind of generalized implication connectives they possess. It yields a new classification of logics expanding Leibniz hierarchy: the hierarchy of implicational logics. In this framework the notion of implicational semilinear logic can be naturally introduced as a property of the implication, namely a logic L is an implicational semilinear logic iff it has an implication such that L is complete w.r.t. the matrices where the implication induces a linear order, a property which is typically satisfied by well-known systems of fuzzy logic. The hierarchy of implicational logics is then restricted to the semilinear case obtaining a classification of implicational semilinear logics that encompasses almost all the known examples of fuzzy logics and suggests new directions for research in the field.     

The bounded proof property via step algebras and step frames

The paper introduces semantic and algorithmic methods for establishing a variant of the analytic subformula property (called ‘the bounded proof property’, bpp) for modal propositional logics. The bpp is much weaker property than full cut-elimination, but it is nevertheless sufficient for establishing decidability results. Our methodology originated from tools and techniques developed on one side within the algebraic/coalgebraic literature dealing with free algebra constructions and on the other side from classical correspondence theory in modal logic. As such, our approach is orthogonal to recent literature based on proof-theoretic methods and, in a way, complements it.     

Modal characterisation theorems over special classes of frames

We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem’s theorem, which says that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes-for instance, rooted frames, finite rooted frames, finite transitive frames, well-founded transitive frames, finite equivalence frames-as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraïssé versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes. Over most of the classes considered, we obtain finite model theory analogues of the classically expected characterisations, with new proofs also for the classical setting. The class of transitive frames is a notable exception, with a marked difference between the classical and the finite model theory of bisimulation invariant first-order properties. Over the class of all finite transitive frames in particular, we find that monadic second-order logic is no more expressive than first-order as far as bisimulation invariant properties are concerned — though both are more expressive here than basic modal logic. We obtain ramifications of the de Jongh-Sambin theorem and a new and specific analogue of the Janin-Walukiewicz characterisation of bisimulation invariant monadic second-order for finite transitive frames.