Teorema di eliminazione del taglio

Il Teorema di eliminazione del taglio (o Hauptsatz di Gentzen) è il principale risultato che mostra l'importanza del calcolo dei sequenti. Venne dimostrato originariamente da Gerhard Gentzen nel suo storico articolo "Investigations in Logical Deduction" per i sistemi LJ ed LK, in cui sono formalizzate rispettivamente la logica intuizionista e la logica classica. Il teorema di eliminazione del taglio stabilisce che ogni giudizio che possiede nel calcolo dei sequenti una dimostrazione facente uso della regola del taglio possiede anche una dimostrazione senza taglio cioè una dimostrazione che non fa uso della regola del taglio.

La regola del taglio

Un sequente è un'espressione logica che mette in relazione molte formule, nella forma "$A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots$", che deve essere letta come "$A_{1},A_{2},A_{3},\ldots$ dimostra $B_{1},B_{2},B_{3},\ldots$", e (come messo in evidenza da Gentzen) deve essere concepita come equivalente alla funzione di verità "Se ($A_{1}$ and $A_{2}$ and $A_{3}$ …) allora ($B_{1}$ or $B_{2}$ or $B_{3}$ …)." Il lato sinistro (left-hand site o LHS) è una congiunzione mentre il lato destro (right-hand site o RHS) è una disgiunzione.

Il lato sinistro può avere poche o tante formule e quando è vuoto il lato destro è una tautologia. Nella logica classica il lato destro può avere qualsiasi numero di formule; se è vuoto il lato sinistro è una contraddizione, mentre nella logica intuizionista il lato destro può avere solo una formula o nessuna: notiamo che ammettere più di una formula nel lato destro equivale, in presenza della regola di contrazione, all'ammissibilità del principio del terzo escluso.Comunque il calcolo dei sequenti è uno schema abbastanza espressivo e sono stati proposti calcoli dei sequenti per la logica intuizionista che ammettono più formule nel lato destro. Dal calcolo classico dei sequenti (LC) di Jean-Yves Girard è semplice ottenere una formulazione piuttosto naturale della logica classica dove il lato destro contiene al massimo una formula; la chiave è l'interazione della logica e delle regole strutturali.

Il "taglio" è una regola nella normale esposizione del calcolo dei sequenti, e equivalente ad una varietà di regole in altre teorie della dimostrazione che dato

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

e

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

permette di inferire

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

Cioè, "taglia" l'occorrenza della formula $A$ dalla relazione di inferenza.

Collegamenti esterni

• (EN) Eric W. Weisstein, Teorema di eliminazione del taglio, su MathWorld, Wolfram Research.