Philosophical interpretation of the cut rule of Sequent Calculus

Question

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 ?

Answer 1

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).

Answer 2

Mauros answer is excellent, I only wish to add an exposition for the two quotes as requested.

The latter quote admits a fairly easy interpretation. Systems deprived of cut often admit cut as a metatheorem. (logical systems without cut are very difficult to actually work in, see Boolos 1984 for why). For example, ND typically does not have cut as an explicit rule. Rather cut is implicit (as are many of the other structural rules). This holds for various sequent calculi as well.

The first quote is along the lines of the second (although someone better versed in logic or french may perhaps correct me). Cut elimination property implies that cut is an immanent rule. This fits with the given english translation- an immanent rule is not inferable from other rules, and cut is not derivable from the other rules. This is easy to see- no non structural rule makes formulae disappear in the sequent calculus. As for external rule, presumably Lecompte means something along the lines of a metatheorem or non logical axiom.