A Sahlqvist theorem for distributive modal logic

In this paper we consider distributive modal logic, a setting in which we may add modalities, such as classical types of modalities as well as weak forms of negation, to the fragment of classical propositional logic given by conjunction, disjunction, true, and false. For these logics we define both algebraic semantics, in the form of distributive modal algebras, and relational semantics, in the form of ordered Kripke structures. The main contributions of this paper lie in extending the notion of Sahlqvist axioms to our generalized setting and proving both a correspondence and a canonicity result for distributive modal logics axiomatized by Sahlqvist axioms. Our proof of the correspondence result relies on a reduction to the classical case, but our canonicity proof departs from the traditional style and uses the newly extended algebraic theory of canonical extensions.     

Algorithmic correspondence and canonicity for distributive modal logic

We define the algorithm ALBA for the language of the same distributive modal logic (DML) for which a Sahlqvist theorem was proved by Gehrke, Nagahashi, and Venema. Successful executions of ALBA compute the local first-order correspondents of input DML inequalities, and also guarantee their canonicity. The class of inequalities on which ALBA is successful is strictly larger than the newly introduced class of inductive inequalities, which in its turn properly extends the Sahlqvist inequalities of Gehrke et al. Evidence is given to the effect that, as their name suggests, inductive inequalities are the distributive counterparts of the inductive formulas of Goranko and Vakarelov in the classical setting.     

Monadic Bounded Residuated Lattices

Bounded integral residuated lattices form a large class of algebras which contains algebraic counterparts of several propositional logics behind many-valued reasoning and intuitionistic logic. In the paper we introduce and investigate monadic bounded integral residuated lattices which can be taken as a generalization of algebraic models of the predicate calculi of those logics in which only a single variable occurs.     

The relation between intuitionistic and classical modal logics

Intuitionistic propositional logicInt and its extensions, known as intermediate or superintuitionistic logics, in many respects can be regarded as just fragments of classical modal logics containingS4. The main aim of this paper is to construct a similar correspondence between intermediate logics augmented with modal operators—we call them intuitionistic modal logics—and classical polymodal logics We study the class of intuitionistic polymodal logics in which modal operators satisfy only the congruence rules and so may be treated as various sorts of □ and ◇. Supported by the Alexander von Humboldt Foundation. Translated fromAlgebra i Logika, Vol. 36, No. 2, pp. 121–155, March–April, 1997.     

The Gödel-McKinsey-Tarski embedding for infinitary intuitionistic logic and its extensions

The Gödel-McKinsey-Tarski embedding allows to view intuitionistic logic through the lenses of modal logic. In this work, an extension of the modal embedding to infinitary intuitionistic logic is introduced. First, a neighborhood semantics for a family of axiomatically presented infinitary modal logics is given and soundness and completeness are proved via the method of canonical models. The semantics is then exploited to obtain a labelled sequent calculus with good structural properties. Next, soundness and faithfulness of the embedding are established by transfinite induction on the height of derivations: the proof is obtained directly without resorting to non-constructive principles. Finally, the modal embedding is employed in order to relate classical, intuitionistic and modal derivability in infinitary logic extended with axioms.     

Canonical formulas for <Emphasis Type="Italic">k</Emphasis>-potent commutative,integral, residuated lattices

Canonical formulas are a powerful tool for studying intuitionistic and modal logics. Indeed, they provide a uniform and semantic way of axiomatising all extensions of intuitionistic logic and all modal logics above K4. Although the method originally hinged on the relational semantics of those logics, recently it has been completely recast in algebraic terms. In this new perspective, canonical formulas are built from a finite subdirectly irreducible algebra by describing completely the behaviour of some operations and only partially the behaviour of some others. In this paper, we export the machinery of canonical formulas to substructural logics by introducing canonical formulas for k-potent, commutative, integral, residuated lattices (k-CIRL). We show that any subvariety of k-CIRL is axiomatised by canonical formulas. The paper ends with some applications and examples.     

Fibered universal algebra for first-order logics

We extend Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a general framework for providing fibered algebraic semantics for general first-order logics. This framework includes a natural notion of substitution, which allows first-order logics to be considered as structural closure operators just as propositional logics are in abstract algebraic logic. We then establish an extension of the homomorphism theorem from universal algebra for generalized prop-categories and characterize two natural closure operators on the prop-categorical semantics. The first closes a class of structures (which are interpreted as morphisms of prop-categories) under the satisfaction of their common first-order theory and the second closes a class of prop-categories under their associated first-order consequence. It turns out that these closure operators have characterizations that closely mirror Birkhoff's characterization of the closure of a class of algebras under the satisfaction of their common equational theory and Blok and Jónsson's characterization of closure under equational consequence, respectively. These algebraic characterizations of the first-order closure operators are unique to the prop-categorical semantics. They do not have analogues, for example, in the Tarskian semantics for classical first-order logic. The prop-categories we consider are much more general than traditional intuitionistic prop-categories or triposes (i.e., topos representing indexed partially ordered sets). Nonetheless, to the best of our knowledge, our results are new, even when restricted to these special classes of prop-categories.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

Algebraic proof theory for substructural logics: Cut-elimination and completions

We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.We introduce the substructural hierarchy — a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N₂ in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.     

A semantic hierarchy for intuitionistic logic

Brouwer’s views on the foundations of mathematics have inspired the study of intuitionistic logic, including the study of the intuitionistic propositional calculus and its extensions. The theory of these systems has become an independent branch of logic with connections to lattice theory, topology, modal logic, and other areas. This paper aims to present a modern account of semantics for intuitionistic propositional systems. The guiding idea is that of a hierarchy of semantics, organized by increasing generality: from the least general Kripke semantics on through Beth semantics, topological semantics, Dragalin semantics, and finally to the most general algebraic semantics. While the Kripke, topological, and algebraic semantics have been extensively studied, the Beth and Dragalin semantics have received less attention. We bring Beth and Dragalin semantics to the fore, relating them to the concept of a nucleus from pointfree topology, which provides a unifying perspective on the semantic hierarchy.     

On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics.     

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.     

Hypersequent calculi for intuitionistic logic with classical atoms

We discuss a propositional logic which combines classical reasoning with constructive reasoning, i.e., intuitionistic logic augmented with a class of propositional variables for which we postulate the decidability property. We call it intuitionistic logic with classical atoms. We introduce two hypersequent calculi for this logic. Our main results presented here are cut-elimination with the subformula property for the calculi. As corollaries, we show decidability, an extended form of the disjunction property, the existence of embedding into an intuitionistic modal logic and a partial form of interpolation.     

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.     

Monadic Bounded Commutative Residuated ℓ-monoids

Bounded commutative residuated ℓ-monoids are a generalization of algebras of propositional logics such as BL-algebras, i.e. algebraic counterparts of the basic fuzzy logic (and hence consequently MV-algebras, i.e. algebras of the Łukasiewicz infinite valued logic) and Heyting algebras, i.e. algebras of the intuitionistic logic. Monadic MV-algebras are an algebraic model of the predicate calculus of the Łukasiewicz infinite valued logic in which only a single individual variable occurs. We introduce and study monadic residuated ℓ-monoids as a generalization of monadic MV-algebras. Jiří Rachůnek was supported by the Council of Czech Goverment MSM 6198959214.     

A focused approach to combining logics

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.     

Bilattice logic of epistemic actions and knowledge

Baltag, Moss, and Solecki proposed an expansion of classical modal logic, called logic of epistemic actions and knowledge (EAK), in which one can reason about knowledge and change of knowledge. Kurz and Palmigiano showed how duality theory provides a flexible framework for modeling such epistemic changes, allowing one to develop dynamic epistemic logics on a weaker propositional basis than classical logic (for example an intuitionistic basis). In this paper we show how the techniques of Kurz and Palmigiano can be further extended to define and axiomatize a bilattice logic of epistemic actions and knowledge (BEAK). Our propositional basis is a modal expansion of the well-known four-valued logic of Belnap and Dunn, which is a system designed for handling inconsistent as well as potentially conflicting information. These features, we believe, make our framework particularly promising from a computer science perspective.     

Densification via polynomials,languages, and frames

It is known that every countable totally ordered set can be embedded into a countable dense one. We extend this result to totally ordered commutative monoids and to totally ordered commutative residuated lattices (the latter result fails in the absence of commutativity). The latter has applications to density elimination of semilinear substructural logics. In particular we obtain as a corollary a purely algebraic proof of the standard completeness of uninorm logic; the advantage over the known proof-theoretic proof and the semantical proof is that it is extremely short and transparent and all details can be verified easily using standard algebraic constructions.     

Proof analysis in intermediate logics

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the G?del–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules.     

Note on grammatical translations of logical calculi

It is shown that there exists no grammatical translation into classical (propositional) logic of the modal logics, nor of intuitionistic logic and of the relatedness and dependence logics, as defined in Richard L. Epstein's bookThe Semantic foundations of logic. In the book the result is proved for translations without parameters.Classical propositional logicPC can be translated into other logics. Usually the grammatical structure of propositions is preserved, in the sense of the following definition.