Equivalential and algebraizable logics

The notion of an algebraizable logic in the sense of Blok and Pigozzi [3] is generalized to that of a possibly infinitely algebraizable, for short, p.i.-algebraizable logic by admitting infinite sets of equivalence formulas and defining equations. An example of the new class is given. Many ideas of this paper have been present in [3] and [4]. By a consequent matrix semantics approach the theory of algebraizable and p.i.-algebraizable logics is developed in a different way. It is related to the theory of equivalential logics in the sense of Prucnal and Wroski [18], and it is extended to nonfinitary logics. The main result states that a logic is algebraizable (p.i.-algebraizable) iff it is finitely equivalential (equivalential) and the truth predicate in the reduced matrix models is equationally definable.Most of the results of the present and a forthcoming paper originally appeared in [13].Presented by Wolfgang Rautenberg     

A new formulation of discussive logic

S. Jakowski introduced the discussive prepositional calculus D ₂as a basis for a logic which could be used as underlying logic of inconsistent but nontrivial theories (see, for example, N. C. A. da Costa and L. Dubikajtis, On Jakowski's discussive logic, in Non-Classical Logic, Model Theory and Computability, A. I. Arruda, N. C. A da Costa and R. Chuaqui edts., North-Holland, Amsterdam, 1977, 37–56). D ₂has afterwards been extended to a first-order predicate calculus and to a higher-order logic (cf. the quoted paper). In this paper we present a natural version of D ₂, in the sense of Jakowski and Gentzen; as a consequence, we suggest a new formulation of the discussive predicate calculus (with equality). A semantics for the new calculus is also presented.     

Many-Valued Points And Equality

In 1999, da Silva, D'Ottaviano and Sette proposed a general definition for the term translation between logics and presented an initial segment of its theory. Logics are characterized, in the most general sense, as sets with consequence relations and translations between logics as consequence-relation preserving maps. In a previous paper the authors introduced the concept of conservative translation between logics and studied some general properties of the co-complete category constituted by logics and conservative translations between them. In this paper we present some conservative translations involving classical logic, Lukasiewicz three-valued system L ₃, the intuitionistic system I ¹ and several paraconsistent logics, as for instance Sette's system P ¹, the D'Ottaviano and da Costa system J ₃ and da Costa's systems C _n, 1 n.     

Algebraic study of Sette's maximal paraconsistent logic

The aim of this paper is to study the paraconsistent deductive systemP ¹ within the context of Algebraic Logic. It is well known due to Lewin, Mikenberg and Schwarse thatP ¹ is algebraizable in the sense of Blok and Pigozzi, the quasivariety generated by Sette's three-element algebraS being the unique quasivariety semantics forP ¹. In the present paper we prove that the mentioned quasivariety is not a variety by showing that the variety generated byS is not equivalent to any algebraizable deductive system. We also show thatP ¹ has no algebraic semantics in the sense of Czelakowski. Among other results, we study the variety generated by the algebraS. This enables us to prove in a purely algebraic way that the only proper non-trivial axiomatic extension ofP ¹ is the classical deductive systemPC. Throughout the paper we also study those abstract logics which are in a way similar toP ¹, and are called hereabstract Sette logics. We obtain for them results similar to those obtained for distributive abstract logics by Font, Verdú and the author.     

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.     

Non-Adjunctive Inference and Classical Modalities

The article focuses on representing different forms of non-adjunctive inference as sub-Kripkean systems of classical modal logic, where the inference from □A and □B to □A∧B fails. In particular we prove a completeness result showing that the modal system that Schotch and Jennings derive from a form of non-adjunctive inference in (Schotch and Jennings, 1980) is a classical system strictly stronger than EMN and weaker than K (following the notation for classical modalities presented in Chellas, 1980). The unified semantical characterization in terms of neighborhoods permits comparisons between different forms of non-adjunctive inference. For example, we show that the non-adjunctive logic proposed in (Schotch and Jennings, 1980) is not adequate in general for representing the logic of high probability operators. An alternative interpretation of the forcing relation of Schotch and Jennings is derived from the proposed unified semantics and utilized in order to propose a more fine-grained measure of epistemic coherence than the one presented in (Schotch and Jennings, 1980). Finally we propose a syntactic translation of the purely implicative part of Jaśkowski's system D₂ into a classical system preserving all the theorems (and non-theorems) explicilty mentioned in (Jaśkowski, 1969). The translation method can be used in order to develop epistemic semantics for a larger class of non-adjunctive (discursive) logics than the ones historically investigated by Jaśkowski.     

Paraconsistent Logics and Translations

In 1999, da Silva, D'Ottaviano and Sette proposed a general definition for the term translation between logics and presented an initial segment of its theory. Logics are characterized, in the most general sense, as sets with consequence relations and translations between logics as consequence-relation preserving maps. In a previous paper the authors introduced the concept of conservative translation between logics and studied some general properties of the co-complete category constituted by logics and conservative translations between them. In this paper we present some conservative translations involving classical logic, Lukasiewicz three-valued system L ₃, the intuitionistic system I ¹ and several paraconsistent logics, as for instance Sette's system P ¹, the D'Ottaviano and da Costa system J ₃ and da Costa's systems C _n, 1≤ n≤ω.     

On the Existence of Continua of Logics Between Some Intermediate Predicate Logics

A method for constructing continua of logics squeezed between some intermediate predicate logics, developed by Suzuki [8], is modified and applied to intervals of the form [L, L+ ¬¬S], where Lis a predicate logic, Sis a closed predicate formula. This solves one of the problems from Suzuki's paper.     

Analytic Tableau Systems and Interpolation for the Modal Logics KB, KDB, K5, KD5

We give complete sequent-like tableau systems for the modal logics KB, KDB, K5, and KD5. Analytic cut rules are used to obtain the completeness. Our systems have the analytic superformula property and can thus give a decision procedure. Using the systems, we prove the Craig interpolation lemma for the mentioned logics.     

An almost general splitting theorem for modal logic

Given a normal (multi-)modal logic a characterization is given of the finitely presentable algebras A whose logics L A split the lattice of normal extensions of . This is a substantial generalization of Rautenberg [10] and [11] in which is assumed to be weakly transitive and A to be finite. We also obtain as a direct consequence a result by Blok [2] that for all cycle-free and finite A L A splits the lattice of normal extensions of K. Although we firmly believe it to be true, we have not been able to prove that if a logic splits the lattice of extensions of then is the logic of an algebra finitely presentable over ; in this respect our result remains partial.     

Algebraization, Parametrized Local Deduction Theorem and Interpolation for Substructural Logics over FL

Substructural logics have received a lot of attention in recent years from the communities of both logic and algebra. We discuss the algebraization of substructural logics over the full Lambek calculus and their connections to residuated lattices, and establish a weak form of the deduction theorem that is known as parametrized local deduction theorem. Finally, we study certain interpolation properties and explain how they imply the amalgamation property for certain varieties of residuated lattices. Dedicated to the memory of Willem Johannes Blok     

On the Closure Properties of the Class of Full G-models of a Deductive System

In this paper we consider the structure of the class FGModS of full generalized models of a deductive system S from a universal-algebraic point of view, and the structure of the set of all the full generalized models of S on a fixed algebra A from the lattice-theoretical point of view; this set is represented by the lattice FACS_s A of all algebraic closed-set systems C on A such that (A, C) ε FGModS. We relate some properties of these structures with tipically logical properties of the sentential logic S. The main algebraic properties we consider are the closure of FGModS under substructures and under reduced products, and the property that for any A the lattice FACS_s A is a complete sublattice of the lattice of all algebraic closed-set systems over A. The logical properties are the existence of a fully adequate Gentzen system for S, the Local Deduction Theorem and the Deduction Theorem for S. Some of the results are established for arbitrary deductive systems, while some are found to hold only for deductive systems in more restricted classes like the protoalgebraic or the weakly algebraizable ones. The paper ends with a section on examples and counterexamples. Dedicated to the memory of Willem Johannes Blok     

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.     

On the relevant systemsP andP * and some related systems

In this paper we study the systemsP andP ^* (see Arruda and da Costa,O paradoxo de Curry-Moh Shaw-Kwei, Boletim da Sociedade Matemtica de São Paulo 18 (1966)) and some related systems. In the last section, we prove that certain set theories havingP andP ^* as their underlying logics are non-trivial.     

On the size of refutation Kripke models for some linear modal and tense logics

LetL be any modal or tense logic with the finite model property. For eachm, definer _L (m) to be the smallest numberr such that for any formulaA withm modal operators,A is provable inL if and only ifA is valid in everyL-model with at mostr worlds. Thus, the functionr _L determines the size of refutation Kripke models forL. In this paper, we will give an estimation ofr _L (m) for some linear modal and tense logicsL.     

Quine and Slater on Paraconsistency and Deviance

In a famous and controversial paper, B. H. Slater has argued against the possibility of paraconsistent logics. Our reply is centred on the distinction between two aspects of the meaning of a logical constant ^*c^* in a given logic: its operational meaning, given by the operational rules for ^*c^* in a cut-free sequent calculus for the logic at issue, and its global meaning, specified by the sequents containing ^*c^* which can be proved in the same calculus. Subsequently, we use the same strategy to counter Quine's meaning variance argument against deviant logics. In a nutshell, we claim that genuine rivalry between (similar) logics ^*L^* and ^*L^* is possible whenever each constant in ^*L^* has the same operational meaning as its counterpart in ^*L^* although differences in global meaning arise in at least one case.     

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.     

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.     

Proof Nets for the Multimodal Lambek Calculus

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.