##  [Schnittelimination (Cut-Elimination)](/de/node/59922) 

 Definition

Die Beweistransformation, die Cut-Inferenzen (Anwendungen der Cut-Regel) aus einem sequentenkalkülartigen Beweis entfernt, um eine cutfreie Herleitung desselben Endsequents zu erzeugen, wobei die Beweisbarkeit erhalten bleibt, die Struktur und Größe des Beweises sich jedoch oft ändern.

 

 

 

 

 

 





## Prinzip

Prinzip

Inferenzen so permutieren und vereinfachen, dass jede Anwendung der Cut-Regel sukzessive eliminiert wird, indem sie durch Herleitungen ersetzt wird, die nur Unterformeln des Ziels verwenden; dies erhält die Beweisbarkeit und führt zu analytischen Beweisen mit typischerweise der Unterformeleigenschaft.

 

 

 

 

 





## Demonstration

Demonstration

Im Gentzenschen Sequentenkalkül kann ein Beweis, der einen Cut über A verwendet, transformiert werden, indem der Cut durch Herleitungen der Unterformeln von A aus den Prämissen ersetzt und diese komponiert werden, was zu einem Beweis desselben Sequents ohne Cut führt; wiederholtes Anwenden entfernt alle Cuts.

 

 

 

 

## Fehlanwendung

Fehlanwendung

Anzunehmen, Cut-Elimination erhalte die Beweislänge, die Komplexitätsklasse oder die algorithmische Durchführbarkeit im Allgemeinen; sie zu verwenden, um Entscheidbarkeit zu behaupten, wo das System noch unentscheidbare Fragmente besitzt, oder zu ignorieren, dass die Eliminierung den Beweis exponentiell aufblähen oder in manchen Systemen nicht-konstruktive Schritte einführen kann.

 

 

 

 

 





## Konsequenz

Konsequenz

Cut-Elimination liefert cutfreie Beweise mit der Unterformeleigenschaft, ermöglicht Konsistenzbeweise, Interpolationsresultate und feinere Beweisanalyse; sie impliziert, dass durch Cuts eingeführte Lemmata zulässig und nicht notwendig für die Beweisbarkeit des Systems sind.

 

 

 

 

## Umkehrung

Umkehrung

Im Gegensatz dazu steht das Zulassen von Cuts als Praxis der Lemmata-Einführung: Das Hinzufügen von Cuts kann Beweise stark verkürzen und Modularität sowie Wiederverwendbarkeit bieten; die Umkehr betont damit Beweiskompaktheit und menschengerechte Struktur statt analytischer Form.

 

 

 

 

 





## Abgrenzung

Abgrenzung

Cut-Elimination gilt in vielen strukturellen Beweissystemen wie Gentzens LK und LJ unter den Standardlogikregeln, kann jedoch in Systemen mit bestimmten nicht-standardmäßigen Regeln, Fixpunkten oder induktiven Definitionen fehlschlagen oder angepasst werden müssen; Komplexität und Termination sind gesondert zu betrachten.

 

 

 

 

 





## Semantische Spannung

Semantische Spannung

Es besteht Spannung zwischen der Eliminierung von Cuts zur Gewinnung analytischer Beweise und dem Beibehalten von Cuts zur Wahrung von Kürze und Struktur; Analytizität tauscht Kompaktheit gegen Subformel-basierte Argumentation, und praktische Beweiser fügen oft wieder Lemmata (Cuts) zur Effizienz ein.

 

 

 

 

 





## Synthese

Synthese

Cut-Elimination ist die systematische Entfernung nicht-analytischer Inferenzen aus Sequentenkalkül-Beweisen: Durch Transformation und Permutation von Regeln werden Cuts eliminiert und analytisch strukturierte Beweise erzeugt, die Subformelabhängigkeiten offenlegen, womit jedoch manchmal Größe oder konstruktiver Gehalt verändert werden.