4

It seems that the cut elimination theorem of Sequent Calculus has some interesting consequences.

Quote from Alain Lecompte, La logique linéaire et la question des fondements des lois logiques (French) :

Notons alors que la propriété d’élimination des coupures, pour un tel système, a une portée philosophique non négligeable. Elle signifie qu’il peut y exister des règles dont la présence est en quelque sorte immanente : il ne s’agit pas de règle que l’on “rajoute” de l’extérieur, ni même de règle qui “se déduise” d’autres règles

He's saying that the cut elimination property imply the existence of immanent rules : they're not external rules we add or rules we can infer from other rules.

He also said (from the same text) :

La redondance de la règle de coupure est d’une autre nature. Elle est de l’ordre de l’implicite du système de règles global privé d’elle. En la formulant dans le système, on ne fait que l’expliciter.

That is : The cut rule is implicit for a system deprived of it and explicit when we formulate it as a proper rule in a proof system. J.Y Girard (Linear Logic) often use that idea.

Can someone provide an explanation for these two ideas ? As far as I understand :

1) The cut rule is essential and is the core of reasoning. The cut elimination theorem imply that we can infer anything from a proof system S without the cut rule. Therefore, some of the remaining rules also constitute the "core of reasoning".

2) Given a derivation π in a system S without the cut rule. The cut rule still exists somewhere in the reasoning but in "another form" expressed by the other rules.

Are there any other interesting implications of the cut rule of the cut elimination theorem ?

3

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 :

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.