Formalizing Elementary Embeddings and Substructures in ZFC

Question

The concept of elementary embedding is very important in the definition of several large cardinals ideas. The usual model-theoretic definition can not be expressed for some of these ideas within $\text{ZFC}$. There are various tricks to give satisfactory formalization of these ideas. My question is what are the usual ways of expressing concepts like elementary embedding?

For example, how would one express in $\text{ZFC}$ that a (class) function $j : M \rightarrow N$ is an elementary embedding between two (class) transitive structures. Of course, since $j$, $M$, and $N$ may be proper classes, these three will be expressed using their defining formulas; however, still the general satisfaction relation is not expressible. (However, I believe for any $n \in \omega$, the satisfaction relation for $\Sigma_n$ formulas of set theory is definable.)

Other troubling examples are expression that seem to quantify over elementary embeddings and inner models. For instance, in ZFC, it is provable that $\kappa$ is a measurable cardinal if and only if there is an inner model $M$ and an elementary embedding $j : V \rightarrow M$ with critical point $\kappa$. In the case of the measurable cardinal, perhaps the quantification could be replaced by quantifying over ultrafilter with certain properties since the $M$ can be taken to be Mostowski collapse of ultrapowers of $V$; however, is there a general way of expressing statements like the above that appear to quantify over elementary embeddings and inner models?

Also, one uses set elementary substructure of $V$ in $ZFC$. Just in ZFC, this is not possible since there are not even models of $ZFC$. However, often it suffices to consider substructures that are "sufficiently elementary". That is, it would be enought to have a set structure $X$ such that $X \prec_{\Sigma_n} V$. For any $n$, does such a set $\Sigma_n$-elementary substructure of $V$ always exists? This appears to be like the reflection principle for cumulative hierarchies (like $\{V_\alpha\}$ and $\{H_\alpha\}$); however, the form of the reflection principle I am familiar with from Kunen gives elementary substructures with respect to only finitely many formulas.

Thanks for any information that you can provide.

Answer 1

Proposition 5.1 in Kanamori's Higher Infinite provides the answer to one major part of your question:

If $j:M_1\to M_2$ is a $\Sigma_1$-elementary embedding between inner models, then it is an elementary embedding.

Hence you can define in ZFC what elementary embeddings are, at least between inner models, but that is usually what we want.

As for the question about quantification over elementary embeddings, here it is often enough to consider initial parts (sets) of the inner models and of the embeddings. This is the case in the statement about the existence of a measurable cardinal that you mention:

There is a measurable cardinal if there is a non-trivial elementary embedding of some $V_\alpha$ into a subclass of $V_\alpha$ (with critical point $<\alpha$). Or you can phrase this theorem as a schema of theorems: if a formual $\varphi$ defines a (nontrivial) elementary embedding, then there is a measurable cardinal.

In some cases you may be able to restrict your attention to embeddings that are coded by sets in a uniform way such as the ultrapower embeddings in the case of measurable cardinals.

Answer 2

(1) One approach to large cardinal embeddings is to view literal talk about them as "from the outside" about models of set theory, while knowing that particular properties of particular embeddings can often be formalized within the language of set theory in various ways. The simplest example is a measurable cardinal which is equivalent to the existence of a countably complete ultrafilter.

Another approach is to add predicates to the language for $j$ and $M$, expanding the language and usually expanding the axioms like adding instances of comprehension that refer to $j$. This is one way to capture the full content of Kunen's inconsistency theorem.

(2) $\Sigma_n$ truth is formalizable within ZF for any $n$, and we can combine this with reflection to get set-sized $\Sigma_n$ elementary substructures of the universe.