Nested Sequents for Interpolation and Realization

Structural proof theory provides tools for analyzing logical theories by means of analytic proof formalisms. Formalisms such as sequent-like calculi and tableau systems are instrumental for automated proof search and are routinely used for establishing various metalogical properties. The three main aims of this project are to establish three metalogical properties: interpolation (primarily Craig interpolation), realization of modality with justification terms, and decidability. These three properties are to be investigated primarily for intuitionistic modal logics. Intuitionistic modal logics have been studied since 1948 and have their roots in the philosophy of science and the foundations of mathematics. In addition, they have multiple connections to computer science applications, such as Lax Logic, authorization logics, descriptions of communicating systems, lambda-calculus style semantics for functional programming languages with a monad, and reasoning based on partial information, just to name a few. Craig interpolation is sometimes called the last significant metalogical property to be formulated. The first aim of this project is to develop a general method of proving the interpolation property constructively based on nested sequent calculi and to extend this method to more general labelled sequent calculi. Justification logics have been introduced as a way of solving a long-standing problem of classical provability semantics for intuitionistic logic, which was posed by Gödel. The main idea of justification logics consists in refining modal reasoning by introducing a family of terms to replace one modality. These terms have been interpreted as proofs for modal provability logics, and as justifications for modal epistemic logic. The connections to the more traditional modal formalisms are by means of two-way validity-preserving translations, called forgetful projection and realization, with the latter being the non-trivial direction. While most modal logics refined via a realization have been classical, my research suggests that intuitionistic modal logics are even better suited for such a refinement. The second aim of this project is to develop a uniform realization method for intuitionistic modal logics based on their nested sequent representations. This would also enable the study of self-referential properties of intuitionistic modalities. The third aim of this project is to develop a method for proving decidability of intuitionistic modal logics based on their nested sequent representations, with the view of answering well-known open questions for some basic logics, such as intuitionistic S4.

No additional funding sources recorded.