[Solved]: Example of a false proposition when assuming Type : Type

ignougroup
Problem Detail: In Type Theory if one allows Type to be a member of itself, it makes the theory inconsistent. I understand it by analogy to Russel’s paradox in Set Theory, but would prefer to see it done in Type Theory. Is there a short example of the equivalent in Type Theory?

Asked By : Victor

Answered By : cody

The relevant literature is the following: Thierry Coquand A new paradox in type theory (link). He describes his paradox in a system that is somewhat weaker than 

Type : Type

But that can be easily transported to the above. The main idea is taking Reynolds proof that there are no models of system F in set theory. That proceeds by building an initial algebra of the form: $$ Asimeq (A rightarrow mathrm{2}) rightarrow mathrm{2}$$ Where $mathrm{2}$ is a set with 2 elements, and deriving a contradiction by a cardinality argument. Coquand shows

  1. You can carry out this reasoning in the above type theory
  2. There is a model of system F in that theory. This yields a contradiction.

The second article is from Antonius Hurkens, and is titled A simplification of Girard’s paradox (link). The proof involves a construction of the “type of all well-founded types”. I must admit that the general idea seems clear, but the details are quite devilish. I’m afraid there is no simple, easy to understand contradiction in $mathrm{Type} : mathrm{Type}$. However the proof-terms obtained from the contradiction are relatively tractable: only a few lines are sufficient to define them. Alexandre Miquel, in his thesis dissertation, showed that one could construct a model of naive set theory in these inconsistent type systems by using a pointed graph interpretation of sets. He can then simply apply Russel’s paradox directly. Unfortunately the model construction takes a bit of work, and the dissertation is in French.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/12929