[FOM] Inconsistent systems.
hendrik at topoi.pooq.com
Sun Oct 1 17:01:28 EDT 2006
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.
More information about the FOM