Abstract
Correspondence theory originally arises as the study of the relation between modal formulas and firstorder formulas interpreted over Kripke frames. We say that a modal formula and a firstorder 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 Sahlqvistvan Benthem theorem provides an algorithm to transform a class of modal formulas, which are later called Sahlqvist formulas, into their corresponding firstorder formulas. The algorithm SQEMA provides a modal languagebased algorithm to transform a modal formula into a pure modal formula in an expanded language, and then translate the pure modal formula into the firstorder 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 dualitytheoretic and orderalgebraic 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 ordertheoretic 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 ordertheoretic and algebraic insights, is given, which effectively computes firstorder 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 Sahlqvisttype 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 filterdescriptive possibility frames. Chapter 4 applies the unified correspondence methodology to modal compact Hausdorff spaces, and gives alternative proofs of canonicitytype 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.
In the development of correspondence theory, the algorithmic aspect receives increasing attention. The Sahlqvistvan Benthem theorem provides an algorithm to transform a class of modal formulas, which are later called Sahlqvist formulas, into their corresponding firstorder formulas. The algorithm SQEMA provides a modal languagebased algorithm to transform a modal formula into a pure modal formula in an expanded language, and then translate the pure modal formula into the firstorder 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 dualitytheoretic and orderalgebraic 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 ordertheoretic 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 ordertheoretic and algebraic insights, is given, which effectively computes firstorder 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 Sahlqvisttype 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 filterdescriptive possibility frames. Chapter 4 applies the unified correspondence methodology to modal compact Hausdorff spaces, and gives alternative proofs of canonicitytype 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.
Original language  English 

Awarding Institution 

Supervisors/Advisors 

Award date  23 Feb 2018 
DOIs  
Publication status  Published  2018 