|
|
Re: "Elementary" elements in ZFC.
Posted:
Dec 1, 2001 5:04 PM
|
|
hrubin@odds.stat.purdue.edu (Herman Rubin) writes:
> >The simplest solution is to introduce a constant for each urelement.
> >Then, for each pair of distinct constants a,b, one says ~(a=b).
>
> >You can avoid constant proliferation, however, in a couple of ways.
> >If you want a countable set of urelements (without names), you can say
> >(E x)(x is a *countable* set & (A y)(y in x -> y is an urelement)).
>
> >If you want class many, you can write
> >(A x)(x is a set & (A y)(y in x -> y is an urelement)) ->
> >(E z)(z is an urelement and ~(z in x)).
>
> >Etc. You may wish to have a look at /Vicious Circles/ (Barwise and
> >Moss) where they use a huge number of urelements. I don't recall
> >their axiom off the top of my head and my copy of the book is not
> >handy.
>
> The "canonical" method is to take a set (or class) U of
> objects in a model of set theory, and introduce a class
> of individuals labeled by them. Then the universe is
> constructed recursively by letting the level 0 objects
> be U and the empty set, and the level \alpha objects are
> the sets of objects at lower levels not already produced.
>
> There are details missing, but this is quite general.
That sounds like a canonical method for showing that set theory with
urelements is equiconsistent with ZF (or equivalent). I was giving a
more axiomatic approach, whereas your approach should provide a model
for an axiom system like mine.
Correct me if I am mistaken here.
--
"[I]t's good for the economy to charge for intellectual property, so
open source software cannot be good, while Microsoft is the most
far-thinking company around and is doing it all for the good of the
public." -- Linus Torvalds paraphrases Microsoft VP Craig Mundie
|
|
