Ein Verfahren in der Beweistheorie, das einen Sequenz- (oder natürliche Deduktions-)Beweis so umformt, dass Cut‑Schlüsse (Anwendungen der ‚cut‘‑Regel) entfernt werden und ein cut‑freier Beweis mit der Unterformel‑Eigenschaft entsteht.

Prinzip

Cuts wirken als Lemmata, die eingeführt und dann zur Verkürzung von Beweisen genutzt werden können; die Cut‑Elimination ersetzt Cuts systematisch durch Ausfaltungen ihrer Herleitungen, sodass jede Formel im transformierten Beweis eine Unterformel des Endsequents ist, meist erreicht durch Reduktion eines Maßes der Cut‑Komplexität bis zur Aufhebung aller Cuts.

Demonstration

Gentzens Hauptsatz: In den Sequenzkalkülen LK (klassisch) und LJ (intuitionistisch) gibt es ein Verfahren zur Cut‑Elimination. Beispielsweise kann ein Beweis, der einen Cut auf A verwendet, transformiert werden, indem man die Ableitungen der Prämissen und der Schlussfolgerung von A zusammensetzt und Inferenzschritte permutiert und vereinfacht, bis der Cut verschwindet; dies kann jedoch die Beweislänge stark vergrößern.

Fehlanwendung

Die Annahme, Cut‑Elimination liefere stets einen kleineren oder rechnerisch einfacheren Beweis, ist falsch — die Prozedur kann zu exponentiellem oder nicht‑elementarem Beweiswachstum führen. Der naive Einsatz der Cut‑Elimination in Systemen mit Induktion oder bestimmten Fixpunktprinzipien kann fehlschlagen oder zusätzliche metatheoretische Argumente erfordern.

Konsequenz

Wo anwendbar, liefert Cut‑Elimination Konsistenzbeweise, die Unterformel‑Eigenschaft, die Entscheidbarkeits- oder Komplexitätsabschätzungen für Fragmente unterstützt, sowie eine konstruktive Interpretation von Beweisen als normalisierte Berechnungen; ferner bildet sie die Grundlage für Interpolations‑ und Konservativitätsresultate.

Umkehrung

Das Einführen von Cuts (Lemmata) in einen cut‑freien Beweis ist die Umkehr: Cuts können Beweise komprimieren und modularisieren. Die Spannung zwischen cut‑freier Analytizität und cut‑basierter Ökonomie zeigt komplementäre Rollen von Normalisierung und Beweisengineering auf.

Abgrenzung

Die Standard‑Sätze zur Cut‑Elimination gelten für wohldefinierte Sequenzkalküle oder natürliche Deduktionssysteme ohne bestimmte starke Axiome; Erweiterungen auf Systeme mit Induktion, bestimmten modalen oder Fixpunktoperatoren oder nicht‑klassischen Strukturregeln können nur partiell gelten, gestufte Methoden erfordern oder scheitern.

Semantische Spannung

Steht im Widerstreit mit der pragmatischen Nutzung von Cuts als Beweisabkürzungen: theoretische Reinheit (cut‑freie, analytische Beweise) vs praktische Kürze (Cuts zur Handhabung von Beweisen). Es besteht zudem Spannung zwischen syntaktischer Normalisierung und semantischen Modellen, in denen Cuts computationelle Effekte repräsentieren.

Synthese

Cut‑Elimination ist ein syntaktisches Normalisierungsverfahren, das nicht‑analytische Inferenzschritte durch Ausfaltungen und Permutationen der Beweisstruktur entfernt, um die Unterformel‑Eigenschaft zu erreichen; es ist zentral für metatheoretische Resultate, kann aber die Beweisgröße und die praktische Handhabbarkeit beeinträchtigen.