this is what I'm all about...
Jan. 21st, 2004 08:31 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslOpen 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?
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?