Does foundation/regularity have any categorical/structural consequences, in ZF?

Question

(Prompted by reflection on this old answer, and its suggestion of the “harmlessness” of the axiom of regularity.)

In ZFC, one may justify the axiom of foundation (AF, aka the axiom of regularity) as being “convenient, and harmless”, as follows. If $V = (V,\epsilon)$ is a model of ZFC–AF, then its well-founded part $V_{wf}$ models ZFC. Moreover, ZFC–AF suffices for the standard proof of the well-ordering principle, so $V$ believes that every set is isomorphic to some von Neumann ordinal, which will lie in $V_{wf}$. Hence the inclusion $V_{wf} \hookrightarrow V$ underlies an equivalence of their (internal, large) categories of sets; so any “purely structural” statement should hold in $V$ if and only if it holds in $V_{wf}$. “Purely structural” can be made precise in various reasonable ways (e.g. any statement expressible in the language of categories/elementary toposes/higher-order logic/type theory, interpreted into set theory), and includes essentially all of ordinary mathematics, excluding only a few explicitly material-set-theoretic statements such as AF itself.

Summing up: given any model of ZFC–AF, one can replace it by its well-founded part, which is now a model of ZFC, believing the same purely structural statements as the original model. So relative to ZFC–AF, AF has no purely structural consequences — i.e. it’s not quite conservative, but pretty close to it.

However, this argument relied essentially on the axiom of choice! Relative to ZF–AF, is AF still harmless, or does it have some structural consequences? Precisely: is there some “purely structural” statement $\varphi$ (in one of the senses above, or some similar sense), such that $ZF \vdash \varphi$, but $ZF-AF \not \vdash \varphi$?

I’m also interested in the same question with ZF weakened to IZF, CZF, and similar theories. Over these of course AF should be replaced by $\in$-induction (a classically equivalent and constructively better statement), as described in this older question (which considers closely related issues to the present question, but doesn’t as far as I can see directly imply an answer here).

Answer 1

Yes, the axiom of foundation has structuralist consequences.

Let $\phi$ be the assertion, "if every well-founded set is well-orderable, then every set is well-orderable."

This statement, I claim, can be made in a (technically) structuralist manner, since it is a statement about all nodes in a certain kind of digraph, namely, the graphs that are stratified by a well-ordered sequence of levels, such that every new level has a unique node for every subset of the nodes on the previous levels. And then assert that every node in such a graph has another node that amounts to a well-order of the set pointing at that node. That is, just make a structuralist description of the $V_\alpha$ hierarchy, and assert that if all the sets arising in it are well-orderable, then every set is well-orderable.

Certainly ZF proves the statement $\phi$, since ZF proves that every set arises in the well-founded $V_\alpha$ hierarchy.

But ZF-AF does not prove the statement, since, I believe, it is consistent with ZF-FA that the well-founded part of the universe satisfies AC, even if there is a non-well-orderable set of Quine atoms in the non-well-founded part of the universe. One can build such a model, I believe, as a symmetric extension of a model of ZFC, by adding a collection of urelements, considered as Quine atoms.

Answer 2

The following provides an "engine" for generating many structural statements provable in ZF but not in ZF without foundation:

Theorem. Let $S$ be any structural equivalent of the axiom of choice within ZF without foundation (e.g., Zorn's Lemma or Tychonoff's compactness theorem). Then the following structural statement $R_{S}$ (in honor of Herman and Jean Rubin) is provable in ZF; but NOT in ZF without foundation:

$R_{S}$ := "$S$ holds iff every linearly orderable set is well-orderdable".

Explanation. The nontrivial direction ($\leftarrow$) of $R_{S}$ follows from the theorem below, and the observation that the powerset of every well-orderable set $S$ is linearly orderable (by deeming $X$ to be less than $Y$, where $X$ and $Y$ are subsets of $S$, and $S$ well-ordered by $<$, if the $<$-first element in the symmetric difference of $X$ and $Y$ is in $Y$. The proof is readily implementable in Zermelo set theory, i.e., ZF without the foundation axiom and without the replacement cheme, but with the separation scheme).

Theorem (H. Rubin & J. Rubin). ZF proves that if the powerset of every well-orderable set is well-orderable, then the axiom of choice holds.

The above theorem was first published the 1963 book Equivalents of the Axiom of Choice, by Herman and Jean Rubin. A proof can also be found in these lecture notes by Andrés E. Caicedo (see Theorem 13). Later, in this 1973 paper of Felgner & Jech, a model of ZF with atoms was built in which the powerset of every ordinal is well-orderable, but the axiom of choice fails; this proof also appears in chapter 9 of the book Axiom of Choice by Jech.