Inspired by the recent work on approximations of classical logic, we present a method that approximates several modal logics in a modular way. Our starting point is the limitation of the n-degree of introspection that is allowed, thus generating modaln-logics. The semantics for n-logics is presented, in which formulas are evaluated with respect to paths, and not possible worlds. A tableau-based proof system is presented, n-SST, and soundness and completeness is shown for the approximation of modal logics image and image.

We establish the dichotomy property for stable canonical multi-conclusion rules for IPC, K4, and S4. This yields an alternative proof of existence of explicit bases of admissible rules for these logics.

Fibring is defined as a mechanism for combining logics with a first-order base, at both the semantic and deductive levels. A completeness theorem is established for a wide class of such logics, using a variation of the Henkin method that takes advantage of the presence of equality and inequality in the logic. As a corollary, completeness is shown to be preserved when fibring logics in that class. A modal first-order logic is obtained as a fibring where neither the Barcan formula (...) nor its converse hold. (shrink)

In this paper we present a general theory of normal forms, based on a categorial result for the free monoid construction. We shall use the theory mainly for proposictional modal logic, although it seems to have a wider range of applications. We shall formally represent normal forms as combinatorial objects, basically labelled trees and forests. This geometric conceptualization is implicit in and our approach will extend it to other cases and make it more direct: operations of a purely geometric and (...) combinatorial nature will be introduced in order to give a mathematical description of the basic logical/algebraic constructions .We begin by recalling the above-mentioned categorial construction: we need a careful inspection of it because in the various examples considered later we plan to deduce from it in a uniform way the normal forms and the description of finitely generated free algebras. This method always works whenever we can describe the category of algebras corresponding to the logic under consideration as a T-objects category. When this simple description seems not to be available, still the general theory might be of some interest, because a description of the category of algebras as a T-objects category plus equation is possible .The central part of the paper is more advanced and specific: we show how the general approach presented here can provide some insights even in the basic case of the modal system K. Section 4 contains a contribution to the theory of normal forms, namely the description of the uniform substitution. This result will enable us to give a duality theorem for the category of finitely generated free modal algebras and in Section 5 to provide a characterization of the collections of normal forms which happen to be normal forms for a logic, thus giving a description of the lattice of modal logics.Section 6 deals with some applications: we shall show how to use normal forms in order to prove for the modal system K the definability of higher-order propositional quantifiers and of the tense operator F .As to the prerequisites, the paper is almost self-contained. The reader is only assumed to have familiarity with standard techniques in algebraic logic ). Knowledge of the basic facts about adjoint functors is required too, see e.g. McLane or the appendix. (shrink)

This paper develops a new framework for combining propositional logics, called "juxtaposition". Several general metalogical theorems are proved concerning the combination of logics by juxtaposition. In particular, it is shown that under reasonable conditions, juxtaposition preserves strong soundness. Under reasonable conditions, the juxtaposition of two consequence relations is a conservative extension of each of them. A general strong completeness result is proved. The paper then examines the philosophically important case of the combination of classical and intuitionist logics. Particular attention is (...) paid to the phenomenon of collapse. It is shown that there are logics with two stocks of classical or intuitionist connectives that do not collapse. Finally, the paper briefy investigates the question of which rules, when added to these logics, lead to collapse. (shrink)

We consider a 2-valued non-deterministic connective \({\wedge \!\!\!\!\!\vee }\) defined by the table resulting from the entry-wise union of the tables of conjunction and disjunction. Being half conjunction and half disjunction we named it _platypus_. The value of \({\wedge \!\!\!\!\!\vee }\) is not completely determined by the input, contrasting with usual notion of Boolean connective. We call non-deterministic Boolean connective any connective based on multi-functions over the Boolean set. In this way, non-determinism allows for an extended notion of truth-functional connective. (...) Unexpectedly, this very simple connective and the logic it defines, illustrate various key advantages in working with generalized notions of semantics (by incorporating non-determinism), calculi (by allowing multiple-conclusion rules) and even of logic (moving from Tarskian to Scottian consequence relations). We show that the associated logic cannot be characterized by any finite set of finite matrices, whereas with non-determinism two values suffice. Furthermore, this logic is not finitely axiomatizable using single-conclusion rules, however we provide a very simple analytic multiple-conclusion axiomatization using only two rules. Finally, deciding the associated multiple-conclusion logic is \(\mathbf {coNP}\) -complete, but deciding its single-conclusion fragment is in \({\mathbf {P}}\). (shrink)

The standard notion of formal theory, in logic, is in general biased exclusively towards assertion: it commonly refers only to collections of assertions that any agent who accepts the generating axioms of the theory should also be committed to accept. In reviewing the main abstract approaches to the study of logical consequence, we point out why this notion of theory is unsatisfactory at multiple levels, and introduce a novel notion of theory that attacks the shortcomings of the received notion by (...) allowing one to take both assertions and denials on a par. This novel notion of theory is based on a bilateralist approach to consequence operators, which we hereby introduce, and whose main properties we investigate in the present paper. (shrink)

We discuss the axiomatization of generalized consequence relations determined by non-deterministic matrices. We show that, under reasonable expressiveness requirements, simple axiomatizations can always be obtained, using inference rules which can have more than one conclusion. Further, when the non-deterministic matrices are finite we obtain finite axiomatizations with a suitable generalized subformula property.

Transfer theorems are central results in abstract algebraic logic that allow to generalize properties of the lattice of theories of a logic to any algebraic model and its lattice of filters. Their proofs sometimes require the existence of a natural extension of the logic to a bigger set of variables. Constructions of such extensions have been proposed in particular settings in the literature. In this paper we show that these constructions need not always work and propose a wider setting in (...) which they can still be used. (shrink)

Sections 1, 2 and 3 contain the main result, the strong finite axiomatizability of all 2-valued matrices. Since non-strongly finitely axiomatizable 3-element matrices are easily constructed the result reveals once again the gap between 2-valued and multiple-valued logic. Sec. 2 deals with the basic cases which include the important F i from Post's classification. The procedure in Sec. 3 reduces the general problem to these cases. Sec. 4 is a study of basic algebraic properties of 2-element algebras. In particular, we (...) show that equational completeness is equivalent to the Stone-property and that each 2-element algebra generates a minimal quasivariety. The results of Sec. 4 will be applied in Sec. 5 to maximality questions and to a matrix free characterization of 2-valued consequences in the lattice of structural consequences in any language. Sec. 6 takes a look at related axiomatization. problems for finite algebras and matrices. We study the notion of a propositional consequence with equality and, among other things, present explicit axiomatizations of 2-valued consequences with equality. (shrink)

Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. With minor (...) restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the logics. (shrink)

. The semantic collapse problem is perhaps the main difficulty associated to the very powerful mechanism for combining logics known as fibring. In this paper we propose cryptofibred semantics as a generalization of fibred semantics, and show that it provides a solution to the collapsing problem. In particular, given that the collapsing problem is a special case of failure of conservativeness, we formulate and prove a sufficient condition for cryptofibring to yield a conservative extension of the logics being combined. For (...) illustration, we revisit the example of combining intuitionistic and classical propositional logics. (shrink)

Fibring is recognized as one of the main mechanisms in combining logics, with great signicance in the theory and applications of mathematical logic. However, an open challenge to bring is posed by the collapsing problem: even when no symbols are shared, certain combinations of logics simply collapse to one of them, indicating that bring imposes unwanted interconnections between the given logics. Modulated bring allows a ner control of the combination, solving the collapsing problem both at the semantic and deductive levels. (...) Main properties like soundness and completeness are shown to be preserved, comparison with bring is discussed, and some important classes of examples are analyzed with respect to the collapsing problem. (shrink)

A completeness theorem is established for logics with congruence endowed with general semantics (in the style of general frames). As a corollary, completeness is shown to be preserved by fibring logics with congruence provided that congruence is retained in the resulting logic. The class of logics with equivalence is shown to be closed under fibring and to be included in the class of logics with congruence. Thus, completeness is shown to be preserved by fibring logics with equivalence and general semantics. (...) An example is provided showing that completeness is not always preserved by fibring ligics endowed with standard (non general) semantics. A categorial characterization of fibring is provided using coproducts and cocartesian liftings. (shrink)

Inspired by the recent work on approximations of classical logic, we present a method that approximates several modal logics in a modular way. Our starting point is the limitation of the n-degree of introspection that is allowed, thus generating modaln-logics. The semantics for n-logics is presented, in which formulas are evaluated with respect to paths, and not possible worlds. A tableau-based proof system is presented, n-SST, and soundness and completeness is shown for the approximation of modal logics image and image.

Uniform infinite bases are defined for the single-conclusion and multiple-conclusion admissible rules of the implication–negation fragments of intuitionistic logic and its consistent axiomatic extensions . A Kripke semantics characterization is given for the structurally complete implication–negation fragments of intermediate logics, and it is shown that the admissible rules of this fragment of form a PSPACE-complete set and have no finite basis.

. In this paper we address the question of recovering a logic system by combining two or more fragments of it. We show that, in general, by fibring two or more fragments of a given logic the resulting logic is weaker than the original one, because some meta-properties of the connectives are lost after the combination process. In order to overcome this problem, the categories Mcon and Seq of multiple-conclusion consequence relations and sequent calculi, respectively, are introduced. The main feature (...) of these categories is the preservation, by morphisms, of meta-properties of the consequence relations, which allows, in several cases, to recover a logic by fibring of its fragments. The fibring in this categories is called meta−fibring. Several examples of well-known logics which can be recovered by meta-fibring its fragments (in opposition to fibring in the usual categories) are given. Finally, a general semantics for objects in Seq (and, in particular, for objects in Mcon) is proposed, obtaining a category of logic systems called Log. A general theorem of preservation of completeness by fibring in Log is also obtained. (shrink)

. The paper presents a method for transforming a given sound and complete n-sequent proof system into an equivalent sound and complete system of ordinary sequents. The method is applicable to a large, central class of (generalized) finite-valued logics with the language satisfying a certain minimal expressiveness condition. The expressiveness condition decrees that the truth-value of any formula φ must be identifiable by determining whether certain formulas uniformly constructed from φ have designated values or not. The transformation preserves the general (...) structure of proofs in the original calculus in a way ensuring preservation of the weak cut elimination theorem under the transformation. The described transformation metod is illustrated on several concrete examples of many-valued logics, including a new application to information sources logics. (shrink)

We show that the join of two classical [respectively, regular, normal] modal logics employing distinct modal operators is a conservative extension of each of them.

The classesMatr( ) of all matrices (models) for structural finitistic entailments are investigated. The purpose of the paper is to prove three theorems: Theorem I.7, being the counterpart of the main theorem from Czelakowski [3], and Theorems II.2 and III.2 being the entailment counterparts of Bloom's results [1]. Theorem I.7 states that if a classK of matrices is adequate for , thenMatr( ) is the least class of matrices containingK and closed under the formation of ultraproducts, submatrices, strict homomorphisms and (...) strict homomorphic pre-images. Theorem II.2 in Section II gives sufficient and necessary conditions for a structural entailment to be finitistic. Section III contains theorems which characterize finitely based entailments. (shrink)

We study the general problem of strengthening the logic of a given matrix with a set of axioms, using the idea of rexpansion. We obtain two characterization methods: a very general but not very effective one, and then an effective method which only applies under certain restrictions on the given semantics and the shape of the axioms. We show that this second method covers a myriad of examples in the literature. Finally, we illustrate how to obtain analytic multiple-conclusion calculi for (...) the resulting logics. (shrink)

In this paper we address some central problems of combination of logics through the study of a very simple but highly informative case, the combination of the logics of disjunction and conjunction. At first it seems that it would be very easy to combine such logics, but the following problem arises: if we combine these logics in a straightforward way, distributivity holds. On the other hand, distributivity does not arise if we use the usual notion of extension between consequence relations. (...) A detailed discussion about this phenomenon, as well as some elucidation for it, is given. (shrink)

This paper contains some contributions to the study of Belnap's four-valued logic from an algebraic point of view. We introduce a finite Hilbert-style axiomatization of this logic, along with its well-known semantical presentation, and a Gentzen calculus that slightly differs from the usual one in that it is closer to Anderson and Belnap's formalization of their “logic of first-degree entailments”. We prove several Completeness Theorems and reduce every formula to an equivalent normal form. The Hilbert-style presentation allows us to characterize (...) the Leibniz congruence of the matrix models of the logic, and to find that the class of algebraic reducts of its reduced matrices is strictly smaller than the variety of De Morgan lattices. This means that the links between the logic and this class of algebras cannot be fully explained in terms of matrices, as in more classical logics. It is through the use of abstract logics as models that we are able to confirm that De Morgan lattices are indeed the algebraic counterpart of Belnap's logic, in the sense of Font and Jansana's recent theory of full models for sentential logics. Among other characterizations, we prove that its full models are those abstract logics that are finitary, do not have theorems, and satisfy the metalogical properties of Conjunction, Disjunction, Double Negation, and Weak Contraposition. As a consequence, we find that the Gentzen calculus presented at the beginning is strongly adequate for Belnap's logic and is algebraizable in the sense of Rebagliato and Verdú, having the variety of De Morgan lattices as its equivalent algebraic semantics. (shrink)

This is Part 1 of a paper on fibred semantics and combination of logics. It aims to present a methodology for combining arbitrary logical systems L i , i ∈ I, to form a new system L I . The methodology `fibres' the semantics K i of L i into a semantics for L I , and `weaves' the proof theory (axiomatics) of L i into a proof system of L I . There are various ways of doing this, we (...) distinguish by different names such as `fibring', `dovetailing' etc, yielding different systems, denoted by L F I , L D I etc. Once the logics are `weaved', further `interaction' axioms can be geometrically motivated and added, and then systematically studied. The methodology is general and is applied to modal and intuitionistic logics as well as to general algebraic logics. We obtain general results on bulk, in the sense that we develop standard combining techniques and refinements which can be applied to any family of initial logics to obtain further combined logics. The main results of this paper is a construction for combining arbitrary, (possibly not normal) modal or intermediate logics, each complete for a class of (not necessarily frame) Kripke models. We show transfer of recursive axiomatisability, decidability and finite model property. Some results on combining logics (normal modal extensions of K) have recently been introduced by Kracht and Wolter, Goranko and Passy and by Fine and Schurz as well as a multitude of special combined systems existing in the literature of the past 20-30 years. We hope our methodology will help organise the field systematically. (shrink)

What is the fundamental insight behind truth-functionality ? When is a logic interpretable by way of a truth-functional semantics? To address such questions in a satisfactory way, a formal definition of truth-functionality from the point of view of abstract logics is clearly called for. As a matter of fact, such a definition has been available at least since the 70s, though to this day it still remains not very widely well-known. A clear distinction can be drawn between logics characterizable through: (...) (1) genuinely finite-valued truth-tabular semantics; (2) no finite-valued but only an infinite-valued truthtabular semantics; (3) no truth-tabular semantics at all. Any of those logics, however, can in principle be characterized through non-truth-functional valuation semantics, at least as soon as their associated consequence relations respect the usual tarskian postulates. So, paradoxical as that might seem at first, it turns out that truth-functional logics may be adequately characterized by non-truth-functional semantics . Now, what feature of a given logic would guarantee it to dwell in class (1) or in class (2), irrespective of its circumstantial semantic characterization? (shrink)