Cohen symmetric choiceless ZF models

[David Libert]

I am writing this article giving some further background about Cohen
symmetric choiceless ZF models and related issues. This was the method
used in my post last week in "cardinality of the set of reals" to
construct a model with an amorphous set of coubtable sets of reals,
thereby producing a ZF model with more countable sets of reals than
countable sequences of reals (!) .

Paul Cohen invented the method fo these symmetric models, at around
the time he invented forcing (1963) . This method of symmetric models
uses forcing, but it also adds other methods involving symmetry that do
not appear in the basic version of forcing. Forcing over a ZFC model
produces another ZFC model. Symmetric models constructed over a ZFC
model produce a ZF + ~AC model. It is the symmetry part that loses
AC.

This symmetry aspect of Cohen's construction is itself very similar to
another similar construction, namely Fraenkel Mostowski permutation
models. You could say that what Cohen did in making symmetric models
was made a hybrid of his own basic forcing technique for ZFC models and
FM permutation models.

So I will first discuss something of FM permutation models, because
they are easier to understand than Cohen's symmetric models. Even once
we later have Cohen's symmetric models in place, it is useful to keep FM
models in mind as a continuing motivator. There is even a transfer
theorem of Jech & Sochar relating the two types of models.

So FM models were a first stab at making choiceless models of set
theory. Fraenkel proposed an approach in the 1920's and Mostowski
developed in the 1930's. As I recall, in 1908 Zermelo published the
axioms of Zermelo theory: that is ZFC without the axiom of replacement.
Maybe it was around 1918 that Skolem made a first version of replacement
and around 1922 (?) that Fraenkel formulated the axiom of replacement
as we know it today: so the final form of ZFC only emerged sometime
around the early 1920's. So FM models emerged relatively early. Then
the step from FM models to Cohen symmetric models took from the 1930's
to 1963, a much bigger gap than ZFC to FM models. All along the lines
of my comments FM models easier to understand.

The problem is, FM models don't construct true ZF models. The first
construction of true ZF + ~AC models was Cohen's symmetric models in
1963. FM models instead are for variants of ZF, which in one view may
be a small change but for the techniques of contruction the changes are
crucial, allowing a toe-hold to get the FM process started. Later
seeing how to avoid depending on these variants and returning to ZF took
all those decades and was part of a body of work that won the Field's
Medal. So the difference between the original FM variant and true ZF
is a small difference that made all the difference.

The early practioners realized they weren't getting true ZF models,
but they didn't know how to do that and for these variants they could
make working techniques and the variants are similar to the real ZF
case.

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.

FM permutation methods will be how to start with a ZFCU model, and cut
it back to a submodel (same E membership relation and same atoms, fewer
sets), namely the FM model, satisfying ZFU + ~AC + various statements
produced by the exact definition of the specific FM model.

So this shows consistency of statements over ZFU, which isn't quite
the same thing as consistency over ZF but if it is all you know how to
do is still of interest.

Given a starting ZFCU model M, it is not so easy to see how to leave
things off it to make a submodel N satisfying ZFU. Want a ZFU model
with no well-ordering of some set s ? So just leave out all the
well-orderings of s. But the N you make is supposed to be a model of
ZFU, so whatever you started off putting in N, you better close it off
by all the operations of ZFU. But ZFU includes most of the power of
conventional mathematics. There are infinitely many operations to close
off under, having powerful definitions encompassing lots of conventional
math. How do you know the stuff you deliberately left out doesn't sneak
back in under these closure operations? Knowing that from first
principles almost means knowing what you wanted to prove as consistency:
that ZFU can't define a well-ordering of s.

So the FM models will give a uniform criterion for cutting back M to
N, that can be checked to verify that well-ordering of s or whatever
really were left out of N.

There remains the problem of seeing those things meeting the criteria
still make a ZFU model. That is not so easy in general: even numbers
is a uniform criterion to cut back a PA model, but the even numbers
don't satisfy PA.

The FM method will use a cut back always of a certain general form,
and this form will guarantee that the resulting N satisifies ZFU. This
is a general technique, so to apply it in a specific case you make a
specific example of that general style, and arrange the details so the
end result N will satisfy the properties you wanted.

Namely the general method of FM cutback will be heridiatary invariance
with respect to certain permutations. So you will arrange in specific
cases that things you wanted to exclude from N are not suitably
invariant. On the other hand, the regular operations of ZFU will
preserve invariance, the normal set building axioms of ZFU applied to
hereditarily invariant input will produce heritarily invariant output,
so you have the desired closure of N, and hence N satisfies ZFU.

Namely the permutations in question will permute the atoms among
themselves. Since these atoms have no members below they can be
premuted without violating any relations below. So the FM model has a
permutation group, acting on the atoms. This group action can be lifted
up the levels of the cumulative hierarchy by transfinite induction.
Sets of atoms are permutated to their range under the permutation acting
on the atoms. Similarly higher hierachy levels are permuted by taking
ranges of the lower level members under the permutation. In this
process pure sets never move. The resulting action of permutations on
the M model of ZFCU is an automorphism of that model, ie E is respected
by the permutation action. We lifted the action up the cumulative
hierarchy levels in exactly the way to make this respecting of E true.

So we have a group acting on M. Now we need an invariance notion of
this action, to be our criterion to cut back from M to N.

The most obvious invariance notion would be total invariance: those
objects (atoms or sets) fixed by every permutation of the group.

This does not work well though and to my knowledge has never been used
in an example. Namely a typical application of these methods would have
every atom is moved by some permutation. Ie for all atoms there exists
a permutation moving the atom. So this method would already throw all
atoms out of N.

FM models actually include all the atoms in N. So atoms individually
should be allowed, but sets depending on lots of simultaneous special
relations with many different atoms should be excluded.

So this is along the lines: N members can depend on one atom, but
they can't depend on too many atoms simultaneously.

So we are led to the notion of support, reminscent of Galois theory.
For o and object in M, a support set for o is a set of atoms A
s.t. for all permutations p in the group, if p fixes every member of A
then p fixes o. So for any atom a, {a} is a support set for a. On
the other hand, for any set s in M, the set of all atoms in M is a
support set for s.

So the FM model will specify a group of permutations and its action
on atoms (and hence definable its action on all of M), and it will
specify a collection of accepted support sets. The invariance notion is
having a support set among the accepted ones.

To get all atoms in N, it is sufficient that all singleton support
sets are acceptable. On the other hand, if the set of all atoms is
acceptable, then everything in M is invariant, so N = M, so in this case
N satisified AC after all and we got nothing new, so no one ever uses
a model where the set of all atoms is accepted :-P .

So an FM model specifies the starting M with its atoms, the group and
its action and the "support": which support sets are accepted. You
vary these parameters to make different N 's.

Well a few more points. The support notion should always be closed
under finite union. If you have several N members, and want to do a
ZFU definable operation on them, in general the output will have support
the union of the support of the inputs. That union will always work as
a support set. Sometimes proper subsets of it will also work, but why
press your luck. To prove that every ZFU operation on every tuple of
inputs stays in N, the usual thing is to rely on closure of support by
union. And if you have that that gets the basics: separation,
replacement, pairing etc.

There is one particular support notion that is the most commonly
used. Finite support. The accepted support sets are exactly the finite
sets of atoms. This is closed under union and always produces a ZFU
model.

The arguments I am most used to along these lines use finite support,
and all the fine-tuning and structure to make the specific example is in
the definition of the atoms and the group action.

So in these early days they got ZFU models with amorphous sets (as
defined in my previous post) and related things (these actually
consequences of amorphous) sets that can't be linearly ordered or
well-ordered, and I suppose failures of trichomy of cardinals (that
certainly is doable an FM model anyway).

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.

So that is the state of things from the 1920's until Cohen. See how
hard it is to try to extend these ideas to ZF. The whole basis of the
method is automorphisms. Godel-Bernays which has the ability to
quantify over classes and so even state the following proves: there are
no non-trivial automorphisms of the set theoretic universe. Ie as I
said above, {} can't be moved and then inductively up the levels.

ZF can't directly quantify over all automorphisms, but as a schematum
ZF similarly for each definition of a class sized map of the universe to
itself proves that definition is not defining a non-trivial
automorphism.

The FM method handles N and all the structure of the proof as specific
definitions in M. So at the outset all the tools of the FM method are
refuted in ZF.

So we jump ahead 30 years to 1963. Cohen has his method of forcing,
to construction new ZFC models from old. Cohen combines forcing with
FM, this in spite of the fact that the ZFC models Cohen is working with
admit no non-trivial automorphisms.

So suppose we have an original ZFCU model M, and we do in that an
FM model N, based on a group G acting on atoms and a support. Cohen's
method is to make an analofue of this for some ZFC (not ZFCU) model M',
and some constructed permutation model N' of ZF (not ZFU).

Cohen will take M' to be a very special form of ZFC model: namely one
constructed by Cohen's method of forcing. Specifically, in trying to
make an analogue of the FM construction of the ZFU model N, Cohen will
arrange a forcing construction of M' acted on by the same group G in
ways analogous to the original action of G on the ZFCU atoms in M.

It is meaningless to have G acting on M' the ZFC model directly (no
non-trivial automorphisms), but Cohen takes a step back and makes G act
on the construction process behind M'. Cohen then makes a support
notion for the G action on the forcing contruction, and gets a version
of heritarily invariant applying not to a model of ZFC directly but to
its construction process.

The N' the Cohen symmetric part of M' is the part of M' constructed by
the heritarily invariant part of the construction that made M'.

This defines Cohen's permutation model N'. The proof that this is a
model of ZF is similar to the proof that N was a model of ZFU, except
instead of arguing directly about sets you argue about descriptions of
sets as those appear as part of Cohen's forcing construction.

The final stage of proofs by FM methods is to show that constructed FM
ZFU models N satisfy certain statements, typically statements coded for
in the group action and support. These are typically proofs by
contradiction, using that group elements acting as automorphisms on N
preserve truth in N.

These arguments will be imitated in analysing a Cohen permutation
model N'. Where the FM argument applied group elements to N, in the
Cohen version we now apply the group elements to the construction
process behind N'. So in arguing by contradiction, we assume some
statement is true in N', but now in a step not seen in the FM version,
we use properties of Cohen's forcing to infer from truths in the final
model N' certain information about the forcig construction behind N'.
The permutations are then applied to this information about the forcing
construction. The contradictions based on permuting to get
contradictory information depend on contradictions against the basic
theory of how forcing works.

Here is another way to rephrase this. Boolean valued models is a
different treatment of essentially the same ideas behind forcing. In
this version, consider usual set theory as ranks, where each new rank
instead of being subsets of the previous rank is mapping of the previous
rank to the two element Boolean algebra. Boolean valued models is a
generalization of this, where we replace the two element Boolean algebra
by an arbitrary complete Boolean algebra.

In general, given any collapsing of the Boolean algebra to a quotient
algebra, this induces in an obvious way working up the ranks inductively
a quotienting of the Boolean valued model to a smaller Boolean valued
model based on the quotient algebra.

The ultimate quotienting of a Boolean algebra is back down to the two
element Boolean algebra. So a Boolean valued model can be quotiented
back to a regular model of set theory.

Cohen's forcing method of producing new regular models of ZFC can be
described as producing such collapses of Boolean valued models to get
regular models again. Namely Cohen's forcing corresponds to a special
sort of collapse of this form: those in which the preimage of 1 is not
just any ultrafilter, but a so-called generic ultrafilter.

Given a Boolean valued model M based on a complete Boolean algebra B,
any automorphism f : B -> B of complete Boolean algebras canonically
lifts to an automophism g : M -> M of Boolean valued models. Namely
given any automorphism g: M -> M there is a canonical map
g x g : M x M -> M x M. M a Boolean valued model over complete
Boolean algebra B has distinguished "membership map" m : M x M -> B.

Then g the listing of f is uniquely characterized by g making the
following diagram commute:

g x g
M x M ---------> M x M
| |
| |
| |
v v
f
B ----------> B

It can be shown that every g : M -> M automorphisms of Boolean
valued models arises this way from some f : B -> B. Also f the
identity induces g the identity.

From all this it follows the question of M having non-trivial
automorphisms is equivalent to B having non-trivial automorphisms. The
M' produced by Cohen's basic forcing is a regular ZFC model, in other
words a Boolean valued model with the two element Boolean algebra. The
2 element Boolean algebra has no non-trivial automorphisms, so M' also
has none.

On the other hand, the symmetric models are made from forcings with
non-trivial automorphisms, ie the group action. When these are redone
as Boolean valued models the complete Boolean algebras gave
corresponding automorphisms and group action.

So this reworking of Cohen's method uses the group action on the
orginal Boolean valued model to define and analyse the symmetric model.

This is the general comparison of proof organizations between FM
models starting from M and Cohen symmetric models starting from M'. I
will now describe this relation in more, but not complete detail.

The starting ZFCU model M for the FM construction had atoms. Cohen's
construction is to start from M', as ZFC model. The ZFC model M' is
formed in analogue to M, but what were orginally atoms in M are turned
into sets in M', by putting members below them. We saw this previously
for extending FM methods to models dropping regularity. Now though, M'
is to be a full ZFC model, including regularity, so the new structure
below to make the atoms into sets is put in as well-founded structure.

By adding this well-founded structure below atoms, and putting
distinct structure below different atoms (to make the resulting model
satisfy extensionality), we have ruined the symmetries in M and lost all
the non-trivial automorphisms and the group action.

But the point is: this new structure below the atoms to make them
sets is the structure added by forcing. So this is where all the above
about doing the symmetries in the forcing arises.

I will say some more about the nature of the symmetry arguments on the
forcing or on the Boolean valued models. Each of these versions can be
described as constructions in stages. At the outset in forcing there is
no information about the parts of the model under construction that the
forcing will fill in. By the end of the forcing construction, a ZFC
model has been produced with total information about all membership
facts in the model.

This transition from no information to total information can be
described in one presentation as proceeding in stages. A lot of the
technicalities of forcing are about how these intermediate stages relate
to the final model.

In the Boolean valued version, there is a starting Boolen valued model
which by the end of the construction is quotiented down to a 2-valued
model. This quotienting can itself be broken into stages. It can be
factored as a composition of intermediate partial quotients. There can
be many steps of such intermediate quotients, and the final ultimate
collapse is a direct limit of this system of intermediate quotients.
The special quotienting corresponding to forcing are those that admit
such intermediate quotients of a special form.

In either version, the details of the forcing construction or of the
special quotients corresponding to forcing make transfers of information
between the final result and the intermediate stages.

The first stage, in forcing no special information what's below atoms,
in Boolean valued models the most general Boolean valued model before
all collapsings, these starting stages have the least specialized
information and so the most symmetries and most automorphisms.

The final stage in either version is a rigid structure with no
automorphisms.

In general the passage through intermediate stages is losing
automorphisms along the way. As you work your way through the
intermediate stages you have to keep dealing with the group action on
smaller and smaller subgroups. By the end it is down to the one element
subgroup.

The proofs analysing the final model must derive contradictions from
assumptions about the final model. The starting stage of the
construction has the full group action but no specialized information
about the final model. The final model has total information about
itself but only a trivial part (identity element) of the group action.

It is the intermediate stages that are intermediate in both aspects
and therefore have a mixture of both aspects. It is in these that you
reflect some facts about the final model, but still have enough symmetry
to work with those facts, in imitation of FM.

The fact that these intermdiate stages do reflect part of final
information: that is because of the details of the definition of
forcing (or of generic ultrafilters in the Boolean valued models
version).

Here is an analogy that may be helpful. We have a final model M',
which when viewed in total detail it is seen the different parts of it
have detailed shapes different from each other, and so can't be mapped
to each other by automorphisms.

The begining of the construction processes of M' (ie forcing or the
starting Boolean valued model) are like blurry pictures of M', where all
the details are lost. In this blurry view it has an indistinct shape,
all the parts look the same and there are lots of automorphisms.

The passage between these two extremes is a gradual sharpening of the
picture. As our view becomes more detailed, by slow stages more and
more shape differences come into focus, so the corresponding losses of
symmetries are gradual accross stages.

If you want to know something about the final M', the first view is
too blurry to reflect useful information. The final M' view lost all
the symmetries you needed to work with. So the intermediates let you
combine non-trivial premises for contradiction with the symmetry
techniques needed to work with the definition.

I will mention a distinction between presentations of the forcing
version (as opposed to Boolean valued models) of this symmetric models
construction. This is about some of the details of how the orginal FM
group action and support gets imitated in the forcing behind M' to work
toward symmetric model N'.

Cohen had an original style of presentation, which is closer to the
orginal FM. There was a later slick version, which did the equivalent
in a shorter but more abstract description. I have encountered this
version in Jech's writeups.

This distinction only comes up in the forcing style. Boolean valued
models are themselves a slick reworking of the original Cohen in other
aspects. To get to Boolean valued models you have to first have the
original slickening above.

So Cohen's orginal basic forcing from ZFC to ZFC (backgroung now
before we return to the symmetric version for ZF) was about how to
extend a ground model M0 to a generic extension model M1. Cohen
introduced a ramified language which included terms for the members of
M1. M1 was to be what can be constructed from the objects of set theory
from M0 's elements and from something new. So the basis of the terms
in Cohen's ramified language was terms for each M0 element, and a single
term for one new set. Cohen's forcing construction was how to give
information about this new term. M1 has cross effects between these,
but those would be more complex terms built from the basics, and the
basics have only one new term beyond the M0 term.

This basic forcing model will always produce a ZFC model. The proof
that the output model has AC is based on M0 having AC, and that at the
basic level beyond M0 we only had one other term.

That is the basic forcing to get AC. The original Cohen treatment of
symmetric models, you have a larger ramified language, with a basic term
corresponding to each atom, as terms for new sets beyond M0. So many
basic terms instead of only one. And the first step of getting the
group G to act on the forcing construction is to make it act on these
terms.

In that version, G acts on these terms from the ramified language.
This is used to lift the action of G to the forcing conditions, which
are the instructions in the forcing construction for how to fill in the
new information making new sets not in M0.

Now we come to the slick reworking as found in Jech. Jech says given
such an action of the group G on the forcing conditions, consider
forming for those forcing conditions the original ZFC style basic
forcing, ie amalgamate all the new information from the forcing as being
about just one new set. So back to AC. So this is defining M1, a ZFC
extension of M0 by forcing. Then from the group action on the forcing
conditions, you can lift the action to this new ramified language for
that ZFC forcing.

This is a different ramified language than Cohen has used. Jech's
version has just one new term, which is using all the information from
the forcing. Cohen's version had many terms, but each used only a
sybset of the forcing information. So Cohen's ramified language has
extra information, about how to partition the information coming from
the forcing.

Also, the FM imititation in symmetric models must have its own version
of support from FM. Where FM specified supports as sets of atoms,
Cohen's recopied version specifies supports as sets of terms, ie the
terms corresponding to FM atoms.

In Jech's style, there are no such terms around, we only have the
forcing conditions and one special term. We want to copy over the
support information into Jech's style. How this is done is each support
set that we accepted in the Cohen version determines a subgroup of G,
namely those permutations fixing the support set. We form the set of
all such subgroups. Since the acceptable support sets are closed under
finite union, (as from FM models), the set of groups we get this way
are closed under finite intersection. We form the upward closure of
this, taking also supergroups of accepted subgroups. We end up getting
a filter in the lattice of all subgroups of G.

We already got G acting on the Jech ZFC style ramified language over
the forcing. We can rephrase our definition of invariance for the
ramified language: a term is invariant if the subgroup of all
permutations fixing it is in the filter we just constructed.

Now we come to the amazing part. Having this notion of invariance we
can form the sublanguage of the Jech style ramified language, consisting
of hereditarily invariant terms, ie terms designated by there form as
only having earlier invariant terms as members, and being themselves
invariant.

Then: this language is isomorphic to Cohen's original multi-term
ramified language.

So ie: Cohen started with a complex ramified language and a group
acting on that language and a support notion for that language. From
these Cohen definitions we can extend the group action to the forcing
conditions, and recode the support notion as a filter on the lattice of
subgroups.

Now we forget the starting Cohen complex ramified langauage, and
only retain the forcing conditions, and the group acting now on the
forcing conditions but not the Cohen ramified language, and we discard
the orginal notion of support, which applied to Cohen's ramified
language, and instead use the recoded version of support, as a filter on
the lattice of subgroups. For this coded version we don't need the
original Cohen ramified language, only the group. And if want to
realize the group as a concrete permutation group, we can use its action
on the forcing conditions now.

So we have above just recoded everything to not directly use Cohen's
original ramfied language. Then we form the new Jech ramified language,
ie the old ZFC style Cohen language with only one new term, as opposed
to the complex Cohen language we just discarded.

Then from this recoded version, we can lift the group action back to
the Jech ramified language. And we get the support notion now from the
filter in the lattice of subgroups, and we use that to define invaraince
on this Jech language. Then we can use that invaraince to get back to
an isomorphic copy of the Cohen language we just discarded.

So what this says, is where the Cohen treatment started with a complex
ramified language and a group and support for that language, and off to
the side the forcing conditions, we can instead make the basics be
the group acting on the forcing conditions, not the language, and make
the support notion be re the group, not re the language, and we can
drop the complex Cohen ramified language entirely as a primitive, and
instead just use an old style Cohen ZFC one new term ramified
language. And from all this we can recover the discarded information.

So Cohen's treatment of symmetric models required coming up with a new
version of ramified language, different from the old ZFC ramified
language. This Jech style instead only needs the old style ramified
language.

Anyway this is the reworked version of symmetric models: forcing
conditions, conventional ZFC style ramified language, group acting
originally on forcing conditions, and support notion as filter on
lattice of subgroups. That is the basic data in this version, and
everything else is derived.

Note that Boolean valued models correspond to the usual ZFC style
ramified language, so to even get to the Boolean valued version of
symmetric models requires this Jech style reworking.

So the above has been about how Cohen's construction can imitate FM
models. To some extent this can be formalized.

There is the Jech Sochar transfer theorem, about certain relations
between FM and Cohen symmetry. This theorem says suppose M0 is a
countable FM model of ZFU having a set of atoms. Suppose alpha is
an ordinal in M0. Then there is a Cohen symmetric model M1 such that
there is a map f carrying the atoms of M0 into sets in M1, s.t.
f" the atoms of M0 is a set in M1 and
taking ranks in M0 as atoms and {} are rank 0 and levels above as
usual, f is an isomorphism of the set of all rank < alpha atoms and
sets in M0 to the alpha'th level powerset iteration in M1 over the
base set f" the atoms of M0.

What this says if you have an FM model M0, and you only care about a
bounded level of ranks above atoms, you can get a corresponding ZF
Cohen symmtric model s.t. each M0 atom corresponds to an set in M1,
and just looking at the part of M0 you cared about, you can
ismorphically build the corresponding powerset hierarchy over the base
corresponding to atoms on the M1 side. This is stronger than saying the
powerset hierachy up to level alpha has a copy of sets with same
membership in M1. It is also saying up to level alpha the notion of
powerset is preserved, the set in M1 corresponding to a powerset from
M0 is what M1 also thought was a powerset.

So this really says if you only care about a bounded rank level, you
may as well assume any FM model you have is a Cohen model.

Note it is essential that alpha was an ordinal above. It is
impossible to have such an f as above mapping all M0 into M1 for
well-founded M0 and M1. For exposition assume these models are standard
on pure sets. Namely for a an atom f(a) will be a pure set in
M1. So f(a) as a pure set is in M0, and f is identity on pure sets, so
f is not injective as a and f(a) both go to f(a).

The theorem leads to certain transfer results of consistency results
over ZFU by FM methods to consistency results over ZF. Namely any
result about atoms phraseable in some bounded rank level transfers.

So for example: a set being amorphous only quantifies over its
powerset. So an amorphous set of atoms in an FM model, the set
collecting the atoms is rank 1, and we need only quantify over subsets
of that to recognize amorphous. Well we must also recongnize finiteness
etc, needing for definition quantification some type levels above.
alpha = omega should suffice. So from an FM amorphous set of atoms by
Jech Sochar ZF + there is an amorphous set is consistent.

Jech noted that after Cohen there was various work copying over old FM
results to Cohen symmetric. Many of these are direct consequences of
his transfer theorem. He noted that there has been some recent study of
further Cohen symmetry results that can't be directly done by this
transfer.

On the other hand, given statements in an FM model not of the form as
in the Jech Sochar theorem, by which I mean not equivalent to a
statement with all quantifiers relativized to some rank alpha set as in
the theorem, it is possible to have diveregences.

One example Jech gives. Consider the axiom of multiple choice: AMC:
for every family F of pairwise disjoint non-empty sets, there exists an
mu;tiple-choice set C s.t. for every f in F f ^ C is non-empty
finite.

By contrast AC in this language: AC: for every family F of pairwise
disjoint non-empty sets there is a choice function C s.t. for every f
in F, |f ^ C| = 1.

So the almost choice set reduces arbitrary choices to choices among
finite.

ZFU |- AC -> AMC just by specialization ie the choice set AC
gives works for AMC. Similarly ZF |- AC -> AMC.

There is an FM model of ZFU + AMC + ~AC .

On the other hand: ZF |- AMC -> AC. So that last FM model does not
have its result transfer. This ZF proof is not trivial : it uses
regularity.

Ie the FM model could also give for ZF- = ZF without regularity,
a ZF- + AAC + ~AC model.
--
David Libert (ah...@freenet.carleton.ca)
1. I used to be conceited but now I am perfect.
2. "So self-quoting doesn't seem so bad." -- David Libert
3. "So don't be a morron." -- Marek Drobnik bd308 rhetorical salvo IRC sig