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 simplytyped 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 uberrusty by now).
Are you using cut elimination to try to prove strongnormalization 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 MartinLo: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 welltyped 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. 


