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 byIn 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 respectivelyIndeed, 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 recursionThen 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.
Articles by others on the same topic
There are currently no matching articles.