The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2013/10/28 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).

You are mixing set theory and type theory, but well, the problem is not there…

What do you say that you cannot prove "P ⇒ ⊥"?
Of course, you could prove it.
By definition of X, from "H: X ∈ X", you can infer that "K: (X ∈ X) ⇒ ⊥". From there, "K H" is a proof of "⊥". Conclusion: "X ∈ X ⇒ ⊥".

So excluded-middle (without extra 's', as far as I know) is not involved here.

I can also prove "P".
As I know (see previous proof) that "X ∈ X ⇒ ⊥", by definition of X, I can tell that "X ∈ X".

Conclusion: I CAN PROVE BOTH "P" and "P⇒⊥". So I can prove "⊥". Excluded-middle is excluded from proof.
 

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

Let us suppose the previous thing I wrote is wrong, and that excluded middle is mandatory for known proofs of the paradox. If Coq did not have that kind of guard against this family of inconsistencies, then that would mean that you could not add Excluded-Middle to your theory without breaking all. So you could not do classical reasoning. That would not be acceptable by many of Coq users. In intuitionistic type theory, you cannot prove excluded-middle (well assuming the theory is consistant), but you cannot prove its contrary either. And we do not want to be incompatible with it. So any theory known to be contradicting excluded-middle is very unlikely to be implemented for Coq.
 

Thanks!

--
.../Sedrikov\...