Forcing constructs new first-order models while controlling which ground-model properties survive. Fix a ground model and a partially ordered set , writing when is the stronger condition. A generic filter is upward closed, directed towards stronger conditions, and meets every ground-model dense subset of a forcing order. If is externally a countable transitive model, enumerate its dense subsets and successively choose stronger conditions in them. The resulting filter is -generic. External countability is crucial: this is not a claim that the ground model regards its own universe as countable.
A forcing name is built recursively from pairs of earlier names and conditions. For a generic filter , its evaluation of a forcing name is
The canonical forcing name evaluates to , so . Recursive evaluation also proves transitivity. Name ranks bound the ranks of their evaluations, so an ordinal in the extension is below some ground ordinal and is already a ground ordinal. Thus forcing preserves ordinals.
The central link between syntax and generic interpretation is the forcing theorem. The relation is definable in the ground model, and the forcing truth lemma says
For an atomic membership assertion, densely many refinements must witness equality with a member-name whose associated condition is compatible with the refinement. Equality is obtained by recursive mutual inclusion of names. For negation, means no stronger condition forces ; for an existential quantification, witnesses must be obtainable densely below . Induction on name rank establishes the atomic clauses, and induction on formulas establishes definability and the truth lemma. The generic filter meets the relevant dense sets at the existential step. An arbitrary semantic assertion about one chosen generic filter is insufficient: the definable relation must work uniformly for all generic interpretations.
This explains preservation of ZFC. Extensionality and foundation follow from transitivity; canonical names supply infinity. Pair and union names give pairing and union. For separation, restrict a name's members to conditions forcing the defining formula. For replacement, the definable forcing relation lets ground axiom schema of collection bound a set of names for all possible witnesses to the unique outputs; evaluating their collected name gives the range. For power set, let name the given set and let be the set of its member-names. Every subset of has an equivalent name drawn from , by the truth lemma, so a ground set of candidate names collects all its subsets. Finally choose a ground well-order of the relevant names; its evaluated image surjects onto the desired set, and choosing the first name for each value well-orders that set. This is why ordinary forcing over a choice model preserves choice.
For a concrete example, Cohen forcing consists of finite partial functions , ordered by extension. The generic union is total because deciding each coordinate is dense. For every ground real , the set of conditions disagreeing with somewhere is dense, so . This construction changes the universe by adding a genuinely new real without changing its ordinals.
The size and compatibility of conditions determine what else changes. With the countable chain condition for forcing, an ordinal-valued name has only countably many possible values at each coordinate: take a maximal antichain deciding that value. Therefore the possible range of a name for a map with infinite ground domain of cardinality lies in a ground set of size at most . This prevents cardinal collapse and changes of uncountable regular cofinalities. Forcing by finite partial functions is ccc: the delta-system lemma thins any uncountable family of finite domains to a delta-system, and a further thinning makes their values agree on its finite root. Two remaining conditions are compatible. Distinct coordinates add distinct reals.
For example, start with GCH and take . This forcing has size and adds distinct reals. A nice name for a real uses countably many antichains, and each antichain is countable. The ground arithmetic bounds the number of such names by . Hence
giving a relative-consistency example of the failure of CH. The ground choice of GCH is available through the constructible universe; no claim that every starting model has this arithmetic is needed.
By contrast, countably closed forcing adds no new countable sequences of ground ordinals. Given a name, recursively strengthen a condition to decide each coordinate, then take a lower bound of the descending sequence. That condition decides the entire sequence. Closure and chain conditions thus control different features; neither should be silently substituted for the other.
Further applications include changing cofinalities, adding branches through trees, and constructing prescribed continuum patterns. If the aim is to violate choice, an ordinary generic extension of a choice model will not do: one restricts to a suitable symmetric collection of names, checking the axioms again. These examples also mark a limitation: forcing proves relative consistency, not absolute consistency of the background theory. The countable-transitive-model picture gives a concrete semantic construction; the definable forcing relation and Boolean-valued formulation supply the corresponding formal consistency arguments without asserting that a transitive ground model can be proved to exist.
The assertions are relative independence results. We construct countermodels in a background model of ZFC; if ZF is consistent, its constructible universe gives a model of ZFC as well. The original model satisfies foundation and choice, supplying the positive sides.
For failure of foundation, use a Rieger-Bernays permutation model. Let interchange the old and and fix every other object, and put iff . The new extension of is the old set , so the representative of any old extension is . Bijectivity gives extensionality. Translate formulas recursively by this definition of . Old separation gives each new definable subset, and old replacement gives each new functional range; apply to the resulting extension to obtain its new representative.
Explicitly, a new pair is represented by ; the new union of is represented by ; and the new power set of is represented by
Starting from the new empty set, iterate the new successor and collect these iterates by old replacement, obtaining an inductive set. The old axiom of choice selects a member from each nonempty extension and thereby gives new choice functions. However the old object now satisfies and has exactly itself as its member: it is a Quine atom. Its new singleton has no -minimal member, so foundation fails.
To make choice fail, retain infinitely many Quine atoms and impose a finite-support symmetry restriction. A precise background construction uses tagged set codes. Each atom has extension . For every other set of available objects , introduce a unique ordinary set code with extension , except that is already represented by itself. Iterate this construction through the ordinals. Omitting the duplicate singleton codes makes the resulting relation extensional. Every permutation of extends to an automorphism of this universe by recursion through its ordinary codes.
An object has finite support if some finite has the property that every permutation fixing pointwise fixes that object. Retain the hereditarily finite-supported Quine-atom model: the object and every object reached through its membership relation must have finite support. The atomic self-loops are permitted. The atom set and all pure sets are retained.
The union of supports for a domain and finitely many parameters supports any definable subset or functional image: every permutation fixing those supports preserves the defining formula. Members of the subset or image are already hereditary, so this verifies separation and replacement. The collection of all retained subsets of a retained set is invariant under any permutation fixing that set's support, and each of its members is hereditary; this verifies the Axiom of power set. Pairs and unions have the union of the requisite finite supports, and the pure natural-number hierarchy verifies infinity. The coding still verifies extensionality.
If a choice function on all two-element subsets of had finite support , choose distinct . The transposition of fixes and the unordered pair , but moves either possible chosen value. This contradicts invariance of the function. Hence choice fails, while a Quine atom witnesses failure of foundation. We have a model of . Together with the original model this proves the required independence of choice over .
Work in a background model of ZFC. Each structure below satisfies every axiom of ZF except the indicated one and falsifies that axiom; the background model supplies the other consistency direction.
For the Axiom of union, put and use the hereditarily locally small membership model
The transitive class inherits extensionality and foundation. Definable subsets of its sets remain in it. If , a functional image of has size at most ; every member of that image is already hereditary, so the image belongs to . This verifies replacement, even though its values can have unbounded ranks. Also by the strong limit cardinal property, and each subset of is locally small. This verifies the Axiom of power set. Pairing and infinity follow similarly. But
since while . This is failure of sumset without failure of replacement or power set.
For the Axiom of power set, use the hereditarily countable sets . This is a transitive class. A countable union of countable transitive closures is countable, so it is closed under pairs, unions and functional images of its countable domains; these facts verify pairing, union and replacement. Separation, foundation and infinity also hold. Every subset of is hereditarily countable, but the full power set is uncountable by Cantor's theorem and cannot be a member of . Since every candidate internal power set would have to contain all those subsets, the power-set axiom fails.
For replacement, take the rank-initial transitive set . A limit rank contains the empty set and is closed under pairs, unions, subsets and power sets; it contains , and foundation and extensionality are inherited. Fix the parameter . The definable map
is internally described by a finite sequence of power-set iterations. Each finite sequence belongs to , so the definition is genuinely functional there. Its range has rank and is not in the structure. Thus this instance of replacement fails.
For extensionality, use the non-extensional membership model with one atom. Start with an atom having no members and build the ordinary cumulative coded sets over it, including a separate empty set. Interpret membership by the contents of a set code and give no members. The two different objects have identical empty extensions. Foundation holds by the code ranks; pure finite ordinals give infinity; pairs, unions, definable subsets and functional ranges have their usual set codes. For unrestricted power set, include the atom as well as all ordinary subset codes: the atom satisfies vacuously for every . This detail is necessary because the formulas here are the unmodified ZF formulas, without a set predicate. The collection still has a set code, so the Axiom of power set holds. All axioms except extensionality are satisfied.
Finally, , the hereditarily finite sets, satisfies every axiom except infinity. Pairs, unions, power sets and subsets of finite sets are finite, and every functional image of a finite domain is finite, so the full replacement schema holds. An inductive set would contain every finite von Neumann ordinal and would be infinite, whereas every member of is finite. Hence infinity fails.
A countable set is one admitting an injection into ; this includes finite sets and the empty set. An infinite countable set can equivalently be listed in a sequence indexed by .
For a countable union of countable sets , choose an injection for each nonempty . Assign the pair , where is the least index with . This is an injection into . The pairs are countable by diagonal enumeration; explicitly, with natural numbers starting at one, the Cantor pairing function
maps them bijectively to . Composing the two maps proves that the union is countable. Empty members contribute no elements.
To prove uncountability of the power set , suppose all subsets could be listed as . Define
For every , differs from on whether it contains . Thus is missing from the supposedly exhaustive list. This Cantor diagonal argument proves is uncountable.
For increasing functions in the question's non-strict sense, encode every subset by
where the value at zero is only a convenient auxiliary convention. Then
Each is even strictly increasing, hence is a nondecreasing function as required, and its successive differences recover uniquely. This is an injection from the uncountable power set into the requested collection. Therefore the increasing functions form an uncountable set.
For a decreasing function in the question's sense, is a nonincreasing function with positive integer values. Each strict decrease lowers its value by at least one, so there can be at most strict decreases. There is consequently a final drop, after which the function is constant. Every such function is determined by a finite initial list whose final value repeats forever. The set of all these lists is contained in
a countable union of countable sets, hence countable by the result just proved. Thus the decreasing functions form a countable set. These contrasting cardinalities of monotone natural-number functions come from the absence of an upper bound for increasing values and the finite number of drops available to decreasing natural-number values. If the natural numbers include zero, the same proof uses the bound instead.
Work in a ground first-order model of set theory satisfying ZF, and let be a definable bijection of its universe, whose inverse is also definable. Write and replace membership by
In this Rieger-Bernays permutation model, an object having prescribed extension is represented by . The Axiom schema of replacement in the ground model guarantees that images of sets under and are sets. The axiom of extensionality follows from injectivity of ; the new empty set is , and the new pair of is .
For the Axiom of union and Axiom of power set, representatives are respectively
Indeed, is an -subset of exactly when . Translate every first-order formula by replacing membership with membership in . Ground separation then forms each desired subextension of , and ground replacement forms each functional image; applying supplies its representative. To verify the axiom of infinity, define by ground recursion
Then is an -inductive set. Thus every ZF axiom except possibly the Axiom of foundation survives.
Interchange two distinct objects and , fixing everything else. Then , so is a Quine atom: internally . The nonempty set has no member disjoint from itself, violating the Axiom of foundation. The original membership model satisfies that axiom. Foundation is therefore relatively independent of the other ZF axioms.
A full Rieger-Bernays permutation model of a choice model still satisfies the axiom of choice: choose an old member of each nonempty extension and encode the resulting choice graph with the new ordered-pair operations. To obtain failure of choice, an additional restriction by symmetries is necessary.
Start instead with ZFC and use the definable permutation interchanging every with . These transpositions are disjoint and produce an infinite set of Quine atoms. Inside the resulting membership model build the cumulative universe over , closing at successive stages under sets of previously constructed objects, represented by . Atomic objects are kept as the designated base objects; for . Every permutation of extends recursively to an automorphism of this universe, with the atomic self-loops fixed by the recursive convention.
An object has finite support if every permutation fixing some finite pointwise fixes it. Retain the objects which have finite support and whose members recursively also have finite support, interpreting the atomic self-loops as the base case. This is the hereditarily finite-supported Quine-atom model. It is transitive for the new membership relation. Extensionality is inherited. Pairs and unions have supports contained in the union of the finitely many relevant supports. For a supported set , the collection of all retained subsets of is a ground set, by the full model's power set axiom, and is fixed by every permutation fixing a support of . Its members are retained, so this collection supplies the internal power set. A first-order formula with retained parameters is invariant under their common stabilizer. Consequently its definable subset of , and the range of a functional relation on , have that same finite support; ground separation and replacement first ensure that they are sets. The pure natural-number hierarchy supplies infinity. These arguments verify all of ZF except Axiom of foundation, which fails at the Quine atoms.
The family of all two-element subsets is retained and has empty support. If it had a retained choice function , choose two distinct Quine atoms outside a finite support of . The transposition of fixes and fixes the unordered pair , but moves either possible value . This is impossible. Thus ZF without Foundation has both choice models and models in which Choice fails, relative to the usual consistency assumption. The construction also explains why twisting membership alone was insufficient.
All assertions of independence below are relative consistency assertions. We construct structures satisfying the other ZF axioms but falsifying the indicated axiom; an ordinary model of ZF supplies the positive side. The convenient ground theory is ZFC, which has the same consistency strength as ZF by the constructible universe theorem.
For the Axiom of union, put and use the hereditarily locally small membership model
It is a transitive class. The condition requires each individual set in the membership ancestry to have size below ; it does not require its entire transitive closure to have size below . Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and witnesses infinity. For , the actual also belongs to : if , then by the strong-limit property, while every subset of and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain , ground replacement, applied to the relativized first-order formula, gives its range . Since and every value is already in , its range is also locally small. Thus every replacement instance holds.
However, belongs to : its members have cardinalities , and their members are smaller still. Its actual union is , of cardinality , which is not in . Transitivity makes any internal union witness equal to this actual union. Hence Union fails while all the other ZF axioms hold.
For the Axiom of power set, use the hereditarily countable sets in the ground choice universe. This is transitive and contains . Pairs, subsets and unions have countable transitive closure. For replacement, a functional image of a countable domain is countable, and the union of countably many countable transitive closures is countable; hence that image is again hereditarily countable. These observations, with inherited extensionality and foundation, verify all the remaining axioms. Every real, viewed as a subset of , belongs to . A power-set witness for would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas is uncountable by Cantor's theorem. Power set fails.
For the Axiom schema of replacement, use with actual membership. This limit-rank structure contains and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below . A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable function
is obtained by successive power-set operations starting with the parameter . Each finite iteration, including its finite history, belongs to the structure. Its range has rank and is not an element of . Thus the replacement instance for this first-order formula fails, although every other ZF axiom holds.
For the axiom of extensionality, take the well-founded cumulative set universe over two distinct urelements, and forget the predicate distinguishing urelements from sets. Each urelement has no members, just as the ordinary empty set has no members, so extensionality fails. Every other axiom survives in this pure membership language. Pairing, union, separation and replacement are witnessed by the corresponding ordinary sets of urelements and sets; foundation follows from their well-founded ranks, and the pure supplies infinity. Here foundation is written with “has a member” as its nonemptiness antecedent, and disjointness means having no common member. Formulations using inequality to one designated empty object are not equivalent after removing extensionality. There is also one necessary adjustment to power set: an urelement is vacuously a subset of every object because it has no members. Thus the power-set witness for is the ordinary set of all usual subsets of its extension, together with both urelements. This is still a set, and contains exactly the objects satisfying the unrestricted subset first-order formula. Consequently the countermodel falsifies Extensionality alone, without silently weakening Power set to sets only.
Finally, the hereditarily finite sets satisfy extensionality, foundation, pairing, union, power set and separation. Every functional image of a finite domain is a finite set of hereditarily finite objects, hence also belongs to , giving all replacement instances. No finite set contains and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.
For the Ehrenfeucht-Mostowski theorem, start with an infinite structure and a total order . Choose a Skolem expansion , and adjoin constants for . Require the elementary diagram of , distinctness of these new constants, and the order-indiscernible sequence schema: any two increasing tuples of the of the same length satisfy the same first-order formulas in the expanded language. Every finite fragment mentions finitely many new constants and finitely many first-order formulas. Enumerate a countably infinite subset of . For each of the finitely many first-order formulas, color its increasing tuples by its truth value in , including whatever fixed parameters occur in the fragment. Successive applications of the infinite Ramsey theorem leave an infinite subset homogeneous for all these colorings. Assign the finitely many new constants to distinct elements of this subset in their index order. Their finite indiscernibility requirements and the elementary diagram are then simultaneously satisfied.
The compactness theorem supplies an elementary extension containing the required distinct indiscernibles. Their Skolem hull is an elementary substructure: an existential first-order formula true of its elements has its chosen Skolem-function witness in the hull, so the Tarski-Vaught test applies. Any order automorphism of acts on this hull by
Indiscernibility makes this well defined, since every equality of two term representations is preserved. The same argument preserves every first-order formula; the inverse is given by . Thus it is an automorphism, uniquely determined in the language of the chosen Skolem expansion by its values on the generators. This proves both the indiscernible-model and automorphism forms of the Ehrenfeucht-Mostowski theorem. Uniqueness is not claimed for automorphisms of the reduct which need not preserve the chosen Skolem functions.
For simple typed set theory with atoms, write for the set predicate at sort . Members have sort one lower; urelements have no typed members, extensionality applies to sets, and every well-typed first-order formula defines a set at the next sort. Typical ambiguity adds for each closed sentence, where raises every sort by one. We prove finite satisfiability using Ramsey theorem, rather than assuming that adjacent sorts have the same cardinality.
Let . If , then . For increasing integers , interpret sort by , interpret by the objects of , and interpret adjacent-sort membership by actual membership restricted to these designated sets. All other objects of a sort are typed urelements. Every subset of is a designated set in , so comprehension holds for every first-order formula, including first-order formulas with quantifiers and parameters at other sorts. Two designated sets with the same members are equal, while the other objects have no typed members. Thus this is a full model of the typed axioms for every increasing sequence of levels. The extra preceding level gives a consistent interpretation of the bottom set predicate as well.
Take finitely many ambiguity sentences and let bound their highest sort before raising. Color increasing -tuples by the vector of truth values of these sentences in the corresponding finite sorted structure. There are finitely many colors. The infinite Ramsey theorem supplies an homogeneous set of indices. Choose the level sequence from it. The sentence is evaluated in the window , while is evaluated in the next window ; homogeneity makes their truth values equal. Sentences using fewer sorts simply ignore the unused final levels. Thus every finite family of ambiguity axioms has a model satisfying all the typed axioms. Apply many-sorted first-order compactness theorem to obtain
This is a relative consistency construction in the ordinary set-theoretic metatheory. Allowing urelements is essential here: skipping ranks leaves objects outside the represented power sets, and those objects must be permitted as urelements.
View a set family as a set of vertices of the Boolean lattice. The operation acts independently on each pair , where : it keeps a full or empty pair and moves a sole upper member down. Thus downward coordinate compression preserves cardinality.
Fix a tracing set . If , compression leaves the trace of a set family on unchanged. If , write for the two sections of the old trace, according to absence or presence of . The absent- section of the new trace is . Its present- section is contained in : an upper member survives only when its lower partner was also present in the original family. Consequently
In particular, downward coordinate compression cannot create new set shattering.
Repeatedly apply any changing downward coordinate compression. Each change strictly decreases , so the process terminates at a down-set with the same cardinality and with no larger trace on any . The Sauer-Shelah lemma says that a family shattering no -element set satisfies
Indeed, the compressed down-set also shatters no -element set. If it contained any member of size at least , all subsets of a -subset of that member would belong to the down-set, contradicting this restriction. Every member therefore has size at most , giving the bound. Equivalently, VC dimension at most gives size at most . The family of all sets of size at most attains this bound.
There is a different extremal example when . Toggle a fixed coordinate in the family of sets of size at most two:
The symmetric difference is a bijection, so this family has members. On each tracing set , it simply toggles coordinate if ; thus it preserves trace cardinality and set shattering. A triple has seven trace patterns, not eight. The new family differs from the original one because it contains . For the specified cardinality is , so the entire power set is the unique family of that size; the different example requires .
For the final bound, let count pairs both in the family. Deleting coordinate identifies precisely these pairs, so
Suppose every deletion lost at least two members, so for every . The trace inequality and preservation of cardinality show that after downward coordinate compression. The down-set contains the empty set and every singleton. For each , its second edge in direction has an upper endpoint of size at least two. Downward closure then supplies a pair . The pairs in therefore cover all coordinates, so at least pairs are needed. This proves two cube edges in every direction force many vertices:
Taking the contrapositive gives the required answer:
The threshold is sharp for every . Take the empty set, all singletons and pairs covering every coordinate. For even , use the disjoint pairs ; for odd , pair the first coordinates and add . This down-set has exactly members and at least two edges in every direction, so every -coordinate trace has size at most . Adding further members preserves those pairs and therefore preserves the failure whenever a larger cardinality is feasible. For , the putative counterexample cardinality is three, exceeding the size of the Boolean lattice; the sharpness construction naturally starts at .
A sigma-algebra on is a collection containing , closed under complements relative to , and closed under countable unions. These properties also give closure under countable intersections by De Morgan laws.
Let . Every constituent sigma-algebra contains , so . If , its complement belongs to every , hence to . Likewise, if for all , then belongs to every . Thus is a sigma-algebra. For an empty indexing set, the usual intersection convention gives , which is also a sigma-algebra.
A union need not work. On take
Their union contains and but not , so it is not a sigma-algebra. Put and let be the collection of all sigma-algebras on containing . This collection is nonempty because it contains the power set . By the preceding intersection argument,
is a sigma-algebra containing every , and it is contained in every other such sigma-algebra. This proves existence and minimality.
For the independent random variables, define the tail sigma-algebra by
Fix a tail event . For each , it belongs to , which is independent of . To justify independence of the generated sigma-algebras, first use independence of finite collections on cylinder events, then extend twice by the pi-lambda theorem. In particular, for every and every .
The increasing union is an algebra of sets generating . The collection of satisfying this factorization is a Dynkin system: it contains , is closed under complements, and under countable disjoint unions. The pi-lambda theorem therefore extends the factorization to all . Since , taking gives . Consequently,
This is the Kolmogorov zero-one law, proved here directly.
For each fixed , write for , with . The random variable is finite, so . Adding a real sequence tending to zero changes neither the extended-real limit inferior nor the extended-real limit superior. Hence
The quantities on the right are measurable with respect to : write the limit inferior as and the limit superior as , using countable operations on measurable functions. Therefore both threshold events belong to every such sigma-algebra, and hence are tail events, for every real threshold, including when either limit is infinite.
The final recurrence claim is false under the printed hypotheses. For , let be independent signs with equal probabilities for and , and set . These random variables are independent, have symmetric distributions, and obey . Nevertheless, the geometric series gives, on every sample path,
Thus the proposed repeated-return event has probability zero, even though none of the increments is degenerate. The Kolmogorov zero-one law does not determine which of zero and one occurs.
An additional identical-distribution hypothesis makes the intended conclusion true. Here is a full proof of that qualified version, using the oscillation of a bounded centered iid random walk. Symmetry and integrability give , so is a martingale for its natural filtration. If the common probability distribution is concentrated at zero, every is zero and the conclusion is immediate. Otherwise choose with . The Borel-Cantelli lemmas then give infinitely often almost surely; thus cannot converge to a finite limit.
For , let . Before the sum is below , and at it is at most . The stopped martingale is therefore nonnegative. A stopped integrable martingale remains a martingale at these bounded times, and a nonnegative martingale converges finitely almost surely by the martingale convergence theorem. On this would force to converge finitely, which has just been ruled out. Hence almost surely. Apply the same argument to and take a countable intersection over positive integer . It follows that
There are therefore arbitrarily late passages from above to below . A path with bounded increments of magnitude at most cannot make such a passage without visiting : jumping directly between its two open complementary half-lines would require an increment larger than . There are infinitely many such visits. Thus with the added identical-distribution hypothesis, the intended answer is
A transitive set satisfies , equivalently . If is transitive and , choose with . Transitivity gives , so . Thus is transitive. If , then and transitivity implies , whence . Thus the power set is transitive as well.
The converse for the union is false: take . Then is transitive but is not. The power-set converse is true: if , then implies , so .
Define , and . This is a set by replacement and union, contains as a subset, and is transitive because taking a member advances one stage. Induction shows it is contained in every transitive set containing , proving the transitive closure property.
If the rank of a set is , then
Every subset of has rank at most , and itself is an element of , proving the first formula. The second is transitive closure preserves set-theoretic rank. Here the convention is , not .
The Rieger-Bernays permutation model changes membership, not the underlying domain. In a model of ZF, let be a definable class bijection, with parameters allowed, and define
Every old set is the new extension of precisely the object . Translation of formulas replaces each membership assertion by this definable relation. Both images and inverse images of old sets under are sets by replacement.
Here are the axiom checks. Extensionality follows because equal new extensions mean and hence . The new empty set is and the new pair is . For an object , new union and power set have representatives
These formulas verify the actual new membership conditions. A definable subset of the new extension is an old set by separation after translation, and its representative gives new separation. Similarly, a functional new formula on that extension has an old set as range by replacement; apply to its range. For infinity, iterate the new successor operation
starting from the new empty set. Old recursion and replacement collect its finite iterates into a set , and is a new inductive set. Thus all axioms of ZF except possibly foundation hold.
Now swap the old objects and and fix everything else. The old object then satisfies , and its entire new extension is . It is a Quine atom, so foundation fails. Taking to be the identity gives the original model where foundation holds. Foundation is independent of the other ZF axioms, relative to consistency of ZF.
A full permutation of a model of choice does not destroy choice. Given a new family of nonempty new sets, old choice selects an element of each old extension ; replacement converts its graph into new ordered-pair coding. Thus simply repeating the preceding unrestricted permutation construction would not prove independence of choice. The extension needed is the hereditarily finite-supported Quine-atom model.
Start with a model of ZFC and simultaneously swap with for all . These transpositions have disjoint supports: none of these infinite ordinals is a singleton, and the ordinals and their singletons are separately distinct. Put , whose members now have new extensions . Build the universe over these Quine atoms by allowing arbitrary new sets of previously constructed objects at each successor stage, and taking unions at limit stages. More explicitly, begin with , put
and take the union over all ordinals. The singleton with sole member is already , as extensionality requires; it is not added as a different atom or set. Every other object's membership has a well-founded construction rank once these designated atomic self-loops are treated as rank-zero leaves.
Every permutation of extends to an automorphism of this universe: on atoms use , and on every non-atomic object recurse by
The inverse permutation gives its inverse, and the formula preserves . Call an object supported by a finite when every permutation fixing pointwise fixes that object. Retain only objects which are supported and all of whose members are hereditarily supported; the recursion here again stops at atoms, whose support is their singleton. Denote this class by .
We verify that is a model of ZF without foundation. It is membership-closed and hence retains extensionality. Pairing uses the union of the two parameter supports, and union uses the support of its input. For separation, use the finite union of the supports of the domain and all parameters: permutations fixing them preserve satisfaction in , so they fix the defined subset. Every member remains hereditary. For replacement, the same support fixes the image of a definable functional relation; its elements already lie in by the internal range condition, and old replacement supplies the underlying set of them. These assertions are legitimate class translations because construction ranks, supports and hereditary support are definable in the starting model.
For power set, start with the set of all new subsets of a supported set and retain exactly those lying in . The resulting collection is fixed by every permutation fixing the original set's support: the action preserves hereditary support and permutes its subsets. Every retained member is hereditary, so this is the internal power set. The empty set and the pure finite and infinite natural-number hierarchy have empty support, yielding infinity. The new pairing, union and comprehension representatives discussed above therefore remain inside . Foundation still fails because all the Quine atoms are in .
The set itself has empty support and hereditary members. So does the family of its two-element subsets, each of which has a finite support in a permutation action. If this family had a choice function , let be a finite support in a permutation action of , and choose distinct . The transposition of fixes and the unordered pair , but interchanges either possible chosen value . It cannot fix the function graph, contradicting its support. Thus choice fails in .
The unrestricted permutation model over the same initial ZFC model satisfies choice and fails foundation, whereas its hereditarily supported submodel fails both. Hence choice is independent of ZF with foundation omitted. These are relative-consistency constructions, not an assertion that ZF proves its own consistency. Starting with ZFC is harmless for the usual consistency comparison with ZF, by the constructible-universe relative-consistency theorem.