Re: no names allowed, we serve types only

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