Critical points and the Foundation Axiom

(Note: This question is related to my previous mathoverflow question, "Critical Points in $ZF$ without Choice".)

In the Stanford Encyclopedia of Philosophy entry "Non-Wellfounded Set Theory" (Section 2.2, "The Foundation Axiom"), one has the following statement (my comments regarding it are in brackets):

The Foundation Axiom ($FA$) may be stated in different ways. Here are some formulations; their equivalence in the presence of the other [$ZF$?] axioms is a standard result of elementary [$ZF$?] set theory [the last two, (4) and (5), are particularly relevant to my previous question]:

(4). For every set $x$, there is an ordinal $\alpha$ such that $x$$\in$$V_{\alpha}$. [seemingly necessary for Asaf's proof in his answer to my previous question]

(5). $V_{[ZF?]}$=$WF$ [the class of well-founded sets].

Question 1: Can the equivalence of (4) and (5) (and their equivalence to $FA$) be proved in $ZF$ alone, without recourse to Choice?

Question 2: Regarding (5) (i.e. $V$=$WF$--my comment excluded), does $V$=$V_{ZF}$? I ask this question because of the following: in the Daghighi, Golshani, Hamkins, and Jerabek paper, "The Role of the Foundation Axiom in the Kunen Inconsistency", they claim (and prove, in $GBC^{-f}$ and in $ZFC^{-f}$) that the Kunen inconsistency (in the following form: "There is no nontrivial $\Sigma_1$-elementary embedding $j$:$WF$$\rightarrow$$WF$.") holds for $WF$. If $V_{ZF}$=$WF$, then it seems that there must be a way to adjust their proof so that it doesn't need Choice (in which case, a major open problem will have seemingly been solved). What, if anything, is wrong with this picture?

• Where do you think the axiom of choice is being used in the proof of equivalence between Foundations and the two statements you wrote? – Asaf Karagila Jun 29 '16 at 12:54
• What is $V_{ZF}$? (I also second Asaf's question - I don't see where choice is being used in the standard argument that $(4)$ is equivalent to Foundation). – Noah Schweber Jun 29 '16 at 13:35
• @AsafKaragila: I wished to see if (4), (5) , and $FA$ could be proved equivalent in $ZF$ alone--I am not presuming Choice is needed (as Noah was kind enough to point out in his comment). I presume, then, that (5) can be proved equivalent to (4) and $FA$ in $ZF$ and in (5), $V$=$V_{ZF}$, $V_{ZF}$ being the universe generated by the axioms of $ZF$ (as opposed to the universe $V_{ZFC}$, which is the universe generated by the axioms of $ZFC$)? – Thomas Benjamin Jun 29 '16 at 15:01
• I think Asaf and Noah have answered your question: The usual proofs of these equivalences don't use choice. But your last comment raises another question: What do you mean when you say a universe is "generated" by some axioms? One possibility is that you mean a universe that is assumed to satisfy those axioms but is not further specified. Your use of the definite article ("the universe generated by ...") suggests that you have something else in mind, but I can't imagine what. – Andreas Blass Jun 29 '16 at 15:56
• @AndreasBlass: I really should have said 'satisfied by $V$'. By 'generated', I meant 'generated by the axioms and theorems in 'the' cumulative hierarchy'. Since one can use the term 'model' as 'universe', the axioms 'generate' a proper class of similar, but distinct models that satisfy a given first-order theory. Apologies. – Thomas Benjamin Jun 29 '16 at 16:41

As far as I understand your question, this is the answer:

Suppose $V$ is a model of $ZF$ minus Foundation (call this theory "$ZF^-$"). Then the following are equivalent:

• $V$ satisfies Foundation - that is, $V$ is in fact a model of all of $ZF$.

• "$V=\bigcup_{\alpha\in ON} V_\alpha$" - that is, for each $x\in V$ there is some $\alpha\in ON^V$ such that $V\models x\in V_\alpha$.

The usual proof goes through without any changes - in particular, Choice is not used anywhere.

As far as the result of Daghighi, Golshani, Hamkins, and Jerabek you cite: this seems orthogonal to the (non-)use of choice in the above theorem. Their result is that if $V$ is a model of - say - $ZFC^-$, then there is no nontrivial $\Sigma_1$-definable elementary embedding from $WF^V$ to $WF^V$. I don't see how the observation above has anything to do with removing choice from this argument.

• Regarding the second point in your answer--this is because $WF^{V}$ (since $WF^{V}$ is a model of $ZFC^{-f}$) is a class of well-ordered sets (since Choice still holds for $WF^{V}$)? – Thomas Benjamin Jun 30 '16 at 1:07
• @ThomasBenjamin Yes, but I still don't see the connection - how does the fact that "$\bigcup V_\alpha=V$ is equivalent to foundation over ZF" have anything to do with extending the result mentioned to ZF? – Noah Schweber Jun 30 '16 at 5:07
• Since $V_{ZF}$=$WF$ and $V_{ZFC}$=$WO$ ($WO$=the class of all well-ordered sets), the $V$ for $ZFC^{-f}$ is still a class of well-orderd sets (since Choice still holds for $ZFC^{-f}$). Recall that in the paper mentioned, the theorem ("Work in $GBC^{-f}$ or $ZFC^{-f}$. Then there is no nontrivial $\Sigma_1$-elementary embedding $j$:$WF$$\rightarrow$$WF$.") was billed as stating that the Kunen inconsistency still holds for the class $WF$ of $GBC^{-f}$ or $ZFC^{-f}$. Though true, it seems to me a bit of 'false advertising', since the '$WF$' for $GBC^{-f}$ and $ZFC^{-f}$ are – Thomas Benjamin Jun 30 '16 at 9:49
• (cont.) really classes of well-ordered sets, and the Kunen inconsistency holds of course for these. Since for $<$$WF,\in$$>$, $\in$ is rigid for $WF$ (since $WF$ is a transitive class), I conjectured that there are no nontrivial elementary embeddings $j$:$WF$$\rightarrow$$WF$ and asked essentially whether the results of Theorem 1 of the paper in question can, in fact be extended to the class $WF$ (a closer look at the theorem suggests--probably not....). – Thomas Benjamin Jun 30 '16 at 10:38
• Considering that my question has been downvoted, I am considering deleting the question. Since I have accepted your answer, I am not sure whether I should. Please advise. Thanks. – Thomas Benjamin Jul 1 '16 at 0:07