MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 15 down vote accepted

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 formalization in Twelf.

In general, these questions are not equivalent, though they often coincide. A "reasonable" type theory will by inspection have no normal 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.

share|cite|improve this answer

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 simplification of Girard's paradox

share|cite|improve this answer
Here's a free version of the linked paper: – erdeszt Nov 2 '15 at 20:48

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.