Re: Question about Gentzen's LK system and cut elimination
From: Jamie Andrews; real address _at_ bottom of message (me_at_privacy.net)
Date: 07/22/04
- Next message: Chris Menzel: "Re: Disproof of the Halting Problem's Conclusion"
- Previous message: George Greene: "Re: Disproof of the Halting Problem's Conclusion"
- In reply to: Burning Trident: "Question about Gentzen's LK system and cut elimination"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Date: 22 Jul 2004 18:55:07 GMT
Burning Trident <see@sig.below> wrote:
> i.e. instead of first starting with a system that has a cut rule, then
> showing that the cut rule is undesirable because it does not have the sub
> formula property, and then showing that it can be done away with, why dont
> we start with a system without the cut rule?
Given a proof system, e.g. LK without cut, most people
would be likely to consider it a nice system that accords with
their intuition if it has the following property: whenever
(Gamma |- A) and (A |- Delta) are provable, (Gamma |- Delta) is
also provable. Given a proof system, if it did not have that
property, most people might think there was something a little
wrong with the proof system.
One way to prove that property is to introduce the cut rule
and then show that any proof with cut can be transformed into a
proof without cut. That's Gentzen's result.
Now, IIRC he didn't state it in this way, but more in the
way that you described above, as a way of proving consistency.
However, I think it amounts to the same thing. There are two
ways of presenting it:
(a) "Here's LK without cut. We can easily prove it consistent.
Now here's a new, intuitive rule. Look, we can eliminate
that rule, so it's still consistent even with the new rule."
(b) "Here's LK with cut. It has all the rules we would expect,
including this nice, intuitive cut rule. The only problem
with cut is that it prevents us from proving consistency
easily. But look, we can eliminate that rule, so we can
prove it's consistent."
--Jamie. (a Dover edition designed for years of use!)
andrews .uwo } Merge these two lines to obtain my e-mail address.
@csd .ca } (Unsolicited "bulk" e-mail costs everyone.)
- Next message: Chris Menzel: "Re: Disproof of the Halting Problem's Conclusion"
- Previous message: George Greene: "Re: Disproof of the Halting Problem's Conclusion"
- In reply to: Burning Trident: "Question about Gentzen's LK system and cut elimination"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Relevant Pages
|
