Ein beweistheoretischer Rahmen, in dem Inferenzregeln in beliebiger Tiefe innerhalb logischer Ausdrücke angewandt werden dürfen, statt nur an der Wurzel; Tiefeninferenz ermöglicht symmetrische, lokale und häufig kompaktere Beweissysteme wie den Calculus of Structures.

Prinzip

Regelanwendung innerhalb beliebiger Teilformeln zulassen: Inferenzkontexte sind nicht auf die oberste Ebene beschränkt, was lokale Umformungen ermöglicht, die Beweisstrukturen komprimieren oder symmetrieren, sofern Metaeigenschaften (Soundness, Cut-Elimination) durch geeignete Regelgestaltung und strukturelle Kontrollen gewahrt bleiben.

Demonstration

In einem Tiefeninferenzsystem für die propositionale Logik kann eine Regel, die A∨(B∧C) durch (A∨B)∧(A∨C) ersetzt, innerhalb größerer Kontexte angewandt werden, also direkt in einer verschachtelten Teilformel X[…] umschreiben, ohne sie an die Oberfläche zu heben; diese Lokalität kann kürzere Ableitungen als sequentielle Systeme liefern.

Fehlanwendung

Das gedankenlose Zulassen beliebiger innerer Umschreibungen ohne Beschränkungen kann Termination oder Korrektheit zerstören (schleifenbildende Ableitungen oder das Herleiten ungültiger Sequenzen); unbeschränkte tiefe Regeln in Systemen mit komplexem strukturellem Verhalten können Nicht-Konfluenz oder nicht eliminierbare Cuts erzeugen.

Konsequenz

Tiefeninferenz führt oft zu kürzeren, symmetrischeren Beweisen, unterstützt feingranulare Lokalität, die parallelisierbar ist, und ermöglicht uniforme Systeme für klassische und nichtklassische Logiken, die sich schwer kompakt in sequentiellen Darstellungen fassen lassen.

Umkehrung

Das Gegenteil ist flache Inferenz (traditionelle Sequenten- oder Natürlichkeitskalküle), bei der Regeln nur auf der äußersten Ebene wirken; flache Systeme bieten eine klare operationale Lesart und etablierte Normalisierungsstrategien, produzieren aber längere, stärker sequenzielle Beweise.

Abgrenzung

Gilt dort, wo logische Konnektive und Strukturregeln lokale innere Umschreibungen zulassen und wo man meta-theoretische Kontrollen durchsetzen kann; es ist kein Allheilmittel—einige Systeme erfordern zusätzliche strukturelle Beschränkungen oder ein Beschriftungsapparat, um Eigenschaften wie Cut-Elimination und Entscheidbarkeit wiederherzustellen.

Semantische Spannung

Spannung zwischen Tiefen- und flachen Inferenzkalkülen: Tiefeninferenz betont Lokalität und Symmetrie auf Kosten komplizierterer Meta-Theorie, während Sequentenkalküle modulare Regelzusammensetzung und einfachere Normalisierungsbeweise bevorzugen; sie tauschen Beweislänge, Klarheit und proof-theoretische Kontrolle gegeneinander aus.

Synthese

Tiefeninferenz verallgemeinert Ort und Modus der Regelanwendung innerhalb von Formeln: durch Zulassen lokaler, tiefer Umschreibungen entstehen kompakte, symmetrische Beweissysteme, die Parallelität und Modularität freilegen, jedoch sorgfältige Regelgestaltung und strukturelle Beschränkungen zur Sicherung von Korrektheit und Normalisierung erfordern.