All consistency assertions here are relative: begin with a model of ZFC, obtainable from a model of ZF by its constructible universe as proved below. First use the Rieger-Bernays permutation model. Let exchange the old empty set with its old singleton and fix every other object, and define
An old set is the extension, in the new relation, of . This immediately verifies extensionality and gives explicit representatives for the new empty set, pairs, unions and power sets: the old extensions required are respectively , , , and . Translate any formula by replacing membership by ; old separation and replacement then give the desired new subsets and functional ranges, whose representatives are obtained by .
For infinity, recursively form the new empty object and successors . The old replacement axiom collects the sequence ; the representative of its range is a new inductive set. The old object has new extension , so and its singleton witnesses failure of the Axiom of foundation. Choice survives this full permutation construction: old choice applied to a family of nonempty new extensions selects its members, and new ordered pairs and a representative of their old set give the new choice function. Thus is relatively consistent. A well-founded starting model gives the opposite possibility for foundation.
To make choice fail, a symmetry restriction is essential. Here is an explicit pure-set construction with many Quine atoms. Take a countably infinite set of distinct tagged objects . Give the extension . For every subset of objects already constructed, introduce an object with extension , except that is defined to be itself. Use a disjoint tag for all other codes , so identical extensions have identical codes and distinct extensions have distinct codes. Iterate this operation transfinitely, taking unions at limits. Each level is an old set, and its subsets are an old set, so this is a definable class construction. Every non-atomic membership edge decreases construction rank. Atomic edges are just the prescribed self-loops. Consequently the resulting structure is extensional, has the required pairs, unions and power sets, and the old replacement axiom bounds ranks of definable functional ranges. Its pure finite ranks supply infinity.
Every permutation of extends recursively by . An object is finitely supported if some finite has the property that every permutation fixing pointwise fixes that object. Retain objects all of whose members, and members' members, are finitely supported, with recursion stopping at the atomic self-loops. Call this class , the hereditarily finite-supported Quine-atom model.
We must verify its set axioms, not merely declare it a symmetric model. Empty set, pairs and unions have supports given by finite unions of the supports of their arguments. For separation, a formula with finitely supported parameters and domain is invariant under permutations fixing the union of those supports; its selected extension is therefore supported, and all its elements already lie in . For power set, take all codes with and . They form an old set, by separation from the bounded code level. Permutations fixing a support of permute this entire collection, so its code is supported and belongs to . For replacement, translate the relativized formula to the original universe and use old replacement to collect its unique values. Equivariance gives this range a support from the parameters and domain, and every range element lies in . Infinity uses the pure natural-number construction, fixed by every atom permutation. This proves .
The set and the collection of its two-element subsets have empty support and belong to . Suppose the latter had a choice function , with finite support . Choose distinct . The transposition of fixes , hence , and fixes the unordered pair . But it swaps whichever member selects, a contradiction. Therefore
Together with the full permutation model satisfying choice, this proves independence of choice from ZF without foundation, using the same replacement of atoms by self-membered pure sets. The negated-choice model also fails foundation; this suffices for independence over the foundation-free base.

Articles by others on the same topic (0)

There are currently no matching articles.