Talk:Cut-elimination theorem: Difference between revisions

Mathematics Start‑class Mid‑priority

This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles Start This article has been rated as Start-class on Wikipedia's content assessment scale. Mid This article has been rated as Mid-priority on the project's priority scale.

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)[reply]

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

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)[reply]

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)[reply]

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)[reply]

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)[reply]