[ back to Tom 7 Radar ]

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! ;))
c
o
m
m
e
n
t
mike (cmu-89128.wv.cc.cmu.edu) – 09.05.03 14:49:09
booooooooooooooooooooring
c
o
m
m
e
n
t
Adam (lynx.auton.cs.cmu.edu) – 09.05.03 15:04:54
I like ponies.
c
o
m
m
e
n
t
Jeff (phd15.cs.yale.edu) – 09.05.03 16:52:24
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?
c
o
m
m
e
n
t
Tom 7 (gs82.sp.cs.cmu.edu) – 09.05.03 17:41:16
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...
c
o
m
m
e
n
t
Anonymous (yale128036076025.student.yale.edu) – 09.06.03 11:43:19
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
c
o
m
m
e
n
t
Tom 7 (h-66-167-9-120.phlapafg.covad.net) – 09.06.03 19:49:33
Yeah, if I had proof terms it would probably amount to the same thing.
p
o
s
t

a

c
o
m
m
e
n
t
[ Tom 7 Radar  •  Tom 7 on Google+  •  on Twitter  •  on Facebook ]