Re: The Dedekind Snap

On Tue, 16 Dec 2008 14:41:29 -0800 (PST) MoeBlee wrote:


Note that in this case "0" is a primitive.

No, it is defined.

???


We prove: E!xAy ~yex.

Then define: 0=x <-> Ay ~yex.

Ah. Then you will not have any urelements in your theory (i.e. effectively
excluded them), you know, right. :-)

So why not just define

set x :<-> x = x

in this case?


c is a class <-> (Ex xec v c=0)

Well, no proper classes in Z (sic!) set theories! ;-)

Yes, so?

And why the 'sic'?

Because "Z" (->Zermelo) set theories only know about /sets/ (and possibly
urelements). (Hence it's not sensible to define /proper classes/ _in this
context_.)

Remember your original claim was:

"One can define 'set' in such theories as Z set theories."

With other words:

  y is a set <-> (Ex xey v y=0)


Now from your theorem above:

E!xAy ~yex

and the definition

0=x <-> Ay ~yex

We get the theorem:

Ax(set x).

Well great. That's why I propose the definition

set x :<-> x = x

in this case. Then we still get the theorem

Ax(set x).

On the other hand, if you intend that your theory allows for urelements,
and you want to use the definition

y is a set <-> (Ex xey v y=0) ,

"0" "most probably" is a primitive of your system. (Just what I claimed.)

Anyway:

A very reasonable definition imho: Something is a set if it has some
elements,  o r  (otherwise) is the empty set (sic!).



Herb

.