coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: root <root AT topoi.cam.org>
- To: "Carlos.SIMPSON" <carlos AT math.unice.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: Types, again
- Date: Fri, 16 Feb 2001 10:46:26 -0500
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:
-- hendrik
- Types, again, Carlos.SIMPSON
- Re: Types, again, root
Archive powered by MhonArc 2.6.16.