Write for ZF with the Axiom of foundation omitted. Independence is a relative-consistency assertion: from a model of ZFC we construct models of , both with and without axiom of choice. A model of ZFC itself supplies the positive cases.
First use a Rieger-Bernays permutation model. Inside the starting model choose a definable class bijection and put exactly when . The new extension of is the old set , so any prescribed set of new members has representative . We verify the axioms rather than treating the change of membership as automatically harmless.
The axiom of extensionality follows from injectivity of . The new empty set is and a pair with members is . The union of a new set is represented byA new subset of means . Hence the new power set of is represented byThese are sets by the original power-set and replacement axioms. Translate each formula by replacing membership with . The original separation axiom extracts the required subset of , and replacement collects the range of a definable functional relation on ; applying gives their new representatives. Thus the full Axiom schema of replacement and separation schemes survive.
For axiom of infinity, start at , iterate the new successor along the old , and take a new set representing this range. It contains the new empty set and is closed under the new successor. Finally, the old axiom of choice well-orders each old extension . Encode that relation using new ordered pairs and its new set representative. All subsets of the extension are represented in the new model, so this is genuinely a new well-order. Thus choice survives the full membership permutation.
Now transpose the old and and fix every other object. The old empty set satisfies , so its sole new member is itself: it is a Quine atom. The nonempty new set has no member disjoint from it, violating foundation. This gives . Together with the starting model, this proves independence of foundation.
For failure of choice, a membership permutation alone is insufficient, as the verification above shows. Add a symmetry restriction. Choose distinct old objects for and let simultaneously swap with , fixing all other objects. The two families are disjoint, so this is a class bijection. Each is now a Quine atom. Write for the new set having precisely these atoms as members.
Every permutation of the atoms extends to an automorphism of the new universe, fixing its pure well-founded part. To construct it, send the atoms according to the prescribed permutation and, for any other object , take the unique object whose new members are the images of its new members. This recursion is well founded away from the atomic self-loops: every other membership step decreases old rank, including the steps from the transposed singletons to their old extensions. Thus all the required automorphisms exist.
An object is supported by a finite set if every atom permutation fixing pointwise fixes it. Let consist of objects that have finite support in a permutation action and all of whose new membership descendants also have finite support in a permutation action. This is the hereditarily finite-supported Quine-atom model. The atoms belong to , as does itself. We check that restricting to preserves .
Extensionality is inherited because every member of an object of is again in . Empty sets, pairs and unions have supports obtained by taking finite unions of the supports of their parameters, and their descendants are already supported. The pure natural numbers and their set are fixed by every atom permutation, giving infinity. For separation, permutations fixing the domain and formula parameters preserve the defined subset, which therefore has their common finite support in a permutation action. For replacement, translate the relativized formula into the original universe and use original replacement to collect its unique values. Every value lies in , and the range is invariant under the same finite support in a permutation action. Finally, the collection of all -subsets of an object is a subcollection of its full new power set, hence is a set in the original universe. Every permutation fixing a support of permutes these supported subsets, so this collection is supported; its members and their descendants lie in . This verifies the internal power-set axiom. These arguments handle the full schemes with arbitrary finite tuples of parameters.
There is no choice function on the two-element subsets of in . Suppose were one and had finite support in a permutation action . Choose distinct atoms . The transposition exchanging them fixes and the unordered pair , but exchanges its two possible selected values. Thusis impossible. The family of all such pairs belongs to : it is invariant under every atom permutation and each pair has finite support in a permutation action. Therefore ; it still contains the self-membered atoms, so it also fails foundation. We have provedThe positive-choice permutation model and this negative-choice symmetry model establish independence of choice from . These constructions can be carried out internally in any starting model; no assumption of a transitive set model is needed.
Articles by others on the same topic
There are currently no matching articles.