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. A fundamental tool for attaining this level of generality and uniformity is a principled way, based on order theory, to define the Sahlqvist and inductive formulas and inequalities in every such signature. 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 versions of Gödel-McKinsey- Tarski translations, suitably defined in each signature, as main tools. In view of this state-of-the-art, it is natural to ask (1) whether a general perspective on Gödel-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 Gödel-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 Gödel-McKinsey-Tarski translations. In the present paper, we set out to answer these questions. We answer (1) in the armative; 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.@en

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. @en

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. @en

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. @en

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. @en

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. @en

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.@en

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.@en

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. @en

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 ◊x∨◊y=◊(x∨y) and multiplicativity □x∧□y=□(x∧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. @en

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 ◊x∨◊y=◊(x∨y) and multiplicativity □x∧□y=□(x∧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. @en

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 ◊x∨◊y=◊(x∨y) and multiplicativity □x∧□y=□(x∧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. @en

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. @en

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. @en

Correspondence theory originally arises as the study of the relation between modal formulas and first-order formulas interpreted over Kripke frames. We say that a modal formula and a first-order formula correspond to each other if they are valid on the same class of Kripke frames. Canonicity theory is closely related to correspondence theory. We say that a modal formula is canonical if it is valid on its canonical frame, or equivalently,if its validity is preserved from a modal algebra to its canonical extension, or from a descriptive general frame to its underlying Kripke frame. Canonicity is closely related to completeness. If a modal formula is canonical, then the normal modal logic axiomatized by this modal formula is complete with respect to the class of Kripke frames defined by it. In the development of correspondence theory, the algorithmic aspect receives increasing attention. The Sahlqvist-van Benthem theorem provides an algorithm to transform a class of modal formulas, which are later called Sahlqvist formulas, into their corresponding first-order formulas. The algorithm SQEMA provides a modal language-based algorithm to transform a modal formula into a pure modal formula in an expanded language, and then translate the pure modal formula into the first-order language. SQEMA succeeds on a strictly larger class of modal formulas, which are called inductive formulas. In recent years, unified correspondence theory is developed based on duality-theoretic and order-algebraic insights. In this approach, a very general syntactic definition of Sahlqvist and inductive formulas is given, which applies uniformly to each logical signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives. In addition, the Ackermann lemma based algorithm ALBA, which is a generalization of SQEMA based on order-theoretic and algebraic insights, is given, which effectively computes first-order correspondents of input formulas/inequalities, and is guaranteed to succeed on the Sahlqvist and inductive classes of formulas/inequalities. This dissertation belong to the line of research of unified correspondence theory. Chapter 3 applies the unified correspondence methodology to possibility semantics, and gives alternative proofs of Sahlqvist-type correspondence results to the ones in [196], and extends these results from Sahlqvist formulas to the strictly larger class of inductive formulas, and from the full possibility frames to filter-descriptive possibility frames. Chapter 4 applies the unified correspondence methodology to modal compact Hausdorff spaces, and gives alternative proofs of canonicity-type preservation results to the ones in [14]. Chapter 5 examines the power and limits of the translation method in obtaining correspondence and canonicity results. Chapter 6 is about an application of unified correspondence theory to the proof theory of strict implication logics, showing the usefulness of unified correspondence theory in the design of analytic Gentzen sequent calculi, especially when it comes to computing the corresponding analytic rules of a given sequent.@en