# Return to Answer

 2 added 247 characters in body edited Feb 17 '17 at 12:59 Mauro ALLEGRANZA 29.2k22 gold badges2020 silver badges6969 bronze badges Perhaps, the most relevant aspect of cut is cut-elimination. This result was firstly proved for sequent calculus by Gerhard Gentzen in 1934 under the name Hauptsatz in his Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39, 1934-35 : The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. Some very important facts are related to cut-elimination : proof without cut have the so-called sub-formula property : the formulae used in the premises are sub-formulae of those in the conclusion, and this in turn is very useful for "root-first proof search". this is also related to consistency proofs : once a system is shown to have a cut elimination theorem, it is normally immediate that the system is consistent (see also Gentzen's consistency proof). the possibility of carrying out proof search based on resolution (used e.g. in Prolog), depends upon the admissibility (i.e. eliminability) of cut. Cut-elimination is related also to normalization in Natural Deduction : normalization is the process of transforming a derivation into one in normal form, where the resulting derivation is "without detours" (but in some case, very long). From the intuitive point of view, "detours" and cuts are the formal counterparts of the use of lemma (or sub-proof) in mathematical proofs. Some useful material (at different level of "complexity") may be found in : Jean-Yves Girard, Proofs and Types, Cambridge UP (1989) Paul Taylor, Practical foundations of mathematics, Cambridge UP (1999) Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001) Katalin Bimbo, Proof Theory : Sequent Calculi and Related Formalisms, CRC (2015). A "gentle" introduction to this topic can be found in Ch.6 Proof Complexity of : Pavel Pudlak, Logical Foundations of Mathematics and Computational Complexity, Springer (2013). Perhaps, the most relevant aspect of cut is cut-elimination. This result was firstly proved for sequent calculus by Gerhard Gentzen in 1934 under the name Hauptsatz in his Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39, 1934-35 : The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. Some very important facts are related to cut-elimination : proof without cut have the so-called sub-formula property : the formulae used in the premises are sub-formulae of those in the conclusion, and this in turn is very useful for "root-first proof search". this is also related to consistency proofs : once a system is shown to have a cut elimination theorem, it is normally immediate that the system is consistent (see also Gentzen's consistency proof). the possibility of carrying out proof search based on resolution (used e.g. in Prolog), depends upon the admissibility (i.e. eliminability) of cut. Cut-elimination is related also to normalization in Natural Deduction : normalization is the process of transforming a derivation into one in normal form, where the resulting derivation is "without detours" (but in some case, very long). From the intuitive point of view, "detours" and cuts are the formal counterparts of the use of lemma (or sub-proof) in mathematical proofs. Some useful material (at different level of "complexity") may be found in : Jean-Yves Girard, Proofs and Types, Cambridge UP (1989) Paul Taylor, Practical foundations of mathematics, Cambridge UP (1999) Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001) Katalin Bimbo, Proof Theory : Sequent Calculi and Related Formalisms, CRC (2015). Perhaps, the most relevant aspect of cut is cut-elimination. This result was firstly proved for sequent calculus by Gerhard Gentzen in 1934 under the name Hauptsatz in his Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39, 1934-35 : The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. Some very important facts are related to cut-elimination : proof without cut have the so-called sub-formula property : the formulae used in the premises are sub-formulae of those in the conclusion, and this in turn is very useful for "root-first proof search". this is also related to consistency proofs : once a system is shown to have a cut elimination theorem, it is normally immediate that the system is consistent (see also Gentzen's consistency proof). the possibility of carrying out proof search based on resolution (used e.g. in Prolog), depends upon the admissibility (i.e. eliminability) of cut. Cut-elimination is related also to normalization in Natural Deduction : normalization is the process of transforming a derivation into one in normal form, where the resulting derivation is "without detours" (but in some case, very long). From the intuitive point of view, "detours" and cuts are the formal counterparts of the use of lemma (or sub-proof) in mathematical proofs. Some useful material (at different level of "complexity") may be found in : Jean-Yves Girard, Proofs and Types, Cambridge UP (1989) Paul Taylor, Practical foundations of mathematics, Cambridge UP (1999) Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001) Katalin Bimbo, Proof Theory : Sequent Calculi and Related Formalisms, CRC (2015). A "gentle" introduction to this topic can be found in Ch.6 Proof Complexity of : Pavel Pudlak, Logical Foundations of Mathematics and Computational Complexity, Springer (2013). 1 answered Feb 17 '17 at 10:28 Mauro ALLEGRANZA 29.2k22 gold badges2020 silver badges6969 bronze badges Perhaps, the most relevant aspect of cut is cut-elimination. This result was firstly proved for sequent calculus by Gerhard Gentzen in 1934 under the name Hauptsatz in his Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39, 1934-35 : The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. Some very important facts are related to cut-elimination : proof without cut have the so-called sub-formula property : the formulae used in the premises are sub-formulae of those in the conclusion, and this in turn is very useful for "root-first proof search". this is also related to consistency proofs : once a system is shown to have a cut elimination theorem, it is normally immediate that the system is consistent (see also Gentzen's consistency proof). the possibility of carrying out proof search based on resolution (used e.g. in Prolog), depends upon the admissibility (i.e. eliminability) of cut. Cut-elimination is related also to normalization in Natural Deduction : normalization is the process of transforming a derivation into one in normal form, where the resulting derivation is "without detours" (but in some case, very long). From the intuitive point of view, "detours" and cuts are the formal counterparts of the use of lemma (or sub-proof) in mathematical proofs. Some useful material (at different level of "complexity") may be found in : Jean-Yves Girard, Proofs and Types, Cambridge UP (1989) Paul Taylor, Practical foundations of mathematics, Cambridge UP (1999) Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001) Katalin Bimbo, Proof Theory : Sequent Calculi and Related Formalisms, CRC (2015).