this is what I'm all about...

[gusl]

Open Proofs and Open Terms: a Basis for Interactive Logic

also, I'll try to dig out my introductory letter to the FOM... where I discuss my "radical" beliefs regarding proofs, e.g. "it should not be hard to write a formal proof if you have the right tools".

A question which may be obvious to you logicians:
Show me an axiomatic system where all axioms are independent, yet some theorems have two or more proofs, which are not equivalent in a simple way (i.e. there is no simple normalization). I strong feel that there isn't such a system, but many people strongly feel otherwise (they are probably right).

Can anyone enlighten me here?

Comments

[candid.livejournal.com]

My gut instinct is that you're wrong, but I don't have any good justification for it. I'll think about it.