Cut-eliminatiestelling

In de logica is de cut-eliminatiestelling (of Gentzens Hauptsatz) een centraal resultaat in de bewijstheorie, met name in de context van de sequentiële calculus, waarbij het doel is om bewijzen te vereenvoudigen die gebruik maken van de cut-regel.

Het werd oorspronkelijk bewezen door Gerhard Gentzen, in zijn artikel "Investigations in Logical Deduction" uit 1934, voor de systemen LJ en LK die respectievelijk intuïtionistische en klassieke logica formaliseren. De cut-eliminatiestelling drukt uit dat elk oordeel dat een bewijs bezit in de sequentiële analyse waarbij gebruik wordt gemaakt van de cut-regel, ook een bewijs heeft dat geen gebruik maakt van de cut-regel (een cut-vrij bewijs).

De cut-regel

Een sequent is een logische uitdrukking die meerdere formules met elkaar in verband brengt, in de vorm "$A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots$", dat gelezen moet worden als "$A_{1},A_{2},A_{3},\ldots$ bewijst $B_{1},B_{2},B_{3},\ldots$", en (zoals verduidelijkt door Gentzen) moet worden opgevat als gelijkwaardig aan de waarheidsfunctie "Als ( $A_{1}$ en $A_{2}$ en $A_{3}$ …) dan ( $B_{1}$ of $B_{2}$ of $B_{3}$ …).". Merk op dat de linkerkant (LHS) een conjunctie (en) is en de rechterkant (RHS) een disjunctie (of).

De LHS kan willekeurig veel of weinig formules hebben; wanneer de LHS leeg is, is de RHS een tautologie. In LK kan de RHS ook een willekeurig aantal formules hebben - als deze er geen heeft, is de LHS een contradictie. In LJ kan de RHS slechts één of geen formule hebben: hier zien we dat het toestaan van meer dan één formule in de RHS equivalent is, in aanwezigheid van de juiste contractieregel, met de toelaatbaarheid van de wet van de uitgesloten derde. De sequentiële calculus is echter een tamelijk expressief raamwerk, en er zijn sequentiële calculi voor de intuïtionistische logica voorgesteld die veel formules in de RHS mogelijk maken. Uit de logica LC van Jean-Yves Girard is het gemakkelijk om een relatief natuurlijke formalisering van de klassieke logica te verkrijgen, waarbij de RHS hoogstens één formule bevat; het is het samenspel van de logische en structurele regels dat hier de sleutel is.

"Cut" is een regel in de normale verklaring van de sequentiële calculus, en gelijkwaardig aan een verscheidenheid aan regels in andere bewijstheorieën, die, gegeven

1. $\Gamma \vdash A,\Delta$

en

1. $\Pi ,A\vdash \Lambda$

toelaten om de volgende conclusie te trekken

1. $\Gamma ,\Pi \vdash \Delta ,\Lambda$

Dat wil zeggen, het "knipt" de exemplaren van de formule $A$ buiten de afgeleide relatie.

Cut-eliminatie

De cut-eliminatiestelling stelt dat (voor een bepaald systeem) elke sequent die kan worden bewezen met behulp van de regel Cut, ook kan worden bewezen zonder gebruik van deze regel.

Voor sequentiële calculi die slechts één formule in de RHS hebben, luidt de regel "Cut", gegeven

1. $\Gamma \vdash A$

en

1. $\Pi ,A\vdash B$

laat dit ons toe om de volgende conclusie te trekken

1. $\Gamma ,\Pi \vdash B$

Als we $B$ als een stelling zien, dan drukt cut-eliminatie in dit geval uit dat lemma$A$ gebruikt kan worden om te bewijzen dat deze stelling ingelijnd worden. Wanneer het bewijs van de stelling lemma $A$ vermeldt, kunnen we de voorkomens vervangen door het bewijs van $A$. Bijgevolg wordt de cut-rule ook toelaatbaar genoemd.

Gevolgen van de stelling

Voor systemen die in de sequentiële calculus zijn geformuleerd, zijn analytische bewijzen de bewijzen die de Cut-regel niet gebruiken. Typisch zal een dergelijk bewijs langer zijn, en niet noodzakelijkerwijs triviaal. In zijn essay "Don't eleminate Cut!" demonstreerde George Boolos dat er een afleiding bestond die op een pagina kon worden voltooid met behulp van de Cut-regel. Het analytische bewijs ervan kan echter niet binnen de levensduur van het universum worden voltooid.

De stelling heeft vele gevolgen:

• Een systeem is inconsistent als het een bewijs van het absurde toelaat. Als het systeem een cut-eliminatiestelling heeft, dan zou het, als het een bewijs heeft van het absurde, of van de lege sequent, ook een bewijs moeten hebben van het absurde (of de lege sequent), zonder cuts. Het is doorgaans heel eenvoudig om te controleren of dergelijke bewijzen niet bestaan. Dus zodra is aangetoond dat een systeem een cut-eliminatiestelling heeft, volgt normaal gesproken hieruit onmiddellijk dat het systeem consistent is.
• Normaal gesproken heeft het systeem ook, althans in de logica van de eerste orde, de subformule-eigenschap, een belangrijke eigenschap in verschillende benaderingen van de bewijstheoretische semantiek.

Cut-eliminatie is een van de krachtigste hulpmiddelen voor het bewijzen van interpolatiestellingen. De mogelijkheid om bewijsonderzoek uit te voeren op basis van resolutie, het essentiële inzicht dat leidt tot de programmeertaal Prolog, hangt af van de toelaatbaarheid van Cut in het juiste systeem.

Voor bewijssystemen die zijn gebaseerd op getypeerde lambdacalculus van hogere orde via een Curry–Howard-isomorfisme, komen cut-eliminatie-algoritmen overeen met de sterke normalisatie-eigenschap. Deze eigenschap stelt dat elke bewijsterm in een eindig aantal stappen wordt gereduceerd tot een normaalvorm.