Talk:Cut-elimination theorem

Neil Leslie's complaint

This page is very confused; for example there is not a sequent calculus there are very many, and there isn't a cut-elimination theorem there are very many, and of course one can frame the theorem as "every derivation can be replaced by a derivation with the same endsequent in which CUT does not occur", or as "the system is closed under the additon of CUT" depending on whether you want to think of cuts as eliminable or admissible. Someone should re-do this page. In the meantime have a look at Goran Sundholm article on Systems of Deduction in the Handbook of Philosophical Logic. He doesn't spend that much time on cut elimination, but the article is generally excellent.

There is no doubt the article could be much improved, but I'm a bit surprised by the first part of this criticism: the article talks about three different systems. There is room for disagreement over whether there are many sequent calculi: one can say there are many proof systems formulated in the sequent calculus; calculus here would mean certain conventions about how you formulate a proof system. I've an idea this point has been discussed elsewhere on wikipedia, but I forget the outcome, and I don't recall where.

Admissibility of cut is the formulation of the CE theorem I by far hear most, but it is worth putting both formulations. Why not add it yourself? --- Charles Stewart 02:46, 6 October 2005 (UTC)

One reason for not changing it is that it seems to me to suffer from having been edited by lots of people (Yes, I know that's the whole point of a Wiki). I don't want to add to the confusion by adding yet another patch. There just seems to be a lack of consistency about the page. For example there are two mentions of the subformula property (one implict) which are not really in harmony with each other. A more careful edit is required than the one I would do just now :-) Neil

Similarity to the syllogism

The only thing I know about cut-elimination and the sequent calculus is what I just read in this article, but it seems to me that cut-elimination is very similar to the principle of syllogism: (P→Q)^(Q→R)→(P→R)

If this observation is correct, perhaps the article could mention this connection and discuss its significance. Saying that cut-elimination is analogous to the principle of syllogism early on in the article would make understanding it easier for readers who are more familiar with the first order logic, like me. -- noosphere 17:01, 15 December 2006 (UTC)

Well, yes. Cut could be called syllogism or transitivity of implication or by other names (which I do not remember). But doing so here would be misleading because this theorem applies only to the sequent calculi which are a specialized kind of logic different from those which use those other names. JRSpriggs 07:22, 16 December 2006 (UTC)

Two reasons why it is not similar to the principle of syllogism: (P→Q)^(Q→R)→(P→R):

((First: syllogism neads quantification, so P→Q)^(Q→R)→(P→R) is not a syllogism.))

Second: The Cut-elimination theorem is a theorem about the cut which is a meta-logic theorem, not a logic theorem: (P→Q)^(Q→R)→(P→R) is simply true. Cut-theorem is very complicated and not simply true. The different is, that P,Q,R are logical formulars and the cut theorem is about Sequents.--Paul Conradi 16:44, 16 December 2006 (UTC)

WikiProject class rating

This article was automatically assessed because at least one WikiProject had rated the article as stub, and the rating on other projects was brought up to Stub class. BetacommandBot 03:54, 10 November 2007 (UTC)

Tautology at syntax level

The article says "T in case of ⊢ T" is a tautology. Do you know that tautology is a semantic category whereas ⊢ operates at syntax level? At syntax level, tautology is called a theorem. Why wasn't it used? --Javalenok (talk) 01:39, 2 January 2014 (UTC)

Side remark: Is that so? I always thought "Theorem" == "True sentence given a Model" (whether syntactically derived or otherwise) and "Tautology" == "True sentence for any Interpretation"? So there are sentences that can be theorems but that are not tautologies. There is a T101 in your kitchen (talk) 04:50, 31 August 2016 (UTC)

My understanding is, a theorem is a proposition that has a proof (from a given set of axioms). (Models are not directly relevant, though for logics that satisfy Gödel's completeness theorem, you can phrase it in terms of models if you want to — the rephrasing would be, a theorem is a sentence that is true in every model satisfying the axioms.)

A sentence that is true in every interpretation is a validity, not necessarily a tautology. In logics satisfying completeness, a validity is a statement that can be proved without assuming any axioms at all (except the logical axioms, of course).

A tautology is a validity of the propositional calculus, or to put it another way, it's a sentence that can be seen to be true without considering the quantifiers. (See my remarks at talk:tautology (logic)#Tautology vs validity, which unfortunately have not yet elicited a response.)

I am not sure quite how this relates to Javalenok's criticism, because I don't quite follow his/her remarks. But in first-order logic (or any logic satisfying completeness), being a validity is the same as being provable from no axioms. If ⊢T, then T is provable from no axioms, so it's more than a theorem, it's a validity. I renew my objection to saying it's necessarily a "tautology", which ought to mean that it's provable in a much weaker framework (for example, truth tables). --Trovatore (talk) 07:04, 31 August 2016 (UTC)

Did George Boolos really talk about Cut Elimination?

We read: In his essay "Don't Eliminate Cut!" George Boolos demonstrated that there was a derivation that could be completed in a page using cut, but whose analytic proof could not be completed in the lifespan of the universe."

I have checked that paper by George Boolos and I am mightily confused. In that article he is not talking about Sequent Calculus at all (it's not even mentioned) but about Natural Deduction only. The "cut" he is talking about is the "Modus Ponens" of Natural Deducation, not the "cut" of Sequent Calculus (Why does Boolos call this "cut"? I don't know!). Indeed, the point of the paper seems to be to compare refutation proofs (whereby you add the negation of the goal to the premises and derive BOTTOM) and Natural Deduction proofs employing Modus Ponens. It seems to have nothing at all to do with the Cut-Elimination theorem.

To reformulate: In his essay "Don't Eliminate Cut!" George Boolos demonstrated that there was a derivation that could be completed in a page using Natural Deduction, but whose proof via refutation could not be completed in the lifespan of the universe."

Maybe more on this when I get the time to pore over said paper, Reading George Boolos is hard going as he takes a lot of context for granted and the reasoning is sometimes elided, as if he were entertaining a very bright student who knows what was hot at the time the paper was written. There is a T101 in your kitchen (talk) 04:50, 31 August 2016 (UTC)

Why?

If cut elimination is so useful, why have a cut rule in the first place? 31.52.252.40 (talk) 20:47, 25 April 2019 (UTC)

Strong or weak normalization?

I'm pretty sure this sentence is wrong

For proof systems based on higher-order typed lambda calculus through a Curry–Howard isomorphism, cut elimination algorithms correspond to the strong normalization property (every proof term reduces in a finite number of steps into a normal form).

If the cut-elimination property states that for any proof *there is* an equivalent cut-free proof I don't see why that would imply *strong* normalization.

In fact, I'm not even sure it implies even the weak one as it's worded, since it's not stated that the equivalent cut-free proof is found by iterated single cut eliminations, but that is more of a pedantic remark since that is the case in general. Mtzguido (talk) 19:00, 19 March 2024 (UTC)