When can "$j: V \rightarrow M$ is an elementary embedding" be defined in ZF?

Question

This regards elementary embeddings of inner models of set theory.

It seems that it is in general "stated" via an axiom schema each member of which states that the class function is elementary with respect to a specific formula.

However, for certain elementary embeddings — namely those induced by measurable cardinals — it can be stated in a single sentence that the embedding is elementary by stating it is induced by a $\kappa$-complete ultrafilter on $\kappa$ for some $\kappa$. Thus the proper axiom schema is in some cases equivalent to a single sentence.

When is this the case? Do there exist nontrivial elementary embeddings $j$ such that there is no sentence equivalent to "the class function $j$ is an elementary embedding"?

Answer 1

While not a complete answer, there is a paper by Mitchell Spector which deals with ultrapowers in $\sf ZF$.

Mitchell Spector, Ultrapowers without the axiom of choice, J. Symbolic Logic 53 (1988), no. 4, 1208--1219.

There he proves (Theorem 1), quite nicely, that the following are equivalent for an ultrapower embedding $j\colon\mathfrak M\to\mathfrak M^I/U$, where $I$ is some index set and $U$ is an ultrafilter on $I$, in $\frak M$:

1. In $\frak M$, if $f$ is a function on $I$, such that $f(x)\neq\varnothing$ $U$-a.e., then there is some $g$ such that $g(x)\in f(x)$ $U$-a.e.

2. Los theorem for the ultrapower embedding holds.

3. The embedding is elementary.

4. $\frak M$ and $\mathfrak M^I/U$ are elementarily equivalent.

5. $\mathfrak M^I/U$ satisfies the axiom of extensionality.

6. There is some $d\in\mathfrak M^I/U$, such that $\mathfrak M\models\forall x\forall y((y\in x\leftrightarrow y\in d)\rightarrow x=d)$.

The proof is quite simple, as all the forward implications are trivial. So it only remains to prove $6\implies 1$, and the proof is not hard to follow. (I was told the rest of the papers might contain mistakes, but this proof is quite simple and seems to be correct.)

---

So while I can't quite give you a complete answer, it seems that at least something can be said on ultrapower embeddings. It also means that if the axiom of choice for well-ordered families holds, then ultrapowers with measurable cardinals should be possible.