Interpolation by translation

Abstract

Craigs Interpolationstheorem ist ein zentrales Resultat in der klassischen Prädikatenlogik erster Stufe. In dieser Diplomarbeit betrachten wir die Möglichkeiten der Interpolation in der quantifizierten Modallogik S5. Craigs Interpolationstheorem gilt in dieser Logik nicht im Allgemeinen und wir werden uns in dieser Arbeit mit einigen Ausnahmen befassen. Zuerst beschreiben wir Gentzens Sequenzialkalkül und wichtige darauf beruhende Resultate, wie Gentzens Hauptsatz über die Schnittelimination sowie Craigs Interpolationstheorem. Wir betrachten die Verbindung zum Beth'schen Definierbarkeitstheorem, welches aus dem Interpolationstheorem folgt. Im darauf folgenden Kapitel führen wir die Modallogik S5 ein und betrachten die Möglichkeiten und Limitationen verschiedener Kalküle. Anschließend präsentieren wir den Beweis von Kit Fine, dass das Interpolationstheorem für die quantifizierte Modallogik S5 nicht gilt. Der Beweis gelingt Fine, indem er zeigt, dass das Beth'sche Theorem in S5 nicht zutrifft. Dazu gibt es jedoch Ausnahmen. Im letzten Kapitel zeigen wir, dass man für Sequenzen aus dem Fragment der pränexen Formeln sowie aus dem Fragment der Formeln mit ausschließlich schwachen Modaloperatoren sehr wohl Interpolanten finden kann. Wir finden diese Interpolanten, indem wir die Sequenzen in die klassische zweisortige Logik übersetzen, in dieser mithilfe von Craigs Interpolationstheorem die Interpolante finden, und diese schließlich in S5 zurückübersetzen.

Craig's Interpolation Theorem is a fundamental result in classical first-order logic. In this master's thesis we examine interpolation in the quantified modal logic S5. Craig's Interpolation Theorem does not generally hold in this logic, but we will examine some exceptions. First, we describe Gentzen's sequent calculus and important results such as the cut-elimination theorem and Craig's Interpolation Theorem. We explore the connection to Beth's Definability Theorem, which is implied by the Interpolation Theorem. We proceed to introduce the modal logic S5 and explore some possibilities and limitations of different calculi. Then we present Kit Fine's proof of the statement that the Interpolation Theorem does not hold in S5. Fine proceeds by showing that Beth's Definability Theorem is not valid in S5. However, there are exceptions. In the last chapter, we show that one can find the interpolant for fragments of quantified S5, namely the fragment of sequents of prenex formulas and those containing weak modal operators only. We find the interpolants for these sequents by translating them to classical two-sorted first-order logic, finding the interpolant there with Craig's Interpolation Theorem, and then translating the interpolant back to S5.