Structural analysis of cut-elimination

Abstract

Die Beweistheorie - ein Teilgebiet der mathematischen Logik - betrachtet Beweise als formale Objekte und untersucht deren Eigenschaften mit Hilfe mathematischer Methoden. Der Schnitteliminationssatz - einer der wichtigsten Sätze der Beweistheorie - welcher von Gerhard Gentzen bewiesen wurde, besagt, dass die sogenannte Schnittregel ohne Weiteres aus einem formalen Beweissystem in der Art des Sequentialkalküls LK entfernt werden kann. Eine wichtige Eigenschaft schnittfreier Beweise ist die Tatsache, dass solche Beweise nur Teilformeln jener Formeln enthalten, welche bereits im zu beweisenden Satz enthalten sind (d. h. sie besitzen die sogenannte Teilformel-Eigenschaft). Betrachtet man konkrete mathematische Beweise, so entspricht die Schnittelimination dem Entfernen von Hilfssätzen (Lemmata) aus solchen Beweisen. Bei der Gentzenschen Schnitteliminationsmethode handelt es sich um eine reduktive Methode, da sie lokale Beweistransformationen an einem kleinen Teil des gesamten Beweises durchführt. Die CERES-Methode (cut-elimination by resolution) stellt hingegen einen alternativen Ansatz dar, indem sie - im Gegensatz zu reduktiven Methoden - durch die gleichzeitige Analyse aller Schnitte die globale Struktur eines Beweises berücksichtigt. Grob gesagt extrahiert CERES eine widerlegbare Klauselmenge, welche die Struktur eines Beweises mit Schnitten repräsentiert. Eine Resolutionswiderlegung ebendieser Klauselmenge dient in weiterer Folge als Skelett für einen Beweis, welcher höchstens atomare Schnitte enthält. Baaz und Leitsch konnten zeigen, dass die CERES-Methode die reduktiven Ansätze bis zu jenem Punkt simulieren kann, an dem nur noch atomare Schnitte im Beweis vorhanden sind. In der vorliegenden Arbeit wird ein neues Simulationsresultat bewiesen, welches die bisherige Simulation auf die Elimination atomarer Schnitte ausweitet. Zu diesem Zweck wird eine spezielle indizierte Resolutionsmethode definiert (ähnlich der von Bruno Woltzenlogel Paleo eingeführten "atomic cut-linkage"-Methode für sogenannte "swapped clause sets") und ihre Vollständigkeit - unter Zuhilfenahme einer neuen Klauselterm-Resolutionsmethode - für eine gewisse Klasse von charakteristischen Klauselmengen (welche durch Anwendung der CERES-Methode erhalten wurden) bewiesen. Das erzielte Hauptresultat könnte eine wichtige Rolle im Beweis der Vollständigkeit der CERES-Methode für intuitionistische Logik einnehmen. Weiters kann damit eine Teilantwort auf die von Giselle Reis ausgesprochene Vermutung gegeben werden, ob CERES in Verbindung mit indizierter Resolution und einer weiteren Methode namens "joining projections" einen intuitionistischen Beweis liefert.

Proof theory - a branch of mathematical logic - is concerned with analyzing properties of proofs mathematically by treating them as formal objects. Gerhard Gentzen proved one of the major results of proof theory - the cut-elimination theorem - which states that the so-called cut-rule can be eliminated from formal proof systems in the style of the original sequent calculus LK. An important consequence of the cut-elimination theorem is that a cut-free proof only uses subformulas of the formulas already present in the statement to be proved (i.e. they have the so-called subformula property). In the realm of concrete mathematical proofs, the elimination of cuts corresponds to the omission of lemmas. Gentzen's cut-elimination method is reductive in the sense that it performs local proof rewriting steps on small parts of a proof. The method CERES (cut-elimination by resolution) constitutes an alternative cut-elimination approach that - as opposed to reductive methods - takes the global structure of a proof into account by analyzing all cuts simultaneously. Roughly speaking, CERES extracts an unsatisfiable set of clauses that encodes the structure of a proof containing cuts. A resolution refutation of this set of clauses then serves as a skeleton for a proof containing at most atomic cuts. Due to a result by Baaz and Leitsch it is known that CERES simulates reductive cutelimination methods up to the elimination of non-atomic cuts. In this thesis, we prove a new simulation result in order to positively answer the question whether the simulation also includes the elimination of atomic cuts. To this end, we define a specific indexed resolution method (similar to the method of atomic cut-linkage for swapped clause sets by Bruno Woltzenlogel Paleo) and prove its completeness - using a new resolution method for clause terms - with respect to special characteristic clause sets obtained by CERES. The obtained result can play a crucial role in the completeness proof of CERES for intuitionistic logic and provide a partial answer to the conjecture posed by Giselle Reis whether CERES in conjunction with indexed resolution and the method of joining projections yields an intuitionistic proof.