The fact that the axiom of foundation doesn't imply the axiom of choice is pretty standard (the model Cohen created to prove the consistency of $\neg AC$ models the axiom of foundation as well), and it's also known that you can have both of them (in $\mathbb{L}$ for instance), or neither of them (Fraenkel's model where the set of atoms is countable). But can you have $AC$ without the axiom of foundation ? What might work would be to do just like Fraenkel did and build a model with only one atom, so that you wouldn't have the issue with the set of atoms, but I'm not sure one can prove that choice doesn't fail elsewhere in such a model. So the question is : does $AC$ imply $AF$ ?
2 Answers
Of course the axiom of choice is consistent with the failure of the axiom of foundation.
To get Fraenkel's model with the atoms, you usually start with a model of $\sf ZFA+AC$. You can find the relevant proofs in Jech "The Axiom of Choice" in Chapter 4.
(Note that atoms are usually obtained by weakening extensionality, not foundation. To get to foundation one has some way to go. You can find the details in Felgner's "Models of ZF set theory", and more about independence of various statements.)
-
$\begingroup$ Yes indeed I had forgotten that when you create atoms you keep choice, it's when you go to HDOA that you lose it, so simply creating atoms gives the answer. $\endgroup$ Commented Dec 12, 2016 at 21:50
The following is an easy recipe for building a model of ZFA+AC with one atom, from a model $M$ of ZFC (it's trivial to modify this construction to include arbitrarily large sets of atoms, and even a proper class of atoms). In $M$, let $T$ be the class of well-founded (rooted) trees with all terminal nodes labelled either "$0$" or "$1$". Intuitively, such a tree corresponds to a set in the model of ZFA+AC we're building, with "$0$" being the emptyset and "$1$" being the unique atom $\alpha$. For instance, the set $\{\{\}, \alpha\}$ would correspond to the tree with a root and two leaves, one leaf labelled "$0$" and one leaf labelled "$1$".
Now, many trees correspond to the same set (e.g. consider the tree with a root and two successors, each of which are leaves labelled "$0$" - this corresponds to $\{\{\}, \{\}$, which is just $\{\}$, which is already named by the tree with two vertices, the leaf being labelled "$0$"); but we can fix this by restricting attention to the class $T_0$ of rigid trees (where rigid means no nontrivial self-bijections respecting the tree ordering and the labelling of leaves). And in $T_0$ there's a natural notion of membership, "$\varepsilon$" - namely, $t_0\varepsilon t_1$ if $t_0$ is the tree induced by some immediate successor of the root of $t_1$.
The class $T_0$, with this relation $\varepsilon$, is a model of ZFA+AC+"There is one atom," Choice holding since Choice holds in our background model $M$.
It's worth noting that the model $N=(T_0, \varepsilon)$ is (coded by) a definable subclass of $M$, and that $M$ is isomorphic to the pure part of $N$ via a (definable class) map in $M$.