Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

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?

share|improve this question
add comment

1 Answer 1

up vote 6 down vote accepted

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:

$$ A\simeq (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.

share|improve this answer
add comment

Your Answer

 
discard

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.