Proof Translations for Intuitionistic Modal Logic
Justus Becker
Abstract:
Extending sequent calculus with further structure or language has been a fruitful approach in structural proof theory for finding different cut-free complete proof systems. Finding translations between these different calculi not only gives new completeness results, but also insights into how these different calculi compare. While most research has gone into comparing systems that can be seen as notational variants of each other, only some investigation has been done into systems that are structurally different. Two such structurally different calculi exist for the intuitionistic modal logic IK, namely the (simple) nested Maehara-style calculus, NIKm, and the bi-labelled semantic calculus, labIK_≤ . Intuitionistic modal logics are modal logics whose modal free fragments are an intuitionistic (propositional or predicate) logic, one of which is IK which is defined in the tradition of Fischer Servi. In this thesis we will introduce intuitionistic modal logics together with their Kripke semantics and some of its proof theory, before establishing an effective two way translation between labIK_≤ and NIKm. Constructing the translations relies on admissible and derivable rules in these systems as well as constructing translatable derivations. The translations that we define shed new light on the relationship between invertibility and back-tracking in proof search, including how specifically these two systems compare to each other.