This is a followup question to [Does foundation/regularity have any categorical/structural consequences, in ZF?](https://mathoverflow.net/questions/300046/does-foundation-regularity-have-any-categorical-structural-consequences-in-zf)


As shown in answers to that question, the axiom of foundation (AF, aka regularity) has consequences over ZF–AF that can be formulated purely in structural terms (i.e. using sets only in ways that respect isomorphism).


In particular, it implies the statement “Every set can be embedded into a set equipped with a well-founded extensional relation”, which Mike Shulman has called the *axiom of well-founded materialisation*; and (by the arguments in that question) this axiom should have the same structural consequences as foundation.


This statement is a very mathematically reasonable one. However, I don’t think I have ever seen this or anything similar appearing in practice in ordinary mathematics — only in logical investigations like this one, where it occurs specifically because of its relation to AF. So my question here is:
**Does the axiom of foundation have any consequences (over ZF–AF) that have appeared in ordinary mathematics?**


Slightly more precisely: 


* By “consequence of foundation over ZF–AF”, I of course mean principally a statement that’s provable in ZF, but not in ZF–AF. But I’d also be interested in e.g. a proof in ZF that doesn’t go through in ZF–AF and can’t be trivially modified to do so.
* By “ordinary mathematics”, I mean… this of course is subjective, and mostly I think “we know it when we see it”, and hope that most of us will find our judgement on it mostly agrees. But to articulate my own intent here a little: a sufficient (but not necessary) condition to would be that the statement has been considered in a field of mathematics other than logic; necessary conditions would be that it’s purely structural, and that it’s been considered outside work specifically investigating foundation (or related axioms) or modelling set theories that include foundation. To illustrate the non-necessity of the “outside logic” criterion — I would certainly be happy to consider consequences in e.g. general classical model theory.


See e.g. [Where in ordinary math do we need unbounded separation and replacement?](https://mathoverflow.net/questions/121406/where-in-ordinary-math-do-we-need-unbounded-separation-and-replacement) for a similar question, about different axioms, and relevant discussion of what should be considered “ordinary mathematics”.



Consequences of foundation/regularity in ordinary mathematics (over ZF–AF)?
I think Frucht's theorem, the statement "every group is isomorphic to the automorphism group of a graph", is a great example of what you're looking for; from the statement, it'd be hard to tell that any set theory is relevant in the proof.


Frucht's theorem is true in ZF (and ZFC-AF), but independent from ZF-AF. I'll sketch a proof below.


To construct a model of ZF-AF where Frucht's theorem fails, we start a permutation model of ZFA (ZF with atoms) where it fails. The basic Frankel model, where A is superamorphous, works fine ([see Jech's "The Axiom of Choice" book](https://gwern.net/docs/math/1973-jech-theaxiomofchoice.pdf) if you haven't seen this model before).


To see it fails in the Frankel model, consider the free abelian group $G$ generated by the atoms. Suppose $G$ were the automorphism group of a graph $\Gamma$. Since $\Gamma$ is symmetric, it has a finite support, $E$, and every permutation of $A$ which fixes $E$ must fix $\Gamma$. This means every element of $\mathrm{Perm}(A\setminus E)$ corresponds to an element of $\mathrm{Aut}(\Gamma)$, which is $G$ by assumption. In particular, let $\pi$ the a transposition swapping two elements $a, b\in A\setminus E$. $\pi$ has order 2, so the corresponding element of $G$ has order $\leq$2, but $G$ is free abelian, so we must have $\pi$ acts trivally on $\Gamma$. However, $\pi$ acts non-trivially on $G$; it swaps the generators $g\_a$ and $g\_b$ corresponding to $a$ and $b$. $g\_a$ and $g\_b$ must correspond to distinct automorphisms $\gamma\_a$ and $\gamma\_b$ of $\Gamma$. If $v$ is a vertex in $\Gamma$, then
$$\gamma\_a(v)=\pi(\gamma\_a(v))=\pi(\gamma\_a)(\pi(v)) = \gamma\_b(\pi(v)) = \gamma\_b(\pi(v)) = \gamma\_b(v)$$
So, $\gamma\_a = \gamma\_b$. Since $\gamma\_a$ and $\gamma\_b$ can't be distinct, $\mathrm{Aut}(\Gamma)$ can't be $G$.


Finally, to get a model of ZF-AF instead of ZFA (where atoms are all empty), you can replace each atom with a distinct Quine atom (a set so $x=\{x\}$). As long as you're careful to define free abelian group in a way that doesn't depend on $x$ not equaling the pair $\langle x,x\rangle$, there shouldn't be any difficulties.


As for why Frucht's theorem holds in ZF, it requires fairly trivial modifications to [Sabidussi's ZFC proof](https://link.springer.com/article/10.1007/BF01319053).


Given a group $G$, begin with a colored, directed Cayley graph of $G$. This has automorphism group $G$, but if we forget the edge colors and directions, the graph may have extra automorphisms. We can indicate directions by attaching a stick of length 1 and 2 in the middle of every edge in the Cayley graph, resulting in an undirected colored graph with the correct automorphism group. If there are countably many colors, a similar trick works for colors, but in general, we will need distinct rigid graphs for each generator of $G$ to label each color. Under AC, it suffices to build a unique rigid graph for each ordinal; however, Sabidussi's paper actually builds a unique rigid graph for every set, by induction on rank. The idea is, roughly, that given a set in $S\in V\_{\alpha+1}$, you begin with a complete graph on $V\_\alpha$, and attach to each vertex it's corresponding, inductively defined graph. The resulting graph is now rigid. Then you attach more things to this graph to indicate elements or non-elements of $S$.


I have a better write-up of this argument (with sorely needed pictures) in my thesis, but until that's somewhere I can link conveniently, Sabidussi's paper is probably the best reference for actual induction details.


