# Re: no names allowed, we serve types only

Date: Wed, 24 Feb 2010 22:06:14 -0800 (PST)

Message-ID: <5819bc77-d72b-4ca6-b5d6-e31eb2ae201e_at_y7g2000prc.googlegroups.com>

On Feb 25, 9:39 am, David BL <davi..._at_iinet.net.au> wrote:

> I have doubts whether it is possible under ZFC (which disallows

*> universal sets such as a set of all sets) to formalise a tuple in such
**> a way that subtypes occur in the manner you suggest.
**>
**> If a type <a:t1, b:t2> represents all tuples that at least contains
**> the fields a and b with values of the required types, then this
**> involves a universal and won't represent a set under ZFC.
*

I'll try to provide more justification of that claim.

It is well known that the class of all sets isn't a set under ZFC. For a given x, what about the class of all sets that contain x? It turns out that this is not a set either. Here is a proof:

Suppose exists y such that for all z, x in z --> z in y.

Let R = y union {x}. This must be a set by the axiom of union.

Now x is an element of R, so R must be an element of y (because for all z, x in z --> z in y).

From R = y union {x} it follows that y is a subset of R.

R is an element of y and y is a subset of R, so R is an element of R.

R is an element of R contradicts the axiom of regularity (also called axiom of foundation). Received on Thu Feb 25 2010 - 07:06:14 CET