Verschachtelte Sequenzen für Interpolation und Realisation

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.

Logische Theorien werden dazu verwendet, um korrekte und effiziente Methoden des Schließens zu definieren sowie zu automatisieren. Die Anwendbarkeit und die Nützlichkeit einer logischen Theorie basieren zum Teil auf den positiven logischen Eigenschaften, wobei die logische Konsistenz und die Entscheidbarkeit einer Theorie zusammen mit der Existenz von Interpolanten besonders hervorzuheben sind. Letztgenanntes wird häufig als die abschließende fundamentale logische Eigenschaft bezeichnet. Das Ziel dieses Projekts war es, neue Methoden zur konstruktiven Beweisbarkeit der Interpolation, unter Zuhilfenahme beweistheoretischer Verfahren, zu entwickeln.Aufgrund der nahen Verwandtschaft der Interpolation zur Algebra und den Computerwissenschaften, können algebraische und algorithmische Methoden herangezogen werden, um die Interpolation zu beweisen. Im Gegensatz zu algebraischen Methoden, bei denen lediglich die Existenz von Interpolanten bewiesen wird, liefern algorithmische Methoden zusätzlich gültige Interpolanten. Beweistheorie ist eine der wenigen robusten Verfahren, um die Existenz von Interpolanten konstruktiv abzuleiten. Hierbei werden Sequenzkalküle verwendet, welche allerdings gerade für aussagekräftigere und anwendungsbezogenere logische Theorien kaum vorhanden sind. Aufgrund dieses Projekts war es möglich, die beweistheoretischen Methoden zu verschiedensten Verallgemeinerungen des Sequenzenkalküls, unter anderem zu Hypersequenzkalkülen, Kalkülen mit verschachtelten Sequenzen und Kalküle mit gekennzeichneten Sequenzen, signifikant zu erweitern. Des Weiteren konnten wir für viele Modallogiken zeigen, dass sowohl die Konstruktion von Interpolanten bei vorherigem Nachweis deren Existenz als auch der Beweis der Interpolation selbst automatisierbar ist.Betrachtet man die vielfaltigen Anwendungsbereiche von Modallogiken, die logische Beschreibung von Wissen, Zeit oder Pflicht sind nur einige wenige, tragt deren Weiterentwicklung zur optimalen Nutzung von automatisierten Verfahren in Gebieten wie den Rechtswissenschaften, der Ethik und der verteilten Systeme bei.