Correspondence and Canonicity in Non-Classical Logic
Sumit Sourabh
Abstract:
In this thesis, we study correspondence and canonicity for non-classical logic using algebraic and order-topological methods. Correspondence theory is aimed at answering the question of how precisely modal, first-order, second-order languages interact and overlap in their shared semantic environment. The line of research in correspondence theory which concerns the present thesis is Sahlqvist correspondence theory --- which was originally developed for classical modal logic, and provides a systematic translation between classical modal logic and first-order logic.
Modal languages are expressive fragments of second-order logic when interpreted over relational structures. However, the celebrated Sahlqvist-van Benthem theorem, which is the cornerstone of the correspondence theory, states that for every formula in a large, syntactically defined class of modal formulas called Sahlqvist formulas, the correspondent is, in fact, a first-order sentence. Moreover, this correspondent can be computed effectively. Canonicity is closely related to correspondence, and ensures that logics axiomatized by these formulas are complete with respect to relational semantics. Thus, correspondence and canonicity together establish that Sahlqvist logics are semantically complete with respect to first-order definable classes of relational structures.
The first part of the thesis focuses on algebraic methods for correspondence and canonicity. In chapter 3, we introduce the algebraic approach to Sahlqvist-type correspondence results by proving the classical Sahlqvist correspondence theorem for basic modal logic in the algebraic setting of complex algebras of frames. In the algebraic setting, the reduction strategies for the elimination of the second order variables can be formulated entirely in order-theoretic terms. The order-theoretic conditions that guarantee the applicability of these strategies also lead to a positive characterization of Sahlqvist and inductive formulas across different signatures. Conradie and Palmigiano develop an Ackermann Lemma Based Algorithm (ALBA) for distributive modal logic based on an algebraic analysis of the correspondence theory. We extend the algorithm ALBA to regular modal logic (modal logic with non-normal modalities) and intuitionistic modal mu-calculus in Chapters 4 and 5, respectively. Moreover, we syntactically define the class of inductive inequalities in these languages, and show that the algorithm succeeds on them. In Chapter 6, we develop a version of ALBA for distributive lattice expansions (DLEs), using which we prove the canonicity of certain syntactically defined classes of DLE-inequalities (called the meta-inductive inequalities), relative to the structures in which the formulas asserting the additivity of some given terms are valid.
The second part focuses on order-topological methods. In Chapter 7, we introduce the concept of a subordination on a Boolean algebra, and develop a full categorical duality between Boolean algebras with a subordination and Stone spaces with a closed relation. We further extend this duality to show that the category of de Vries algebras is dual to the category of Gleason spaces, which are extremely disconnected spaces with a closed irreducible equivalence relation. This provides an alternative Jónsson-Tarski style duality to de Vries duality between de compact Hausdorff spaces and de Vries algebras. It also offers a possibility for developing a topological correspondence theory, and a logical calculus for modal compact Hausdorff spaces. In Chapter 8, we prove a Sahlqvist correspondence and canonicity theorem for topological fixed-point logic on compact Hausdorff spaces. This generalizes the Sambin-Vaccaro proof of canonicity for the language of positive modal mu-calculus interpreted over modal compact Hausdorff spaces.