Characterizing Equivalential and Algebraizable Logics by the Leibniz Operator

In [14] we used the term finitely algebraizable for algebraizable logics in the sense of Blok and Pigozzi [2] and we introduced possibly infinitely algebraizable, for short, p.i.-algebraizable logics. In the present paper, we characterize the hierarchy of protoalgebraic, equivalential, finitely equivalential, p.i.-algebraizable, and finitely algebraizable logics by properties of the Leibniz operator. A Beth-style definability result yields that finitely equivalential and finitely algebraizable as well as equivalential and p.i.-algebraizable logics can be distinguished by injectivity of the Leibniz operator. Thus, from a characterization of equivalential logics we obtain a new short proof of the main result of [2] that a finitary logic is finitely algebraizable iff the Leibniz operator is injective and preserves unions of directed systems. It is generalized to nonfinitary logics. We characterize equivalential and, by adding injectivity, p.i.-algebraizable logics.     

Implicit connectives of algebraizable logics

An extensions by new axioms and rules of an algebraizable logic in the sense of Blok and Pigozzi is not necessarily algebraizable if it involves new connective symbols, or it may be algebraizable in an essentially different way than the original logic. However, extension whose axioms and rules define implicitly the new connectives are algebraizable, via the same equivalence formulas and defining equations of the original logic, by enriched algebras of its equivalente quasivariety semantics. For certain strongly algebraizable logics, all connectives defined implicitly by axiomatic extensions of the logic are explicitly definable.Special issue of Studia Logica: Algebraic Theory of Quasivarieties Presented by M. E. Adams, K. V. Adaricheva, W. Dziobiak, and A. V. Kravchenko     

Equivalential logics (I)

The class of equivalential logics comprises all implicative logics in the sense of Rasiowa [9], Suszko's logicSCI and many Others. Roughly speaking, a logic is equivalential iff the greatest strict congruences in its matrices (models) are determined by polynomials. The present paper is the first part of the survey in which systematic investigations into this class of logics are undertaken. Using results given in [3] and general theorems from the theory of quasi-varieties of models [5] we give a characterization of all simpleC-matrices for any equivalential logicC (Theorem I.14). In corollaries we give necessary and sufficient conditions for the class of all simple models for a given equivalential logic to be closed under free products (Theorem I.18). Theorem I.17 can be generalized as follows:For any equivalential logic C, clauses (i), (iii)and (v),formulated in Th.I.17,are equivalent.     

Basic properties of the equivalence

In this paper we investigate some basic semantic and syntactic conditions characterizing the equivalence connective. In particular we define three basic classes of algebras: the class of weak equivalential algebras, the class of equivalential algebras and the class of regular equivalential algebras (see [12]).Weak equivalential algebras can be used to study purely equivalential fragments of relevant logics and strict equivalential fragments of some modal logics (for investigations of strict implicational fragments of modal logics see [20]). Equivalential algebras are suitable to study purely equivalential fragment of BCI and BCK logic (see [21], p. 316). A subclass of the class of regular equivalential algebras is suitable to study equivalential fragments of ukasiewicz logics. Some subvarieties of the class of regular equivalential algebras provide natural semantics for equivalential fragments of the intuitionistic prepositional logic and various intermediate logics (see [13]).The last chapter is a selection of research problems which in the author's opinion are worth to be solved.     

Superintuitionistic Companions of Classical Modal Logics

This paper investigates partitions of lattices of modal logics based on superintuitionistic logics which are defined by forming, for each superintuitionistic logic L and classical modal logic , the set L[] of L-companions of . Here L[] consists of those modal logics whose non-modal fragments coincide with L and which axiomatize if the law of excluded middle p V p is added. Questions addressed are, for instance, whether there exist logics with the disjunction property in L[], whether L[] contains a smallest element, and whether L[] contains lower covers of . Positive solutions as concerns the last question show that there are (uncountably many) superclean modal logics based on intuitionistic logic in the sense of Vakarelov [28]. Thus a number of problems stated in [28] are solved. As a technical tool the paper develops the splitting technique for lattices of modal logics based on superintuitionistic logics and ap plies duality theory from [34].     

Leibniz Filters Revisited

Leibniz filters play a prominent role in the theory of protoalgebraic logics. In [3] the problem of the definability of Leibniz filters is considered. Here we study the definability of Leibniz filters with parameters. The main result of the paper says that a protoalgebraic logic S has its strong version weakly algebraizable iff it has its Leibniz filters explicitly definable with parameters.     

A Cut-Free Sequent System for the Smallest Interpretability Logic

The idea of interpretability logics arose in Visser [Vis90]. He introduced the logics as extensions of the provability logic GLwith a binary modality . The arithmetic realization of A B in a theory T will be that T plus the realization of B is interpretable in T plus the realization of A (T + A interprets T + B). More precisely, there exists a function f (the relative interpretation) on the formulas of the language of T such that T + B C implies T + A f(C).The interpretability logics were considered in several papers. An arithmetic completeness of the interpretability logic ILM, obtained by adding Montagna's axiom to the smallest interpretability logic IL, was proved in Berarducci [Ber90] and Shavrukov [Sha88] (see also Hájek and Montagna [HM90] and Hájek and Montagna [HM92]). [Vis90] proved that the interpretability logic ILP, an extension of IL, is also complete for another arithmetic interpretation. The completeness with respect to Kripke semantics due to Veltman was, for IL, ILMand ILP, proved in de Jongh and Veltman [JV90]. The fixed point theorem of GLcan be extended to ILand hence ILMand ILP(cf. de Jongh and Visser [JV91]). The unary pendant "T interprets T + A" is much less expressive and was studied in de Rijke [Rij92]. For an overview of interpretability logic, see Visser [Vis97], and Japaridze and de Jongh [JJ98].In this paper, we give a cut-free sequent system for IL. To begin with, we give a cut-free system for the sublogic IL4of IL, whose -free fragment is the modal logic K4. A cut-elimination theorem for ILis proved using the system for IK4and a property of Löb's axiom.     

On Definability of the Equality in Classes of Algebras with an Equivalence Relation

We present a finitary regularly algebraizable logic not finitely equivalential, for every similarity type. We associate to each of these logics a class of algebras with an equivalence relation, with the property that in this class, the identity is atomatically definable but not finitely atomatically definable. This revised version was published online in June 2006 with corrections to the Cover Date.     

On Gentzen Relations Associated with Finite-valued Logics Preserving Degrees of Truth

When considering m-sequents, it is always possible to obtain an m-sequent calculus VL for every m-valued logic (defined from an arbitrary finite algebra L of cardinality m) following for instance the works of the Vienna Group for Multiple-valued Logics. The Gentzen relations associated with the calculi VL are always finitely equivalential but might not be algebraizable. In this paper we associate an algebraizable 2-Gentzen relation with every sequent calculus VL in a uniform way, provided the original algebra L has a reduct that is a distributive lattice or a pseudocomplemented distributive lattice. We also show that the sentential logic naturally associated with the provable sequents of this algebraizable Gentzen relation is the logic that preserves degrees of truth with respect to the original algebra (in contrast with the more common logic that merely preserves truth). Finally, for some particular logics we obtain 2-sequent calculi that axiomatize the algebraizable Gentzen relations obtained so far.     

Interpolation and Amalgamation; Pushing the Limits. Part I

Continuing work initiated by Jónsson, Daigneault, Pigozzi and others; Maksimova proved that a normal modal logic (with a single unary modality) has the Craig interpolation property iff the corresponding class of algebras has the superamalgamation property (cf. [Mak 91], [Mak 79]). The aim of this paper is to extend the latter result to a large class of logics. We will prove that the characterization can be extended to all algebraizable logics containing Boolean fragment and having a certain kind of local deduction property. We also extend this characterization of the interpolation property to arbitrary logics under the condition that their algebraic counterparts are discriminator varieties. We also extend Maksimova's result to normal multi-modal logics with arbitrarily many, not necessarily unary modalities, and to not necessarily normal multi-modal logics with modalities of ranks smaller than 2, too.The problem of extending the above characterization result to no n-normal non-unary modal logics remains open.Related issues of universal algebra and of algebraic logic are discussed, too. In particular we investigate the possibility of extending the characterization of interpolability to arbitrary algebraizable logics.     

On Intermediate Predicate Logics of some Finite Kripke Frames,I. Levelwise Uniform Trees

An intermediate predicate logic L is called finite iff it is characterized by a finite partially ordered set M, i.e., iff L is the logic of the class of all predicate Kripke frames based on M. In this paper we study axiomatizability of logics of this kind. Namely, we consider logics characterized by finite trees M of a certain type (levelwise uniform trees) and establish the finite axiomatizability criterion for this case.     

The Classification of Propositional Calculi

We discuss Smirnovs problem of finding a common background for classifying implicational logics. We formulate and solve the problem of extending, in an appropriate way, an implicational fragment H of the intuitionistic propositional logic to an implicational fragment TV of the classical propositional logic. As a result we obtain logical constructions having the form of Boolean lattices whose elements are implicational logics. In this way, whole classes of new logics can be obtained. We also consider the transition from implicational logics to full logics. On the base of the lattices constructed, we formulate the main classification principles for propositional logics.     

Algebras and Matrices for Annotated Logics

We study the matrices, reduced matrices and algebras associated to the systems SA_T of structural annotated logics. In previous papers, these systems were proven algebraizable in the finitary case and the class of matrices analyzed here was proven to be a matrix semantics for them.We prove that the equivalent algebraic semantics associated with the systems SA_T are proper quasivarieties, we describe the reduced matrices, the subdirectly irreducible algebras and we give a general decomposition theorem. As a consequence we obtain a decision procedure for these logics.     

An Approach to Glivenko’s Theorem in Algebraizable Logics

In a classical paper [15] V. Glivenko showed that a proposition is classically demonstrable if and only if its double negation is intuitionistically demonstrable. This result has an algebraic formulation: the double negation is a homomorphism from each Heyting algebra onto the Boolean algebra of its regular elements. Versions of both the logical and algebraic formulations of Glivenko’s theorem, adapted to other systems of logics and to algebras not necessarily related to logic can be found in the literature (see [2, 9, 8, 14] and [13, 7, 14]). The aim of this paper is to offer a general frame for studying both logical and algebraic generalizations of Glivenko’s theorem. We give abstract formulations for quasivarieties of algebras and for equivalential and algebraizable deductive systems and both formulations are compared when the quasivariety and the deductive system are related. We also analyse Glivenko’s theorem for compatible expansions of both cases. Presented by Jacek Malinowski     

Categorical Abstract Algebraic Logic: Behavioral π-Institutions

Recently, Caleiro, Gon¸calves and Martins introduced the notion of behaviorally algebraizable logic. The main idea behind their work is to replace, in the traditional theory of algebraizability of Blok and Pigozzi, unsorted equational logic with multi-sorted behavioral logic. The new notion accommodates logics over many-sorted languages and with non-truth-functional connectives. Moreover, it treats logics that are not algebraizable in the traditional sense while, at the same time, shedding new light to the equivalent algebraic semantics of logics that are algebraizable according to the original theory. In this paper, the notion of an abstract multi-sorted π-institution is introduced so as to transfer elements of the theory of behavioral algebraizability to the categorical setting. Institutions formalize a wider variety of logics than deductive systems, including logics involving multiple signatures and quantifiers. The framework developed has the same relation to behavioral algebraizability as the classical categorical abstract algebraic logic framework has to the original theory of algebraizability of Blok and Pigozzi.     

The Beth Property in Algebraic Logic

The present paper is a study in abstract algebraic logic. We investigate the correspondence between the metalogical Beth property and the algebraic property of surjectivity of epimorphisms. It will be shown that this correspondence holds for the large class of equivalential logics. We apply our characterization theorem to relevance logics and many-valued logics. Dedicated to the memory of Willem Johannes Blok     

On Extensions of Intermediate Logics by Strong Negation

In this paper we will study the properties of the least extension n() of a given intermediate logic by a strong negation. It is shown that the mapping from to n() is a homomorphism of complete lattices, preserving and reflecting finite model property, frame-completeness, interpolation and decidability. A general characterization of those constructive logics is given which are of the form n (). This summarizes results that can be found already in [13,14] and [4]. Furthermore, we determine the structure of the lattice of extensions of n(LC).     

Duality for Lattice-Ordered Algebras and for Normal Algebraizable Logics

Part I of this paper is developed in the tradition of Stone-type dualities, where we present a new topological representation for general lattices (influenced by and abstracting over both Goldblatt's [17] and Urquhart's [46]), identifying them as the lattices of stable compact-opens of their dual Stone spaces (stability refering to a closure operator on subsets). The representation is functorial and is extended to a full duality.In part II, we consider lattice-ordered algebras (lattices with additional operators), extending the Jónsson and Tarski representation results [30] for Boolean algebras with Operators. Our work can be seen as developing, and indeed completing, Dunn's project of gaggle theory [13, 14]. We consider general lattices (rather than Boolean algebras), with a broad class of operators, which we dubb normal, and which includes the Jónsson-Tarski additive operators. Representation of l-algebras is extended to full duality.In part III we discuss applications in logic of the framework developed. Specifically, logics with restricted structural rules give rise to lattices with normal operators (in our sense), such as the Full Lambek algebras (F L-algebras) studied by Ono in [36]. Our Stone-type representation results can be then used to obtain canonical constructions of Kripke frames for such systems, and to prove a duality of algebraic and Kripke semantics for such logics.     

Infinitary Action Logic: Complexity, Models and Grammars

Action logic of Pratt [21] can be presented as Full Lambek Calculus FL [14, 17] enriched with Kleene star *; it is equivalent to the equational theory of residuated Kleene algebras (lattices). Some results on axiom systems, complexity and models of this logic were obtained in [4, 3, 18]. Here we prove a stronger form of *-elimination for the logic of *-continuous action lattices and the –completeness of the equational theories of action lattices of subsets of a finite monoid and action lattices of binary relations on a finite universe. We also discuss possible applications in linguistics. Presented by Jacek Malinowski