[FOM] Inconsistent systems.

[hendrik@topoi.pooq.com]

On Sat, Sep 30, 2006 at 05:19:05PM +1200, Bill Taylor wrote:
> A brief inquiry.
> 
> In the Lucas/Penrose thread, Panu Raatikainen said:
> 
> > such distinguished logicians as Frege, Curry, Church, Quine, Rosser
> > and Martin-Lof have seriously proposed... theories that... turned out
> > to be inconsistent.
> 
> I am aware of the cases of Frege and Quine, but not the others.
> 
> Can someone please give a very brief account, just a summary,
> of the theories by the others, Curry, Church, Rosser and M-L,
> that turned out to be inconsistent?

Martin-Lof's is a constructive theory of types, with type being a type.
It has an elegant consistency proof. Unfortunately, it seems that
the proof can be formalized within the system.

The first contradiction discoverd was, I believe, Girard's paradox, 
which is an adaptation of the Burali-Forte paradox to the type theory.

Martin-Lof patched the theory by introducing a hierarch of universes, 
each a member of the next, making it much less elegant.  I still think 
back to the original inconsistent theory wistfully.  Its consistency 
proof was quite pretty, beautifully illustrated the ideas behind the 
theory, and was utterly irrelevant.

-- hendrik