2 added 247 characters in body
source | link

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 :

A "gentle" introduction to this topic can be found in Ch.6 Proof Complexity of :

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 :

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 :

A "gentle" introduction to this topic can be found in Ch.6 Proof Complexity of :

1
source | link

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 :