The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

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!