Schnitt-Eliminierung

Schnitt-Eliminierung ist Genzens Theorem, dass die Schnittregel, welche die Verwendung von Lemmata formalisiert, aus jedem Sequenzenkalkül-Beweis entfernt werden kann, wodurch ein Beweis übrig bleibt, der nur aus den Formeln besteht, die er betrifft.

Definition

Schnitt-Eliminierung ist das Theorem und das konstruktive Verfahren, das zeigt, dass jede Sequenzenkalkül-Ableitung, die die Schnittregel verwendet, in eine solche umgewandelt werden kann, die dies nicht tut, sodass jede beweisbare Sequenz einen Beweis hat, in dem nur Subformeln der Endsequenz vorkommen.

Scope

Dieses Thema behandelt die Schnittregel und ihre Rolle im Sequenzenkalkül, das Schnitt-Eliminierungsverfahren und dessen Terminierung, die Subformel-Eigenschaft schnittfreier Beweise, die daraus resultierenden Konsistenz- und Entscheidbarkeitskonsequenzen sowie die Grenzen der Beweisgröße, die die Eliminierung verursachen kann.

Core questions

• Was drückt die Schnittregel aus und warum ist ihre Entfernung bedeutsam?
• Wie terminiert das Schnitt-Eliminierungsverfahren?
• Was ist die Subformel-Eigenschaft und was impliziert sie für die Beweissuche?
• Was sind die rechnerischen Kosten der Schnitt-Eliminierung?

Key theories

Gentzen Hauptsatz

Genzens Hauptsatz besagt, dass die Schnittregel im Sequenzenkalkül zulässig ist, sodass jeder Beweis, der Schnitte verwendet, in einen schnittfreien Beweis derselben Endsequenz umgewandelt werden kann.

Subformel-Eigenschaft

Jede Formel, die in einem schnittfreien Beweis vorkommt, ist eine Subformel der Endsequenz, was die Beweisform einschränkt und Entscheidungsverfahren sowie Konsistenzargumenten zugrunde liegt.

Konsistenz durch Schnitt-Eliminierung

Da ein schnittfreier Beweis der leeren Sequenz unmöglich ist, liefert die Schnitt-Eliminierung einen direkten Beweis dafür, dass der Kalkül und somit die von ihm formalisierte Theorie konsistent ist.

Clinical relevance

Schnitt-Eliminierung ist ein grundlegendes Ergebnis mit weitreichenden Konsequenzen: Sie liefert Konsistenzbeweise, die für automatisiertes Theorembeweisen und Tableau-Methoden essentielle Subformel-Eigenschaft, Interpolationstheoreme und, durch die Korrespondenz von Beweisen als Programme, die Normalisierung typisierter Programme.

History

Gentzen bewies die Schnitt-Eliminierung, seinen Hauptsatz, 1934 für die Logik erster Stufe, und die Methode wurde zum Eckpfeiler der strukturellen Beweistheorie. Tait und Girard erweiterten die Technik auf stärkere Systeme und die Logik höherer Stufe, und die Grenzen des Wachstums der Beweisgröße unter Schnitt-Eliminierung wurden zu einem eigenständigen Studienobjekt.

Key figures

• Gerhard Gentzen
• William Tait
• Jean-Yves Girard
• Gaisi Takeuti

Seminal works

• takeuti1987
• troelstra2000
• negri2001

Frequently asked questions

Was ist ein Schnitt in einem Beweis?

Die Schnittregel erlaubt es, ein Lemma zu beweisen und es dann zu verwenden: Aus einer Ableitung, die eine Formel etabliert, und einer anderen, die diese Formel als Prämisse verwendet, wird das kombinierte Ergebnis gefolgert. Die Schnitt-Eliminierung zeigt, dass solche Zwischenlemmata prinzipiell immer entfernt werden können.

Warum kann die Eliminierung von Schnitten Beweise viel länger machen?

Das Entfernen eines Schnitts kann die Duplizierung großer Teile einer Ableitung erfordern, und die Iteration dessen kann die Beweisgröße exponentiell aufblähen. Schnittfreie Beweise sind also konzeptionell einfacher, können aber wesentlich größer sein als die ursprünglichen Beweise mit Schnitten.