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

[gustavolacerda.livejournal.com]

I mean, you will have redundant axioms. The reason we can prove something both geometrically and algebraically is because the two theories are somehow related. Theorems of one theory may be interpreted into the other (quite analogous to: if a scientific theory corresponds to the real world, then its consequences will tend to as well(I say "tend" because scientific models aren't always perfect) ). This is what one of my current projects is about: categories of interpretations.

Some example, taken from my notes from yesterday:
* the Klein model of geometry is an interpretation of hyperbolic into Euclidean geometry.
* Peano Arithmetic is interpreted into ZF.
* more simply, geometry interpreted into algebra: Cartesian space (this example was not checked by an expert).

Interpretations are everywhere in mathematics.

See my next entry for links to interpretations in physics.