taglio, eliminazione del

taglio, eliminazione del

taglio, eliminazione del in logica, e in particolare nel calcolo dei → sequenti, possibilità di non utilizzare la regola del taglio (→ taglio, regola del) in una dimostrazione. Il teorema di eliminazione del taglio infatti stabilisce che è possibile associare a ogni deduzione di un sequente Γ ⊦ Δ una deduzione dello stesso sequente in cui non si faccia uso di tale regola, rendendo così le deduzioni del calcolo dei sequenti assimilabili a procedure algoritmiche e stabilendo un legame fra la teoria della dimostrazione e l’informatica teorica (→ Curry-Howard, isomorfismo di).