Translational Embeddings via Stable Canonical Rules
Antonio Maria Cleani

Abstract:
This thesis presents a new uniform method for studying modal companions of superintuitionistic deductive systems and related notions, based on the machinery of stable canonical rules. Using our method, we obtain alternative proofs of classic results in the theory of modal companions, chiefly the Blok-Esakia theorem for both logics and rule systems. We also establish several new results about modal companions, including a generalisation of the Dummett-Lemmon conjecture to rule systems and axiomatic characterisations of modal companions and superintuitionistic fragments in terms of stable canonical rules.
Because stable canonical rules may be developed for any rule system admitting filtration, our method generalises smoothly to richer signatures. We illustrate this via two case studies. Firstly, we study tense companions of bi-superintuitionistic deductive systems. Via straightforward adaptations of the techniques used in the case of modal companions, we obtain a number of new results about tense companions, including an analogue of the Blok-Esakia theorem (which was known for logics but not rule systems), an extension of the Dummett-Lemmon conjecture, and axiomatic characterisations of tense companions and bi-superintuitionistic fragments in terms of stable canonical rules.
Secondly, we study the Kuznetsov-Muravitsky isomorphism between the lattice of extensions of the modal intuitionistic logic KM and the lattice of extensions of provability logic GL. We develop a new, more flexible analogue of stable canonical rules, called pre-stable canonical rules, which are based on a non-standard notion of filtration appropriate for KM and GL. Following essentially the same blueprint as in previous cases, we prove an extension of the Kuznetsov-Muravitsky theorem to rule systems, which yields the latter as a corollary, and obtain new axiomatic characterisations of the underlying isomorphisms in terms of pre-stable canonical rules.