Extensionality and Circular objects.
zuhair
In previous posts I had presented a strong version of Extensionality
it was the following:
For all x , y
(For all z ((z e x & ~z=x) <-> (z e y & ~z=y)) -> x=y)
However I came to realize that this is not enough.
The idea behind this axiom was allow only sets that can be identified
by the membership of other sets in it.
However that didn't capture my original intention which was actually
to cut all circular sets from existence.
A set is said to be circular iff it is a member of its transitive
closure.
This is obvious, if one say who is John and you reply that John is the
spouse of Mary and then one ask who is Mary, and the answer was Mary
is the spouse of John, then this is obviously circular and convey no
additional information as to who is John, it is actually not much
different from saying John is John.
Any definition of x by a relation to x, is a circular definition of x.
Same thing can happen with sets, take for example ZF minus
Regularity, in this theory there is nothing to shun Quine atoms from
existence, a Quine atom is a singleton that is itself like x below:
x={x}
Now this is only saying that x is the set who's sole member is x,
which is pretty circular, since x is defined by a relation of
membership to itself.
One can see with the current axiom of Extensionality, that if we drop
Regularity one can even have distinct Quine atoms, x={x} ,
y={y} were ~x=y, and this is only ridiculous.
Matters actually don't stop here, we can have circular hereditarily
singletons also.
These can be defined as:
x is a circular hereditarily singleton <->
x is singleton &
for all y ( y e TC(x) -> y is singleton ) &
x e TC(x).
so we can have:
x={{x}} and ~x={x}, I shall denote it as {{x}} for short.
also
x={{{x}}} and ~x={x} and ~x={{x}}, for short x can
be denoted as {{{x}}}
etc....
Actually a Quine atom is nothing by what i call a zero degree circular
hereditarily singleton set.
x={x} is the Zero degree circular hereditarily singleton
x={{x}} is the first degree circular hereditarily singleton
x={{{x}}} is the second degree circular hereditarily singleton
and so one for all finite ordinals...
Actually every i-th degree circular hereditarily singleton
can have a never ending amount of distinct i-th degree copies.
For example take i=1, then we can have
never ending(the size of a proper class) of sets
x={{x}}, y={{y}}, z={{z}}, ..... all are distinct from each other.
These objects cause a lot of problems actually, one of them
is that they hamper a general definition of cardinality in theories
permitting their existence.
They are essentially circular, so why allow them, and allow multiple
copies of them?
Perhaps, one can actually argue that if we allow only one copy of each
i-th degree circular hereditarily singleton, then it is OK, since
these have a property that is different from other sets, so why not
allow them, and this might be acceptable, but allowing multiple copies
of them seems ridiculous.
Therefore to Cut *all* these sets we can have the following strong
version of Extensionality to be added to ZF minus Regularity:
------------------------------------------------------------------------------------
Axiom of Strong Extensionality:
For all x , y
(For all z ((z e x & ~ x e TC(z)) <-> (z e y & ~ y e TC(z)))
-> x=y)
--------------------------------------------------------------------------------------
Or we can define "proper member" as
y is a proper member of x <-> (y e x & ~ x e TC(y)).
Then we stipulate that:
All sets are identical iff they have the same proper members.
if we denote proper membership by the symbol "e*" as below:
Define(e*): y e* x <-> (y e x & ~ x e TC(y)).
Then:
Axiom of Strong Extensionality:
For all x , y ( For all z (z e* x <-> z e* y) -> x=y )
In this way I presume that we will cut all circular sets.
To me this version of Extensionality makes sense more than the
ordinary one, which without the help of Regularity would permit all
kinds of circular sets to exist, which is not a desirable thing.
So this version of Extensionality if added to ZF minus, then we might
be able to arrive at a definition of cardinality for all sets in this
theory.
I don't know if adding the above axiom to NF would make any change as
to the stance of this theory from Choice? I don't think it make any
change though.
Zuhair
David Libert
In the parent article from which I quote below, you discuss two
strong axioms of extensioniality. There are various points of
discussion about them.
I will return to those points in a later article. For this article
I will just note one point about these definitions and collect
some related previous references.
So I will delete for this article the quotes of other points,
and just retain the statement of the axioms and a comment about
them.
zuhair (zalj...@gmail.com) writes:
> Hi all,
>
> In previous posts I had presented a strong version of Extensionality
> it was the following:
>
> For all x , y
> (For all z ((z e x & ~z=x) <-> (z e y & ~z=y)) -> x=y)
This was the first axiom.
[Deletion]
> ------------------------------------------------------------------------------------
> Axiom of Strong Extensionality:
>
> For all x , y
> (For all z ((z e x & ~ x e TC(z)) <-> (z e y & ~ y e TC(z)))
> -> x=y)
> --------------------------------------------------------------------------------------
> Or we can define "proper member" as
>
> y is a proper member of x <-> (y e x & ~ x e TC(y)).
>
> Then we stipulate that:
>
> All sets are identical iff they have the same proper members.
>
> if we denote proper membership by the symbol "e*" as below:
>
> Define(e*): y e* x <-> (y e x & ~ x e TC(y)).
>
> Then:
>
> Axiom of Strong Extensionality:
>
> For all x , y ( For all z (z e* x <-> z e* y) -> x=y )
This is the second axiom.
That second axiom is new, first presented here in that parent article.
The first axiom is old from previous threads.
Some closing comments about the new second axiom:
> In this way I presume that we will cut all circular sets.
>
> To me this version of Extensionality makes sense more than the
> ordinary one, which without the help of Regularity would permit all
> kinds of circular sets to exist, which is not a desirable thing.
>
> So this version of Extensionality if added to ZF minus, then we might
> be able to arrive at a definition of cardinality for all sets in this
> theory.
>
> I don't know if adding the above axiom to NF would make any change as
> to the stance of this theory from Choice? I don't think it make any
> change though.
>
> Zuhair
Just as a related reference, an old post where you previously
stated the first axiom above:
[1] Zuhair "Another definition of Cardinality:"
sci.logic, sci.math Dec 8, 2009
http://groups.google.com/group/sci.logic/msg/cf6c0ccced220fb5
I think [1] was the first post presenting this first axiom.
In our discussion about that axiom in [1]'s thread, we both agreed
that if no set is a member of itself then the first axiom of
strong extensionality above is equivalent to usual extensionality.
A similar property about the new second axiom of strong extensionality:
if no set is a member of its own transitive closure, then the new
second axiom of strong extensionality is equivalent to usual
extensionality.
This second premise for all x x ~ member TC(x) implies
for all x x ~ member x.
So under the 2nd premise for all x x ~ member TC(x)
both new strong axioms of extensionality are equivalent to
the usual axiom of extensionality
As I recall I have given 4 constructions of ZF - regularity models
related to various points in these threads.
In
[2] David Libert "A new definition of Cardinality"
sci.logic, sci.math Nov 23, 2009
http://groups.google.com/group/sci.math/msg/721cb8170033cf84
I constructed a ZFC - regularity model with a proper class of
singleton towers, hence making H_(=1) a proper class.
In
[3] David Libert "Scott like trick? A question"
sci.logic, sci.math Dec 1, 2009
http://groups.google.com/group/sci.logic/msg/796730d70c793d7c
I sketched a proof outline claiming a ZF model with a set so the
sets equinumerous with it have no minimal size of their transitive
closures.
Looking back, I feel more confident of this if I can drop
regularity also and make it more like the next model to be easier
to analyse.
In
[4] David Libert "Why Define Cardinality?"
sci.logic, sci.math Dec 10, 2009
http://groups.google.com/group/sci.logic/msg/0803f45348c83967
I posted a proof outline of a claimed construction of a ZF - regularity
model in which cardinality is undefinable.
In
[5] David Libert "The General Backround of Cardinality"
sci.logic Dec 22, 2009
http://groups.google.com/group/sci.logic/msg/16dc3c6329a74e35
I wrote the [4] proof in more detail, also modifying the definition
to make the proof go through.
In
[6] David Libert "The General Backround of Cardinality"
sci.logic Dec 22, 2009
http://groups.google.com/group/sci.logic/msg/b11fcb00f55fa7ff
I wrote a variant of [5] which also had all H_(x) being sets.
All my 4 models above had for all x x ~ member TC(x).
Of course my models satisfied the usual axiom of extensionality.
So all my models satisfied both axioms of strong extensinality
above.
In particular, my last two models were claiming cardinality is
undefinable.
This would go against your speculations above about defining
cardinality over the new axioms of strong extensionality.
--
David Libert ah...@FreeNet.Carleton.CA
zuhair
> In the parent article from which I quote below, you discuss two
> strong axioms of extensioniality. There are various points of
> discussion about them.
>
> I will return to those points in a later article. For this article
> I will just note one point about these definitions and collect
> some related previous references.
>
> So I will delete for this article the quotes of other points,
> and just retain the statement of the axioms and a comment about
> them.
>
> > Hi all,
>
> > In previous posts I had presented a strong version of Extensionality
> > it was the following:
>
> > For all x , y
> > (For all z ((z e x & ~z=x) <-> (z e y & ~z=y)) -> x=y)
>
> This was the first axiom.
>
> [Deletion]
>
>
>
>
>
> > Axiom of Strong Extensionality:
>
> > For all x , y
> > (For all z ((z e x & ~ x e TC(z)) <-> (z e y & ~ y e TC(z)))
> > -> x=y)
I doubt that though. Simply you cannot have non circular singleton
towers, actually if you have strong Extensionality all such singleton
towers would be hereditarily non circular, and by then you cannot have
a proper class of them. I wrote about that in the topic "Recursive
Cardinals" which is a topic that you didn't address here. The only way
to do that is to violate strong Extensionality presented here, and by
then we'll have proper classes of every i-th degree circular
hereditarily singletons. Without violating strong Extensionality is it
very difficult to see how can we have a proper class of hereditarily
non circular singleton hereditarily singleton sets, actually we cannot
have even an uncountable set of them. I said it many times, that the
lemma that I presented under topic: Recursive Cardinals, would prevent
that. So there must be something wrong with your models.
That is a wrong statement, it should be the other way round.
Another point: in your models you mention the term "atoms" though you
never
clarified what you mean by an "atom" you never defined what is
an "atom" in your models. So I shall understand it as Ur-element
which is a blatant violation of Extensionality, so if I am correct
regarding
"atoms" in your models, then your models do violate even ordinary
Extensionality.
>
> In particular, my last two models were claiming cardinality is
> undefinable.
>
> This would go against your speculations above about defining
> cardinality over the new axioms of strong extensionality.
Well possibly you are right, though I greatly doubt it. I suspect
that all of your models violate Extensionality even the ordinary one.
>
> --
> David Libert ah...@FreeNet.Carleton.CA
zuhair
Let me elaborate on this point though, I think we need to clarify
matters here so that we don't have misunderstandings.
First, a singleton tower, or what I call a "recursive singleton" can
be defined in the following manner:
x is a singleton tower iff
x is singleton &
For all y ( y e TC(x) -> y is singleton ) &
For all y ( y e TC(x) -> ~ y e TC(y) )
So singleton towers are: hereditarily non circular singleton
hereditarily singletons.
so for example x={{{... ...}}} is a singleton tower.
Now for the sake of simplicity lets attach a natural number to each
bracket in these singleton towers, i.e. let's number the brackets in
these towers,
so let's say that x=0{1{2{... ...}}}
i.e. the bracket number sequence of x is <0,1,2,3,.....>
so the outer bracket has the number 0, the one inside it has the
number 1, and the one inside it has the number 2, etc...
Now we can see that the object y defined by the bracket sequence
<1,2,3,....>
will be inside x which is defined by the bracket sequence
<0,1,2,3,....>
So in general the singleton tower xi+1 with bracket sequence of
<i+1,i+2,i+3,....> will be the member of the singleton tower xi with
bracket sequence of <i,i+1,i+2,i+3,...>
I think this is clear, so we have xi+1 e xi for all singleton towers
defined above.
Now lets take the tower i=0 i.e x0 with bracket sequence of
<0,1,2,3,....>
Now what is the transitive closure of x0
This would be
TC(x0)= (x1,x2,x3,..........)
right!
Now obviousely TC(x0) is countable.
Now let's perform iterative singleton operations on x0, and let's use
the negative integers for that purpose, so we'll have
x(-1) = {x0} ,i.e. the bracket sequence of x(-1) is <-1,0,1,2,3,....>
x(-2) = { x(-1) } , i.e. the bracket sequence x(-2) is
<-2,-1,0,1,2,3,...>
.
.
.
(x(-i)) = {x(-i+1)} for all i=1,2,3,.....
Now how many x(-i) we have? of course
we have countably many of them, that is clear.
Now the set of all singleton towers would be
ST={...,x(-2),x(-1),x0,x1,x2,......}
Which is countable! we cannot have more than those!
Now because of the following lemma in ZF minus Regularity:
Lemma: For all x , for all y
y e TC(x) if and only if there exist a finite sequence
<x0,x1,x2,...,xn> were x0 e x and
xi+1 e xi for every i=0,1,2,...,n-1 and y=xn.
Then we cannot go up further, nor we can go down further, i.e. we
cannot have for example a singleton tower with a bracket sequence of
<0,1,2,.....,w,w+1,w+2,...> , this is forbidden by the lemma above,
also we cannot have a singleton tower with a bracket sequence of
<-w,.....,-2,-1,0,1,2,....>, or even <...,-2,-1,0,1,2,....>, all of
these cases are forbidden because of the lemma above.
Actually I don't see how we can ever have an uncountable number of
these singleton towers?!
So how do you claim that we can have a proper class of them???
In topic: Recursive Cardinals, I showed how can we construct these
cardinals, and I showed that they cannot be proper classes.
I used the above lemma, together with the fact that every power set is
bigger than its set, to show that the process of iteration of obtain x-
Recursive Cardinals (review that topic please) is EXHAUSTIVE, so we
cannot have proper classes of them, that's why they are *sets*, and I
used this to show that we CAN *define* cardinality for *every* set in
ZF-Reg.+Anti-Foundation axiom (please refer to the same topic).
I might be mistaken though, but I would like to know how can we have
an uncountable number of these singleton towers? and even more
how can we have a proper class of them? I want a proof form within
the model, and not from outside it.
Zuhair
zuhair
Sorry:
TC(x0) = {x1,x2,x3,....}
George Greene
> These objects cause a lot of problems actually, one of them
> is that they hamper a general definition of cardinality in theories
> permitting their existence.
This is NOT a problem. There is NOT a coherent definition of
cardinality EVEN in the usual case! I repeat, beth-cardinals
are basically underdetermined EVEN BY THE STRONGEST theories.
> They are essentially circular, so why allow them, and allow multiple
> copies of them?
>
> Perhaps, one can actually argue that if we allow only one copy of each
> i-th degree circular hereditarily singleton, then it is OK, since
> these have a property that is different from other sets, so why not
> allow them, and this might be acceptable, but allowing multiple copies
> of them seems ridiculous.
The only thing that seems ridiculous is attempting to dismiss
perfectly reasonable consistent theories. The main reason why
you have to "allow" this (AS IF YOU had the power or the authority!)
is that other people have already dissertated upon it.
http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdf_1&handle=euclid.rml/1081878069
e.g..
To quote this review in pertinent part,
The technicalities begin in Part III. There, Barwise and Moss
introduce
systems of equations in set theory as for example
x = {a, y}
y = {x}.
The Axiom of Anti-Foundation (AFA) states that such a system has a
unique solution (here, a set x such that x = {a, {x}} and a set y such
that y = {{a, y}}); this corresponds to Aczel's Solution Lemma. Part
III also includes a chapter on bisimulations and strong extensionality
and a chapter describing a model of ZFC- + AFA.
Part IV is devoted to elementary applications of AFA. The first
chapter
discusses the original formulation of AFA by Aczel: each graph has
a unique decoration (with atoms, this is no more precisely equivalent
to
AFA). The second chapter presents an alternative semantics for modal
logic, where Kripke structures are replaced with labeled graphs. It is
shown how to characterize some sets by the formulæ they satisfy when
these sets are considered as graphs and thus as modal structures. In
the next chapter, the notion of bisimulation is reformulated in terms
of games, and the hypergame paradox is given a more satisfying
solution
than simply stating that the hypergame does not exist. Then
Barwise and Moss show how to use AFA to solve the liar paradox. To
that end, they introduce a notion of structure whose domain is a set
of
structures, possibly including the structure itself, for a language
with
a truth predicate. Part IV ends with a chapter devoted to streams, a
classical application of AFA.
Parts V and VI present further theory and applications. Mainly
they prove the existence of least and greatest fixed points of
suitable
set theoretic operators. The coalgebras are introduced to generalize
the systems of equations of Part III.
>
> Therefore to Cut *all* these sets we can have the following strong
> version of Extensionality to be added to ZF minus Regularity:
This is still Really Sort Of Not The Point.
The point IS all the GOOD math that WAS done IN this framework.
If you were actually going to somehow rescue cardinality then it
would be worth it, but you are not even addressing the problem
inherent
in the original version of cardinality.
zuhair
> On Dec 23, 6:43 am, zuhair <zaljo...@gmail.com> wrote:
>
> > These objects cause a lot of problems actually, one of them
> > is that they hamper a general definition of cardinality in theories
> > permitting their existence.
>
> This is NOT a problem. There is NOT a coherent definition of
> cardinality EVEN in the usual case! I repeat, beth-cardinals
> are basically underdetermined EVEN BY THE STRONGEST theories.
That is simply not correct. The beth Cardinals are determined
if we assume the Generalized Continuum hypothesis.
>
> > They are essentially circular, so why allow them, and allow multiple
> > copies of them?
>
> > Perhaps, one can actually argue that if we allow only one copy of each
> > i-th degree circular hereditarily singleton, then it is OK, since
> > these have a property that is different from other sets, so why not
> > allow them, and this might be acceptable, but allowing multiple copies
> > of them seems ridiculous.
>
> The only thing that seems ridiculous is attempting to dismiss
> perfectly reasonable consistent theories. The main reason why
> you have to "allow" this (AS IF YOU had the power or the authority!)
> is that other people have already dissertated upon it.http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&i...
Well that is a different matter.
>
>
>
> > Therefore to Cut *all* these sets we can have the following strong
> > version of Extensionality to be added to ZF minus Regularity:
>
> This is still Really Sort Of Not The Point.
> The point IS all the GOOD math that WAS done IN this framework.
> If you were actually going to somehow rescue cardinality then it
> would be worth it, but you are not even addressing the problem
> inherent
> in the original version of cardinality.
Zuhair
David Libert
As last time, for this reply I will concentrate one point to answer,
and so delete other sections from the quote. I will probably reply
to this same parent article again soon, about other points.
zuhair (zalj...@gmail.com) writes:
> On Dec 23, 1:20=A0pm, ah...@FreeNet.Carleton.CA (David Libert) wrote:
[Deletion]
>> In
>>
>> [2] David Libert "A new definition of Cardinality"
>> sci.logic, sci.math Nov 23, 2009
>> http://groups.google.com/group/sci.math/msg/721cb8170033cf84
>>
>> I constructed ZFC - regularity model with a proper class of
>> singleton towers, hence making H_(=1) a proper class.
[Deletion]
>> =A0 In
>>
>> [3] David Libert "Scott like trick? A question"
>> sci.logic, sci.math Dec 1, 2009
>> http://groups.google.com/group/sci.logic/msg/796730d70c793d7c
>>
>> I sketched a proof outline claiming a ZF model =A0with a set so the
>> sets equinumerous with it have no minimal size of their transitive
>> closures.
>>
>> =A0 Looking back, I feel more confident of this if I can drop
>> regularity also and make it more like the next model to be easier
>> to analyse.
>>
>> =A0 In
>>
>> [4] David Libert "Why Define Cardinality?"
>> sci.logic, sci.math Dec 10, 2009
>> http://groups.google.com/group/sci.logic/msg/0803f45348c83967
>>
>> I posted a proof outline of a claimed construction of a ZF - regularity
>> model in which cardinality is undefinable.
>>
>> =A0 In
>>
>> [5] David Libert "The General Backround of Cardinality"
>> sci.logic Dec 22, =A02009
>> http://groups.google.com/group/sci.logic/msg/16dc3c6329a74e35
>>
>> I wrote the [4] proof in more detail, =A0also modifying the definition
>> to make the proof go through.
>>
>> =A0 In
>>
>> [6] David Libert "The General Backround of Cardinality"
>> sci.logic Dec 22, =A02009
>> http://groups.google.com/group/sci.logic/msg/b11fcb00f55fa7ff
>>
>> I wrote a variant of [5] which also had all H_(x) being sets.
Those [2] - [6] are my 4 models under discussion,
[Deletion]
> Another point: in your models you mention the term "atoms" though you
> never
> clarified what you mean by an "atom" you never defined what is
> an "atom" in your models. So I shall understand it as Ur-element
> which is a blatant violation of Extensionality, so if I am correct
> regarding
> "atoms" in your models, then your models do violate even ordinary
> Extensionality.
Above was the comment I wanted to reply to in this post, concerning
those 4 models.
Those models trace back to the general methods from an older post.
Various posts in [2] - [6] reference that older one as background,
in particular [4] does.
The older post was
[7] David Libert "Cohen symmetric choiceless ZF models"
sci.logic July 6, 2000
http://groups.google.com/group/sci.logic/msg/b4271c2585d2f1e5
It was [7] that introduced the terminolgy of atoms, which traces
forward to [2] - [6] .
[7] discussed among other things how to make ~AC models for
ZFU : ZF with Urelements.
It is from those opening parts of [7] the terminlogy of atoms
was introduced.
Later in [7], I noted that these ZFU methods could
in turn be used to build models of ZF - regularity, and specifically
~AC models.
These are the methods being used in [2] - [6]. Well as quoted
above [3] was also about the regularity case.
I will quote from [7], about how atoms arise, and how they later
are used to make sets in the ~ regularity variants:
> So the first variation of ZF amenable to FM techniques is ZFU: ZF
>with urelements (or urelementen), or to use a more prosaic word:
>atoms. These are objects which are not sets, and have no members. So
>unlike ZF, ZFU is a two sorted theory of atoms and sets. Sets can have
>atoms as members and other sets as members. Extensionality is amended
>to only hold between sets. Ie the empty set and all atoms each have the
>same members. The other ZF axioms, and AC for ZFCU, copy over as
>expected. So basically, ZFU is a well-founded cumulative hierarchy, but
>instead of tracing back to {} at the base, it traces back to {} and
>atoms at the base.
>
> ZFCU is equiconsistent with ZFC, by elementary proofs that would be
>known when FM methods were invented. In any ZFCU model, we can define
>by transfinite induction the pure sets: those cumulatively built only
>from {} and no atoms at the base. So every ZFCU model has a canonical
>definable class (the pure sets) sitting inside it and satisfying ZFC.
>
> Conversely, given a ZFC model, you could disignate certain sets s
>as having <0, s> declared as "atoms", and then define a cumulative
>hierachy above these atoms letting <1, t> represent the set t
>collected over prevous levels, defining membership <i, t> E <1, u>
>iff <i, t> member u, for i = 0 or 1, and <i, t> already in the
>hierachy (inductive definition) and u a subset of the previously
>defined stage of the hierarchy. We use the <0, > and <1, > to avoid
>problems if you used s to stand in for an atom and later you wanted to
>use it to represent a set. So in a ZFC model, you can define a proper
>class and a nonstandard E membership relation and a division betweem
>"atoms" and "sets" making a non-trivial ZFCU model: ie a model with
>actual atoms.
Later:
> Early on, they applied these methods above to another variation of
>ZF. Namely take a ZFU model like these, and arange the atoms in
>infinite descending chains, and declare these atoms are now going to be
>considered as sets after all, with membership according to these chains.
>
> Some adjustments have to be made, some sets from the cumlative
>hierachy above have to be discarded because they now coincide with the
>new fake sets. The big point is you can't permute pure well-founded
>sets, because you can't permute {} since its image under an automorphism
>must also be empty, so up the well-founded pure set levels you also
>can't permute. Atoms having no members below could be permuted by an
>automorphism. But also these new non-well-founded sets can be permuted,
>by permuting the entire descending chain at once.
>
> So they can get FM models for pure sets again, no atoms, but they have
>to drop regularity. This they did in those early days.
That is as much as I wanted to quote from [7].
That is the same outline I was using in [2] - [6].
The "atoms" terminology was a hold over from the ZFU case.
But this shows how that is a working step, toward getting back to
just sets in the end.
I can say some more about this method of making ~ regularity models
in general, and so what was in [2] - [6] .
It is hard to build models of ZF and variations. A complete constuction
can't be fully formalized as a bounded contruction in ZF, by Godel's
incompleteness theorem.
So we need to use strong assumptions like Con(ZF) to get going.
So we will begin with an assumed ZF model, and use that as a guide to
building the new ZF - regularity model.
So we want to use the original sets in the starting ZF model as a guide
to making some of the sets in the contructed ZF - regularity model.
But the starting ZF model satisfied regualrity also, which we wanted
to lose, so we shouldn't copy everything over completely faithfully.
We want to deliberately build into the constructed model something
to destroy regularity, and this won't be a straight copy of the starting
ZF model since it had reguarlarity.
So by hand we want to put in membership structure into the constructed
membership relation violating regularity. We have to create this part
ourselves, not just copy from the old ZF model since we want to make
it different from that model.
So we begin with objects to be such sets. We are going to create
the new membership E structure there, so to start these have
no inherited structure on E, a blank canvas. That's why these were
called atoms.
So we define E membership among these atoms. That was the general
method of [7] and was implemented in [2] - [6] .
And this is really the core of the proof. This is where we get
tricky and put weird stuff into E to make the whole proof work
later.
Membership E on these atoms was an explicit construction.
So we should not expect it to already be a full model of
even ZF - regularity, which is still a powerful theory.
We can't make models of this too easily, by simple explicit
definitions, as from Godel's theorem.
So the second phase is we take the E on atoms part from
the first phase, where we out in the basic structure that will
power the proof later, and bulk it out to make a full
ZF - regularity model.
This is the part where we need some mathematical power.
That's where we need to invoke the original assumed
ZF model as a guide to the extra sets to add to the
constructed model to get back a ZF - regularity model.
For this part, we don't create E by hand by explicit
simple specification. Instead we copy from the ZF model
part.
So that's why I call this phase adding sets instead
of adding atoms. Because we are copying set membership
information form the ZF model.
Unlike the first phase, where we didn't use any guide
to define E membership among atoms and just made our
own explicit definitions.
So "atoms" versus "sets" during the construction
made that distinction in the construction process.
But in the final constructed model, all those
"atoms" and "sets" become just various sets in the final
model.
So that "atoms" and "sets" terminology is like scaffolding
during building that will be removed from the final building.
So what about usual extensionality coming from this
building process?
If you didn't do things right it would be possible to
do a construction in the broad outlines above making
extensionalily fail.
But each time you do one of these constructions,
part of your job is to verifiy the specific E definition
you gave doesn't violate extrensionality.
E on atoms has an explicit definition so this can be
checked. And if it didn't work tinker with the definition,
or the definition of the atoms, to make it work. And if you
can't make it work, give up on using these methods.
I guess in [2] - [6] I was not explicit on that checking
but as I recall it was all pretty obvious all would be ok.
Anyway, if that is to be a point of dispute for a specific
such construction, it amounts to a detailed review of the
E definition on atoms.
The "set" phase after. Potentially this could introduce
extensionality counterexamples by adding "sets" with
redundant E membership to previous atoms.
But the [7] broad outline and the later [2] - [6]
anticipated this and left off such bad sets.
With that there remain no extensiionality counterexamples
between atoms and sets or among sets (since the set
info was copied from the ZF model which also satisfied
usual extensionality).
This is the broad outlines of "atoms" and "sets"
to build final sets and extensionality.
If we want to review specific constructions among
[2] - [6] for such extensionality issues that would
amount to a close examination of the technicalities
of the detailed definitions.
I won't try that this article. But this gives
the overall framework.
--
David Libert ah...@FreeNet.Carleton.CA