Talk:Cut-elimination theorem
From Wikipedia, the free encyclopedia
 |
|||||||||||||||||||||||
| Mathematics rating: | Stub Class | Mid Priority | Field: Foundations, logic, and set theory | ||||||||||||||||||||
|
|||||||||||||||||||||||
[edit] 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
[edit] 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)
[edit] 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)
