The basic Fraenkel model is a model of the set theory ZFA that doesn’t satisfy the axiom of choice. It was one of the first examples of a permutation model of set theory. In the basic Fraenkel model, we have a countable set of atoms , and we take the full permutation group of . The normal filter of subgroups is generated by the stabilizers of finite subsets of .
In the language of material set theory, this is just a Fraenkel-Mostowski model given by a countable set of atoms with the full permutation group acting on it. The normal filter of subgroups is generated by the stabilizers of finite subsets of , ie. groups of the form
where is a finite subset of .
We can take the same group as above, with topology generated by the stabilizers . We can then form the topos of continuous G-sets, whose objects are sets with a continuous action of (with the set given the discrete topology), and morphisms are the -equivariant maps. This topos is also known as the Schanuel topos.
The internal logic of this topos can be identified with the standard logic of the material model of ZFA constructed above, if we interpret the universal quantifiers in ZFA suitably (eg. via stack semantics, or other semantics as mentioned in Fraenkel-Mostowski models)
It is clear that the set of atoms in the Fraenkel-Mostowski model cannot be linearly ordered. So the ordering principle (that every set can be linearly ordered) fails. Consequently, the axiom of choice, boolean prime ideal theorem etc. all fail. In fact, even countable choice fails.
We can consider the object consisting of the set of atoms with the obvious action of . It can be shown that this does not biject with any finite set (ie. a set that is a finite coproduct of the terminal object), but any injection must be a surjection (this is true both as an external statement or as a statement in the internal logic). So this is an example of a Dedekind-finite but not finite set.
We can consider the case where we have more atoms, or allow stabilizers of larger subsets. In different cases, weak versions of Choice may hold. For example, if we have many atoms, and take the normal filter generated by stabilizers of countable subsets, then the axiom of choice holds for any well-ordered family of sets. Details can be found in the book Consequences of the Axiom of Choice.
The model is given by in the book
The various properties of the model are listed in detail. Variations of the model are listed as and .