p
e
r
s
o
n
a
l |
A New Kind of Logic
(05 Sep 2003 at 13:10) |
| Proving admissibility of cut is a polynomial time problem: it's O(c * j * r^2), where c is the number of contexts, j the number of judgments, and r the number of rules. But you have to do all that by hand. It is a relaxing process, in a way, like programming or putting stamps on envelopes. My current progress: 675 of 1764 cases. (Of course, in practice many cases are the same or don't apply, so it goes a bit faster than you might think! ;)) |  |
|
| booooooooooooooooooooring |
| I like ponies. |
This is why I was trying to get the Twelf theorem prover to prove cut elimination for me (8 times over, actually) earlier in the summer, but unfortunately the only theorem that I got it to prove successfully was false (one of its immediate consequences: every term in the simply-typed lambda calculus is canonical). Since I don't have the patience to prove cut elimination once, let alone 8 times, I'll have to wait until the Twelf theorem prover is reimplemented, or, more likely, reimpliment it myself (which is a scary proposition in and of itself, since my h4x0r1ng 5k1llz, which were never that great to begin with, are uber-rusty by now).
Are you using cut elimination to try to prove strong-normalization of your symmetric, modal lambda calculus, or is this something else? |
Not really strong normalization (though I believe that would be true, too), but the existence of normal proofs for any provable proposition. That's an important property, I hear, for having a good Martin-Lo:f approved logic.
I have, also, many times today, thought of writing a program to do this proof for me. But now I am stuck on a case (called, amusingly, GOTO), which any such program surely would not have handled... |
Isn't that the same thing as strong normalization? Existence of a normal proof for any provable proposition = existence of a normal term for any well-typed term. This typically also gives you consistancy, since you can just add _|_ to your language and show that, since it has no normal form, and since it has no introduction rule, it must also not have a normal proof (which means it can't have a proof at all); at least that's how Gentzen did it, I hear.
Jeff |
| Yeah, if I had proof terms it would probably amount to the same thing. |
|
|
|
|