Talk:Cut-elimination theorem

From Wikipedia, the free encyclopedia

[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