The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

> On Fri, Feb 16, 2001 at 03:40:18PM -0100, Carlos.SIMPSON wrote:
> > My example is missing a part which I assume exists, basically saying
> > that the statement Type : Type (without a hierarchy) is inconsistent
> > due to Russell's paradox. (Somebody should correct me if I am wrong about 
> > this).
> 
> Actually, I think you need a standard equality on types to get Russel's
> paradox from it, because X : Y is not a proposition.  It is possible to
> get the Burali-Forte paradox without the standard equality, though.
> I think the type-theoretic version of the Burali-Forte paradox
> is known as Girard's paradox.  Am I wrong on this.

  Just to mention that Russell Paradox also can be encoded in
Type:Type (actually U-) using a representation of sets as pointed
graphs (think of them as trees, or dags, representing the arborescent
structure of sets that the relationship relation induces) [this is
recent work by Alexandre Miquel -- see http://logical.inria.fr/~miquel].

                                           Hugo Herbelin