Cut-elimination by resolution in intuitionistic logic

Abstract

Diese Arbeit behandelt die Elimination von Lemmata in konstruktiven Beweisen. Beweise werden im ituitionistischen Sequentialkalkül dargestellt, Lemmata durch Gebrauch der Schnittregel. Somit handelt diese Arbeit über Schnittelimination im intuitionistischen Sequentialkalkül. Die dafür verwendete Methode beruht auf dem Resolutionsprinzip. Warum sollten wir Lemmata überhaupt eliminieren? Der Grund dafür liegt in der Bedeutung für die Beweisanalyse. Verschiedene Beweise des selben Satzes können uns verschiedene Einsichten in den Satz selbst vermitteln. Wir verwenden den intuitionistischen Sequentialkalkül weil wir an konstruktiven Beweisen interessiert sind, welche uns im Prinzip mehr Information liefern können als nicht-konstruktive. Aus einem konstruktiver Beweis kann auch einen konkreter Algorithmus zur Lösung eines Problems gewonnen werden. Wir verwenden eine resolutions-basierte Methode inspiriert durch CERES, welches eine Schnitteliminationsmethode für die klassische Logik auf Basis des Resolutionskalküls ist. Auf bestimmten Beweistypen ist CERES der reduktiven Schnitteliminationsmethode in komplexitätstheoretischer Hinsicht überlegen. Auch die durch CERES gewonnenen Beweise können von denen durch reduktive Methoden erhaltenen verschieden sein, und daher mehr Information in der mathematischen Beweisanalyse liefern. Die Hauptaufgabe dieser Arbeit ist es eine CERES-Typ Methode für die intuitionistische Logik zu entwickeln welche die selben Vorteile bietet wie CERES in der klassischen Logik. Die CERES-Methode, so wie sie für die klassische Logik definiert ist, kann nicht einfach auf intuitionistische Kalküle übertragen werden. Das Hauptproblem kommt daher dass intuitionistische Kalküle vielfach über strukturelle Einschränkungen der Sequente definiert werden. Diese Einschränkungen werden typischerweise durch die CERES-Operationen verletzt wodurch ein nur klassischer Beweis entsteht. Aus diesem Grund muss die Methode modifiziert werden sodass sie diese Einschränkungen beachtet und ein intuitionistischer Beweis resultiert. Diese Modifikation (an den Schritten von CERES) kann auf verschiedene Weise geschehen und führt zur Entwicklung verschiedener neuer Methoden. Die erste Lösung besteht in der Anwendung zusätzlicher Inferenzen um die Regelverletzungen zu vermeiden. Dieser Ansatz stellte sich für eine Unterklasse intuitionitischer Beweise als sinnvoll heraus. Hier wird ein neuer Resolutionskalül entwickelt und die einzelnen Phasen von CERES neu definiert. Die zweite Lösung, welche für die selbe Subklasse gilt, verwendet die ursprüngliche CERES-Methode und wendet ein Postprocessing auf den resultierenden Beweis an. Der dritte Ansatz erforderte eine ausführliche Untersuchung der Regelpermutationen im Sequentialkalkül LJ für die intuitionistiche Logik. Der Ansatz beruht auf der Beobachtung, dass für gewisse Beweisformen der CERES-Beweis durch Postprocessing in einen intuitionistischen Beweis transformiert werden kann (mit Transformationen die in dieser Arbeit definiert werden). Die Regelpermutationen sind dabei nötig um die Beweise in diese Formen überzuführen, wobei interessanterweise auch inkorrekte Beweistransformationen erlaubt sind. Die Inkorrektheit entsteht dabei durch Permutation starker Quantorenregeln. Diese Inkorrektheit ist natürlich im Allgemeinen inakzeptabel, in diesem Falle aber harmlos, da gezeigt werden kann dass diese im Endbeweis wieder verschwinden. Die vierte und fünfte Methode sind nicht Methoden per se. Die vierte liefert eine neue Methode um den Endbeweis in CERES zusammen zu setzen, die fünfte ist eine Resolutionsverfeinerung welche mittels CERES die reduktive Schnitteliminationsmethode approximiert. Wir vermuten dass, durch Kombination von vier und fünf, eine vollständige Schnitteliminationsmethode für intuitionistischen Beweise von skolemisierten Sätzen entsteht. Diese Arbeit fasst die Hauptresultate in der Entwicklung einer resolutions-basierten Methode für die intuitionistische Logik zusammen. Außer den beschriebenen Methoden für Subklassen der intuitionistischen Logik beschreiben wir auch das Verhalten zwischen CERES-Operationen und der intuitionistischen Logik, und zeigen auf, wo genau die Probleme liegen. Am Ende der Arbeit wird die Vermutung definiert, dass (wie oben beschrieben) eine vollständige Methode für die intuitionistische Logik gewonnen werden kann; der Beweis davon ist Aufgabe zukünftiger Forschung.

This work is about eliminating lemmas from constructive proofs. Proofs are represented using intuitionistic sequent calculus and lemmas are cut inferences. So in the end we are actually eliminating cuts from intuitionistic sequent calculus proofs. The way we do this is via a method based on resolution. Why do we want to eliminate lemmas? Because it is important for proof analysis. Different proofs of the same theorem might give us different insights on the theorem itself. We use intuitionistic sequent calculus because we are interested in constructive proofs, which, in principle, give us more information than a non-constructive proof. A constructive proof can actually provide a concrete algorithm for solving a problem. We use a method based on resolution inspired by CERES, which is cut-elimination by resolution for classical logic. CERES can perform better than reductive cut-elimination, complexity-wise speaking, on some types of proofs. Also, the resulting proof after eliminating the cuts via CERES can be different than the ones reductive cut-elimination will yield, which means more information for mathematical proof analysis. Our main goal is to develop a CERES-like method for intuitionistic logic such that it has the same advantages as CERES for classical logic. The CERES method, as is, for classical logic cannot be straightforwardly applied to intuitionistic calculi. The main difficulty comes from the fact that intuitionistic calculi are often defined by some structural restriction on the sequent. These restrictions are bound to be violated when performing some of CERES' operations and because of this the resulting proof tends to be classical. We need to modify the method such that it accommodates these restrictions and yields intuitionistic cut-free proofs. This change can be done in many ways along the steps of CERES, and several methods were developed. Our first solution is based on the application of extra inferences to avoid the violations. This turned out to work only for a subclass of intuitionistic logic. It involves using a new resolution calculus and redefining the elements of CERES. The second solution works for the same subclass, but with the original elements of CERES and a simple post-processing of the final proof. The third approach required an extensive study of rule permutations in the sequent calculus for intuitionistic logic LJ. It is based on the observation that if the input proof is of a specific shape, the final proof can be transformed into an intuitionistic proof by an operation we define. The rule permutations are necessary to transform the input proof into this shape, and interestingly enough, some unsoundness is allowed. This unsoundness comes from the permutation of strong quantifier inferences. Usually, these are not allowed for they might generate eigenvariable violations, but in our case, we can live with the violations and guarantee that they will not occur on the final proof. The fourth and fifth methods are not methods per se. The former defines a new way to assemble the final proof in CERES and the latter is a resolution refinement that approximates CERES to reductive cut-elimination. We conjecture that, by combining these operations we obtain a cut-elimination method by resolution for intuitionistic logic (without strong quantifiers in the theorem to be proven). This thesis summarizes the main results in developing a method of cut-elimination by resolution for intuitionistic logic. Besides the methods already mentioned for sub-classes of this logic, we also discuss the relation between CERES' operations and intuitionistic logic, and pinpoint exactly where the problem lies. We finish the thesis with a conjecture that such a method is possible. The proof of which we leave as future work.