The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Actually, Russell's paradox is constructive.

You can easily prove (A<->~A) -> False.  (The key point is that (A->~A)->~A).

From there, you can have fun proving Russell's paradox in a suitable variant of Coq. It's a bit of work, though. It's been done by Miquel. Girard's or Hurkens's paradoxes are more straightforward. Girard's paradox is actually, if I remember correctly, a variant of Burali-Forti's one, on the ordinal of all ordinals.

On 28 October 2013 16:06, J. Ian Johnson <ianj AT ccs.neu.edu> wrote:

Girard's paradox arises when you don't have predicativity.

http://plato.stanford.edu/entries/type-theory/

-Ian

----- Original Message -----
From: "t x" <txrev319 AT gmail.com>
To: "coq-club" <coq-club AT inria.fr>
Sent: Monday, October 28, 2013 11:02:52 AM GMT -05:00 US/Canada Eastern
Subject: [Coq-Club] Without law-of-excluded-middles, do we need a hierarchy of Types?


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!