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.

Logical theories are used to define and automate correct and efficient ways of reasoning. The applicability and usefulness of a logical theory is determined based, in part, on the positive logical properties it possesses. The most important of these properties are consistency, decidability and interpolation, which is sometimes called the last of the fundamental logical properties to be identified. The goal of this project was to develop novel methods of proving interpolation constructively using proof theory.Interpolation has close connections to algebra and computer science. Accordingly, it can be established by both algebraic and algorithmic methods. The latter are preferable because they provide witnesses for interpolation, so-called interpolants, rather than non-constructively demonstrating that interpolation holds. Proof theory is one of few robust methods of proving interpolation constructively by relying on analytic sequent calculi. The weakness of the method had been the rather limited availability of sequent calculi as far as more expressive and application-driven logical theories are concerned. The main achievement of this project was a significant extension of the proof-theoretic method to various generalizations of sequent calculi, including but not limited to hypersequents, nested sequents, and labelled sequents. Moreover, for a wide variety of modal logics, we have shown that it is possible to automate not only the process of constructing interpolants once the interpolation property is demonstrated, but also automate the proof of the interpolation property itself.Given the widespread use of modal logic to describe phenomena as disparate as knowledge, time, and obligation, the development of automated calibration tools for such modal logics can potentially guide the choice of optimal reasoning frameworks in areas such as law, ethics, and distributed computing.