most recent 30 from http://mathoverflow.net 2013-05-21T15:56:19Z http://mathoverflow.net/feeds/question/18089 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/18089/what-is-the-manner-of-inconsistency-of-girards-paradox-in-martin-lof-type-theory lukepalmer 2010-03-13T19:19:37Z 2010-03-13T21:40:05Z

<p>I am aware that assigning the type of Type to be Type (rather than stratifying to a hierarchy of types) leads to an inconsistency. But does this inconsistency allow the construction of a well-typed term with no normal form, or does it actually allow a proof of False? Are these two questions equivalent?</p>

http://mathoverflow.net/questions/18089/what-is-the-manner-of-inconsistency-of-girards-paradox-in-martin-lof-type-theory/18097#18097 Noam Zeilberger 2010-03-13T20:55:16Z 2010-03-13T20:55:16Z

<p>Girard's paradox constructs a non-normalizing proof of False. You could read Hurken's "A simplification of Girard's paradox", or maybe Kevin Watkin's <a href="http://www.cs.cmu.edu/~kw/research/hurkens95tlca.elf" rel="nofollow">formalization in Twelf</a>.</p> <p>In general, these questions are not equivalent, though they often coincide. A "reasonable" type theory will by inspection have no <em>normal</em> proofs of False, and so then normalization implies consistency. The inverse (non-normalization => proof of False) is much less obvious, and it is certainly possible to construct reasonable paraconsistent type theories, where non-termination is confined under a monad and does not result in a proof of False.</p>

http://mathoverflow.net/questions/18089/what-is-the-manner-of-inconsistency-of-girards-paradox-in-martin-lof-type-theory/18104#18104 Adam 2010-03-13T21:40:05Z 2010-03-13T21:40:05Z

<p>It leads to a well-typed term, having no normal form, which is assigned the type False. You can find the term given explicitly in <a href="http://dx.doi.org/10.1007/BFb0014058" rel="nofollow">A simplification of Girard's paradox</a></p>