In model theory, an elementary embedding between structures is an injection that preserves and reflects all of first-order logic. That is, it is an injection such that for any first-order formula and parameters (of appropriate types), we have
Note that the condition that be injective is automatic as long as the logic in question includes equality, since reflecting of the formula implies that is injective. If is (interpreted as) the inclusion of a subset, we say that is an elementary substructure of .
where denotes the object of interpreting the type , and denotes the corresponding subobject in interpreting the truth value of the formula . Note that for an arbitrary morphism of structures, this square need not even commute; one sometimes says that is an elementary morphism if it does.
Urs Schreiber: let me try to say this more explicitly, to check if I am following:
The theory that we are modelling is exhibited by its syntactic category with finite limits. A model of in a category with limits – equivalently a -structure in – is a finite-limit preserving functor . A morphism of models is a natural transformation between such functors. We say that such a natural transformation is an elementary embedding if its naturality squares on certain morphisms of are pullback squares.
Mike Shulman: Not quite. First of all, the definition officially happens at the more general level of structures rather than models, but we can of course consider those as models for the empty theory. And whether we need finite-limit categories and functors, or something else like regular ones, geometric ones, or Heyting ones, depends on what fragment of logic we consider our (possibly empty) theories as living in. Your rephrasing is correct if we mean finitary first-order theories and therefore Heyting categories and Heyting functors. Otherwise, the syntactic category won’t have the structure required to construct , and the structure wouldn’t be preserved by the functors into , so that we wouldn’t even have naturality squares to ask to commute (I alluded to this in the last sentence above).
I think I didn’t explain this very well, but I have to go now, I’ll try to come back to it later and rewrite it to make more sense.
For instance, the existence of a measurable cardinal is equivalent to the existence of a non-surjective elementary embedding , where is the universe of sets and is some transitive model of ZF. If is a measurable cardinal with a countably-complete ultrafilter , we can form the ultrapower and then take its transitive collapse? to produce . (Countable completeness of is necessary for to be well-founded and thus have a transitive collapse.)
Conversely, if is a nontrivial elementary embedding, it must have a critical point, i.e. a least ordinal such that . It follows that is some ordinal , so in particular (using the von Neumann definition of ordinals). Define by iff ; then is a -complete ultrafilter on .
Stronger large cardinal axioms can be characterized, or defined, as the critical points of elementary embeddings satisfying additional closure axioms on the transitive class .
Any elementary embedding of models of ZF induces a conservative logical functor between their categories of sets. In fact, it is much more than that; a conservative logical functor preserves and reflects only first-order logic with bounded quantifiers, while an e.e. preserves and reflects all first-order logic.
The structural meaning of elementary embeddings seems not to be well-explored.
The “ultimate” closure property, hence the “strongest” large cardinal axiom, would be having a nontrivial elementary embedding (i.e. is all of ). Sometimes the critical point of such an embedding, if one exists, is called a Reinhardt cardinal. However, having such an e.e. turns out to be inconsistent…sort of.
The technicality is that because any e.e. is a proper class, the proposition “there does not exist an e.e. ” cannot be stated in ZF (one cannot quantify over proper classes). What we can prove is the following meta-theorem (one instance per formula that might define an e.e.).
For any formula and any set , it is not true that defining makes into an elementary embedding .
Suppose that and exist. Fix such a . Fix as the smallest ordinal such that there exists an such that defines an e.e. . Now the statement “ is the smallest ordinal such that there exists an such that defines an e.e. .” is definable in the language of ZF (definability of the property “is an e.e. ” is tricky, but true). Therefore, if is any set such that is an e.e., it preserves the truth of this, so it is also true that is the smallest ordinal such that there exists an such that defines an e.e. . This clearly implies that .
Now define to be the smallest ordinal which is a critical point of an e.e. of the form for some . Let be such that is an e.e. and is the critical point of . The definition of is again a definable property, so it follows that is the smallest ordinal which is a critical point of an e.e. of the form for some . Therefore, , a contradiction to being the critical point of .
Now, if we work instead in a theory such as NBG or MK which can contain non-definable proper classes, in theory there might still be an e.e. which is not definable. One can also access such an idea by adding a new symbol “” to ZF and asserting that it is an e.e. However, it was shown by Kunen in 1971, using a technical combinatorial argument, that the existence of such an e.e. is inconsistent with the axiom of choice. It is unknown whether it is consistent with ZF.