The independence statements are relative consistency statements. We construct models from an ambient model of ZFC; the construction is an interpretation and does not assume that the ambient model is transitive. Foundation is already true in the ordinary ambient membership structure, so its positive consistency direction is immediate.
For the negative direction, construct an extensional cumulative universe over Quine atoms. Let be a countably infinite set of formal symbols . Give each the extension . For a set of already constructed objects, let be its unique representative: set , and otherwise use a fresh tagged code . Atom codes have a different tag. Begin with and put
Set . The interpreted membership relation gives exactly the members , and gives exactly the member . This convention matters: creating a second representative for would violate extensionality. Every object is uniquely determined by its extension, so satisfies full extensionality. Every set-sized collection of objects has bounded construction rank, by ambient replacement, and hence has its representative in .
Here are the remaining axiom verifications. Empty set and pairing use and . If , its interpreted union is . Its interpreted power set is
since every subset extension has a unique representative. The pure, atom-free finite hierarchy supplies a copy of and an inductive set. For separation, translate an -formula into the ambient language, with quantifiers restricted to the definable class ; ambient separation gives the appropriate subset of , and represents it. For replacement, uniqueness in the interpreted functional relation gives an ambient definable functional image of the set . Ambient replacement makes that image set-sized, and again represents it. These arguments also establish that all the operations used have bounded construction rank.
Ambient choice gives choice in : choose a member from each nonempty extension in a set-sized family and represent the graph, using interpreted ordered pairs. But , and the nonempty set with extension has no -minimal member. Thus
Together with the ordinary model, this proves independence of foundation from the other ZF axioms, even when choice is retained.
To extend the construction to failure of choice, let the full permutation group of act on by
The singleton convention is equivariant, so this is an automorphism of . An object has finite support if some finite has the property that every permutation fixing pointwise fixes the object. Retain objects all of whose membership descendants have finite support, stopping the hereditary recursion at the atomic self-loops. This gives the hereditarily finite-supported Quine-atom model ; each belongs to it, with support .
Extensionality persists because every retained object's members are retained. Empty set, pairing, infinity and union preserve hereditary finite support. For separation on a retained set , the union of finite supports for and the formula's parameters supports the separated extension: permutations fixing those supports preserve satisfaction in . All its members are retained, so its representative is retained. For replacement, the same support fixes the functional range, because an automorphism must take the unique output at an input to the unique output at its transported input. Ambient replacement bounds that range; all its members are in , so its representative belongs to . Finally, the collection of all retained subset representatives of is an ambient set, contained in the full interpreted power set of . A support of permutes this collection onto itself, and its members are retained. Its representative is therefore the internal power set in . This verifies every ZF axiom except foundation; foundation still fails at each .
The atom set and the family of its two-element subsets have empty support and are retained. Suppose a choice function on were retained, with finite support . Choose distinct outside and transpose them. The transposition fixes and fixes the unordered pair , but moves whichever of its two members selects. Equivariance would require that selected member to be fixed, a contradiction. Hence
The full universe gives the corresponding positive-choice model. Choice is therefore independent of ZF without foundation. Unlike a permutation model with ordinary urelements, this model retains full pure-set extensionality: the atomic objects are self-membered sets, not empty objects exempted from extensionality.
The constructible-universe interpretation gives . Thus the consistency assumptions in both displayed conclusions can equivalently be taken to be ; no additional consistency strength is being used.

Articles by others on the same topic (0)

There are currently no matching articles.