Abstract The symmetric strict implication calculus $\mathsf{S}^{2}\mathsf{IC}$ is a modal calculus for compact Hausdorff spaces. This is established through de Vries duality, linking compact Hausdorff spaces with de Vries algebras—complete Boolean algebras equipped with a special relation. Modal compact Hausdorff spaces are compact Hausdorff spaces enriched with a continuous relation. These spaces correspond, via modalized de Vries duality, to upper continuous modal de Vries algebras. In this paper, we introduce the modal symmetric strict implication calculus $\mathsf{MS}^{2}\mathsf{IC}$, which extends $\mathsf{S}^{2}\mathsf{IC}$. We prove that $\mathsf{MS}^{2}\mathsf{IC}$ is strongly sound and complete with respect to upper continuous modal de Vries algebras, thereby providing a logical calculus for modal compact Hausdorff spaces. We also develop a relational semantics for $\mathsf{MS}^{2}\mathsf{IC}$ that we employ to show admissibility of various $\Pi_{2}$-rules in this system.

Abstract In this paper, we investigate the numerical expressive power of various logical languages, encompassing fragments of Presburger Arithmetic (PbA), monadic second-order logic with counting with respect to finite domains (MSO$^{\phi }(\#)$) and shallow second-order graded modal logic with counting with respect to image-finite frames (SOGML$^{\textsf{s},\phi }$(#)). We show that in their respective existential fragments, the $1$-free fragment of PbA, the =-free fragment of MSO$^{\phi }(\#)$ and the graded modality-free fragment of SOGML$^{\textsf{s},\phi }$(#) possess equivalent numerical expressive power, specifically defining strongly semilinear sets. When adding universal quantifiers or adding $1$, = and graded modality to these three languages, the resulting definable sets become semilinear sets.

Abstract Modal logic with propositional quantifiers (i.e. second-order propositional modal logic ($\textsf {SOPML}$)) has been considered since the early time of modal logic. Its expressive power and complexity are high, and its van Benthem–Rosen theorem and Goldblatt–Thomason theorem have been proved by ten Cate (2006, J. Philos. Logic, 35, 209–223). However, the Sahlqvist theory of $\textsf {SOPML}$ has not been considered in the literature. In the present paper, we fill in this gap. We develop the Sahlqvist correspondence theory for $\textsf {SOPML}$, which covers and properly extends existing Sahlqvist formulas in basic modal logic. We define the class of Sahlqvist formulas for $\textsf {SOMPL}$ step by step in a hierarchical way, each formula of which is shown to have a first-order correspondent over Kripke frames effectively computable by an algorithm $\textsf {ALBA}^{\textsf {SOMPL}}$. In addition, we show that certain $\varPi _2$-rules correspond to $\varPi _2$-Sahlqvist formulas in $\textsf {SOMPL}$, which further correspond to first-order conditions, and that even for very simple $\textsf {SOMPL}$ Sahlqvist formulas, they could already be non-canonical.

Abstract The present paper develops a unified correspondence treatment of the Sahlqvist theory for possibility semantics, extending the results in the work by Yamamoto (2016, Journal of Logic and Computation, 27, 2411–2430) from Sahlqvist formulas to the strictly larger class of inductive formulas and from the full possibility frames to filter-descriptive possibility frames. Specifically, we define the possibility semantics version of the algorithm Ackermann lemma based algorithm (ALBA) and an adapted interpretation of the expanded modal language used in the algorithm. One notable feature of the adaptation of ALBA to possibility frames setting is that the so-called nominal variables, which are interpreted as complete join-irreducibles in the standard setting, are interpreted as regular open closures of ‘singletons’ in the present setting, which is a novelty of the present paper. We prove the soundness of the algorithm with respect to both (the dual algebras of) full possibility frames and (the dual algebras of) filter-descriptive possibility frames, use the algorithm to give an alternative proof to the one in the work by Holliday (2016, Possibility frames and forcing for modal logic. UC Berkeley Working Paper in Logic and the Methodology of Science. URL. http://escholarship.org/uc/item/9v11r0dq) that the inductive formulas are constructively canonical and show that the algorithm succeeds on inductive formulas. We make some comparisons among different semantic settings in the design of the algorithms and fit possibility semantics into this broader picture.

In recent years, unified correspondence has been developed as a generalized Sahlqvist theory which applies uniformly to all signatures of normal and regular (distributive) lattice expansions. This includes a general definition of the Sahlqvist and inductive formulas and inequalities in every such signature, based on order theory. This definition covers in particular all (bi-)intuitionistic modal logics. The theory of these logics has been intensively studied over the past seventy years in connection with classical polyadic modal logics, using suitable versions of Goedel-McKinsey-Tarski translations as main tools. It is therefore natural to ask (1) whether a general perspective on Goedel-McKinsey-Tarski translations can be attained, also based on order-theoretic principles like those underlying the general definition of Sahlqvist and inductive formulas and inequalities, which accounts for the known Goedel-McKinsey-Tarski translations and applies uniformly to all signatures of normal (distributive) lattice expansions; (2) whether this general perspective can be used to transfer correspondence and canonicity theorems for Sahlqvist and inductive formulas and inequalities in all signatures described above under Goedel-McKinsey-Tarski translations. In the present paper, we set out to answer these questions. We answer (1) in the affirmative; as to (2), we prove the transfer of the correspondence theorem for inductive inequalities of arbitrary signatures of normal distributive lattice expansions. We also prove the transfer of canonicity for inductive inequalities, but only restricted to arbitrary normal modal expansions of bi-intuitionistic logic. We also analyze the difficulties involved in obtaining the transfer of canonicity outside this setting, and indicate a route to extend the transfer of canonicity to all signatures of normal distributive lattice expansions.

The present article aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap.These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into 'analytic'structural rules of display calculi.In this context, a rule is 'analytic'if adding it to a display calculus preserves Belnap's cut-elimination theorem.In recent years, the state-of-the-art in correspondence theory has been uniformly extended from classical modal logic to diverse families of non-classical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi.This generalization has given rise to a theory called unified correspondence, the most important technical tools of which are the algorithm ALBA, and the syntactic characterization of Sahlqvist-type classes of formulas and inequalities which is uniform in the setting of normal DLE-logics (logics the algebraic semantics of which is based on bounded distributive lattices).We apply unified correspondence theory, with its tools and insights, to extend Kracht's results and prove his claims in the setting of DLE-logics.The results of the present article characterize the space of properly displayable DLE-logics.

The unified correspondence theory for distributive lattice expansion logics (DLE-logics) is specialized to strict implication logics.As a consequence of a general semantic consevativity result, a wide range of strict implication logics can be conservatively extended to Lambek Calculi over the bounded distributive full non-associative Lambek calculus (BDFNL).Many strict implication sequents can be transformed into analytic rules employing one of the main tools of unified correspondence theory, namely (a suitably modified version of) the Ackermann lemma based algorithm ALBA.Gentzen-style cut-free sequent calculi for BDFNL and its extensions with analytic rules which are transformed from strict implication sequents, are developed. A Algebraic Correspondence

We extend unified correspondence theory to Kripke frames with impossible worlds and their associated regular modal logics. These are logics the modal connectives of which are not required to be normal: only the weaker properties of additivity |$\Diamond x\vee \Diamond y = \Diamond (x\vee y)$| and multiplicativity |$\Box x\wedge \Box y = \Box (x\wedge y)$| are required. Conceptually, it has been argued that their lacking necessitation makes regular modal logics better suited than normal modal logics at the formalization of epistemic and deontic settings. From a technical viewpoint, regularity proves to be very natural and adequate for the treatment of algebraic canonicity Jónsson-style. Indeed, additivity and multiplicativity turn out to be key to extend Jónsson’s original proof of canonicity to the full Sahlqvist class of certain regular distributive modal logics naturally generalizing distributive modal logic. Most interestingly, additivity and multiplicativity are key to Jónsson-style canonicity also in the original (i.e. normal DML. Our contributions include: the definition of Sahlqvist inequalities for regular modal logics on a distributive lattice propositional base; the proof of their canonicity following Jónsson’s strategy; the adaptation of the algorithm ALBA to the setting of regular modal logics on two non-classical (distributive lattice and intuitionistic) bases; the proof that the adapted ALBA is guaranteed to succeed on a syntactically defined class which properly includes the Sahlqvist one; finally, the application of the previous results so as to obtain proofs, alternative to Kripke’s, of the strong completeness of Lemmon’s epistemic logics E2-E5 with respect to elementary classes of Kripke frames with impossible worlds.

The theory of canonical extensions typically considers extensions of maps A→B to maps Aδ→Bδ. In the present article, the theory of canonical extensions of maps A→Bδ to maps Aδ→Bδ is developed, and is applied to obtain a new canonicity proof for those inequalities in the language of Distributive Modal Logic (DML) on which the algorithm ALBA [9] is successful.