The Coq mailing list

[t x <txrev319 AT gmail.com>]

Definitions (in case the true meaning of a word is different from my understanding of it)

Law of excluded-middles:

  forall (P: Prop), P \/ (P -> False)

Hierarchy of Types:

  type_of(nat) = Type0

  type_of(Type0) = Type1

  type_of(Type1) = Type2

  ...

Paradox with "sets of sets":

  X = { s | s \not\in s }

In classical logic, there's the argument:

  does X \in X?

    if yes, then X \not\in X, contradiction

    if not, then X \in X, contradiction

However, in constructive logic, since we don't have the law of excluded middles, it could just be that for "P = X \in X?", we can neither prove P nor prove (P -> False).

Thus, my question: why does Coq have a hierarchy of Types?

Thanks!