\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{elementary embedding}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{model_theory}{}\paragraph*{{Model theory}}\label{model_theory}

[[!include model theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{tarskivaught_test}{Tarski-Vaught test}\dotfill \pageref*{tarskivaught_test} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{elementary_embeddings_between_models_of_set_theory}{Elementary embeddings between models of set theory}\dotfill \pageref*{elementary_embeddings_between_models_of_set_theory} \linebreak
\noindent\hyperlink{in_material_set_theory}{In material set theory}\dotfill \pageref*{in_material_set_theory} \linebreak
\noindent\hyperlink{in_structural_set_theory}{In structural set theory}\dotfill \pageref*{in_structural_set_theory} \linebreak
\noindent\hyperlink{inconsistency}{Inconsistency}\dotfill \pageref*{inconsistency} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In [[model theory]], [[model|models]] of a [[first-order theory]] $T$ are certain kinds of [[functor|functors]] from the [[syntactic site]] of $T$ to $\mathbf{Set}$. Elementary embeddings are [[natural transformation|natural transformations]] between these functors.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

In [[model theory]], an \textbf{elementary embedding} between [[model|structures]] (over a given [[signature]] $\sigma$) is an [[injection]] that preserves and reflects all of [[first-order logic]] over $\sigma$. That is, it is an injection $f\colon M\to N$ such that for any first-order formula $\varphi$ written in the language of $\sigma$ and parameters $a_1,\dots,a_n\in M$ (of appropriate [[type]]s), we have

\begin{displaymath}
M \vDash \varphi(a_1,\dots,a_n) \;\iff\; N \vDash \varphi(f(a_1),\dots, f(a_n)).
\end{displaymath}
In particular, this implies that if either $M$ or $N$ is a [[model]] of some first-order [[theory]], then so is the other.

Note that the condition that $f$ be injective is automatic as long as the logic in question includes equality, since reflecting of the formula $x=y$ implies that $f$ is injective. If $f$ is (interpreted as) the inclusion of a [[subset]], we say that $M$ is an \textbf{elementary substructure} of $N$. We also say here that $N$ is an \textbf{elementary extension} of $M$.

More generally, when we consider structures in a [[category]] as in [[categorical logic]], a morphism $f\colon M\to N$ between structures in $C$ is an \textbf{elementary embedding} if for any formula $\varphi$, the following square is a [[pullback]]:

\begin{displaymath}
\itexarray{[\varphi]_M & \overset{}{\to} & [\varphi]_N\\
  \downarrow && \downarrow\\
  M A_1 \times\dots \times M A_n & \underset{}{\to} & N A_1 \times \dots \times N A_n}
\end{displaymath}
where $M A_i$ denotes the object of $C$ interpreting the type $A_i$, and $[\varphi]_M$ denotes the corresponding subobject in $C$ interpreting the truth value of the formula $\varphi$. Note that for an arbitrary morphism of structures, this square need not even commute; one sometimes says that $f$ is an \textbf{elementary morphism} if it does.

[[Urs Schreiber]]: let me try to say this more explicitly, to check if I am following:

The [[theory]] $T$ that we are modelling is exhibited by its syntactic category $Syn(T)$ with finite limits. A model of $T$ in a category $C$ with limits -- equivalently a $T$-structure in $C$ -- is a finite-limit preserving functor $N : Syn(T) \to C$. A morphism $f : M \to N : Syn(T) \to C$ of models is a [[natural transformation]] between such functors. We say that such a natural transformation is an \emph{elementary embedding} if its naturality squares on certain morphisms of $Syn(T)$ 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 $Syn(T)$ won't have the structure required to construct $[\varphi]$, and the structure wouldn't be preserved by the functors into $C$, 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.

In practice, it is also useful to separate out the weaker notion of \textbf{embedding}.

\begin{defn}
\label{}\hypertarget{}{}
Working over a fixed signature $\Sigma$, an injective homomorphism of structures $f: M \to N$ is an \emph{embedding} if for each relation $R \in \Sigma$ of arity $n$, we have $R_M = (f^n)^\ast R_N$, i.e., $R_M$ is obtained by pulling back the inclusion $R_N \hookrightarrow N^n$ along $f^n: M^n \to N^n$.

\end{defn}
Notice this is \emph{stronger} than just being an injective homomorphism (where we demand only that $R_M \hookrightarrow (f^n)^\ast R^n$, or that $R_M(a_1, \ldots, a_n) \vdash R_N(f(a_1), \ldots, f(a_n))$), and it is weaker than being an elementary embedding since here we are not demanding a pullback condition over all the formulas of the language, just the atomic ones (including equality, which is handled by injectivity as we noted earlier).

A \emph{substructure} is an embedding $f: M \to N$ where $f$ is a set-theoretic inclusion. (In [[structural set theory]], a substructure would just be an isomorphism class of embeddings.)

\hypertarget{tarskivaught_test}{}\subsection*{{Tarski-Vaught test}}\label{tarskivaught_test}

A simple criterion for when one structure is an elementary substructure of another is given by the Tarski-Vaught test. Let $L$ be the language (the set of first-order formulas) over some given signature.

\begin{prop}
\label{Tarski-Vaught}\hypertarget{Tarski-Vaught}{}
A substructure $i: M \hookrightarrow N$ is an elementary substructure if, whenever $\varphi$ is an $(n+1)$-ary formula and $b_1, \ldots, b_n \in M$, there exists $a \in N$ such that $\varphi(a, b_1, \ldots, b_n)$ is satisfied in $N$ only if there exists $c \in M$ such that $\varphi(c, b_1, \ldots, b_n)$ is satisfied in $M$.

\end{prop}
\begin{proof}
By induction on the structure of formulas $\varphi$, using $\neg, \wedge, \exists$ as primitive logical operators. The required pullback condition is satisfied on atomic formulas, by definition of substructure.

If the pullback condition is satisfied for $\varphi$ (of arity $n$ say), then it is trivially satisfied for $\neg \varphi$ because for all $\bar{a} = (a_1, \ldots, a_n) \in M^n$ we have

\begin{displaymath}
M \models \neg \varphi(\bar{a}) \;\; iff \;\; \not [M \models \varphi(\bar{a})] \;\; iff \;\; \not [N \models \varphi(i^n(\bar{a}))] \;\; iff \;\; N \models \neg\varphi(i^n(\bar{a})).
\end{displaymath}
If the pullback condition is satisfied for $\varphi$ and $\psi$, then it is equally trivially satisfied for $\varphi \wedge \psi$:

\begin{displaymath}
\itexarray{
M \models (\varphi \wedge \psi)(\bar{a}) & iff & M \models \varphi(\bar{a}) \; and \; M \models \psi(\bar{a}) \\ 
 & iff & N \models \varphi(i^n(\bar{a})) \; and \; N \models \psi(i^n(\bar{a})) \\ 
 & iff & N \models (\varphi \wedge \psi)(i^n(\bar{a})). 
}
\end{displaymath}
Using these two steps of the induction, we may say that given a substructure, the pullback condition is satisfied for all quantifier-free formulas in the language.

Finally, suppose the pullback condition is satisfied for $(n+1)$-ary formulas $\varphi(v, \bar{w})$. If $\bar{b} \in (\exists_v \varphi)_M$, then there exists $c \in M$ such that $(c, \bar{b}) \in \varphi_M$, whence there exists $a = i(c)$ such that $(i(c), i^n(\bar{b})) \in \varphi_N$, so $i^n(\bar{b}) \in (\exists_v \varphi)_N$, just using the fact that $i$ is a homomorphism. Conversely: if $i^n(\bar{b}) \in (\exists_v \varphi)_N$, i.e., if there exists $a \in N$ such that $(a, i^n(\bar{b})) \in \varphi_N$, then by hypothesis there exists $c \in M$ such that $(c, \bar{b}) \in \varphi_M$, i.e., $\bar{b} \in (\exists_v \varphi)_M$. This completes the inductive proof.

\end{proof}
\begin{example}
\label{}\hypertarget{}{}
In the theory of [[real closed fields]] with signature $(0, 1, +, \cdot, \leq)$, the field of real algebraic numbers is an elementary substructure of the field of real numbers. This follows from the Tarski-Vaught test and the [[Tarski-Seidenberg theorem]] which establishes quantifier elimination over the language generated by the signature (every formula has the same extension as some quantifier-free formula).

\end{example}
Another application is described at [[Löwenheim-Skolem theorem]].

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\begin{prop}
\label{Elementary}\hypertarget{Elementary}{}
Let $T$ be a [[first-order theory]], and $M, N : \mathsf{Syn}(T) \to \mathbf{Set}$ two [[models]] of $T$.

Let $(\mathsf{Syn}(T))_0$ denote the objects (definable sets of $T$) of $\mathsf{Syn}(T)$.

A $(\mathsf{Syn}(T))_0$-indexed collection of maps $f \overset{df}{=} \left(M(X) \overset{f_X}{\to} N(X) \right)_X$ is a [[natural transformation]] if and only if it preserves and reflects [[first-order logic]].

\end{prop}
\begin{proof}
Suppose $f$ is a natural transformation. Then certainly whenever $X$ is a definable set, $x \in M(X) \implies f(x) \in N(X).$

If $f(x) \in N(X)$ but $x$ is \emph{not} in $M(X)$, then $x \in M(\neg X)$, which implies $f(x) \in N(\neg X)$. Since the functor $N$ preserves disjoint unions, $N(\neg X) \cap N(X)$ is empty, which is impossible. So whenever $f(x) \in N(X)$, $x \in M(X)$.

Now suppose $f$ preserves and reflects first-order logic. If $X \overset{\gamma}{\to} Y$ is a map in $\mathsf{Syn}(T)$ and $y \in M(Y)$, then

\begin{displaymath}
M \models \gamma(y) \in M(X) \iff N \models \gamma(f(y)) \in N(X)
\end{displaymath}
and $\gamma(f(y)) = f(\gamma(y))$ since

\begin{displaymath}
M \models \Gamma(y,\gamma(y)) \iff N \models \Gamma(f(y), f \gamma(y))
\end{displaymath}
where $\Gamma$ is the graph of the definable function $\gamma$.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
In the above, we can actually weaken the assumption that we start with a collection of $(\mathsf{Syn}(T))_0$-indexed maps to just starting with a collection of maps $f_C : M(C) \to N(C)$, where $C$ runs along the maximal objects (the [[types]]) in $\mathsf{Syn}(T)$.

Then: the $(\mathsf{Syn}(T))_0$-indexed collection of \emph{pullbacks} along the canonical embeddings $N(X) \hookrightarrow N(C)$ is a natural transformation $M \to N$ if and only if the maps $f_C$ preserved and reflected first-order logic.

\end{remark}
\hypertarget{elementary_embeddings_between_models_of_set_theory}{}\subsection*{{Elementary embeddings between models of set theory}}\label{elementary_embeddings_between_models_of_set_theory}

\hypertarget{in_material_set_theory}{}\subsubsection*{{In material set theory}}\label{in_material_set_theory}

Elementary embeddings play an important role in the study of [[large cardinals]] in (material) [[set theory]].

For instance, the existence of a [[measurable cardinal]] is equivalent to the existence of a non-[[surjection|surjective]] elementary embedding $j\colon V\to M$, where $V$ is the universe of sets and $M$ is some [[transitive set|transitive]] model of [[ZF]]. If $\kappa$ is a measurable cardinal with a countably-complete [[ultrafilter]] $\mathcal{U}$, we can form the [[ultrapower]] $V^{\mathcal{U}}$ and then take its [[transitive collapse]] to produce $M$. (Countable completeness of $\mathcal{U}$ is necessary for $V^{\mathcal{U}}$ to be well-founded and thus have a transitive collapse.)

Conversely, if $j\colon V\to M$ is a nontrivial elementary embedding, it must have a \emph{critical point}, i.e. a least ordinal $\kappa$ such that $j(\kappa)\neq \kappa$. It follows that $j(\kappa)$ is some [[ordinal]] $\gt \kappa$, so in particular $\kappa\in j(\kappa)$ (using the von Neumann definition of ordinals). Define $\mathcal{U}\subset P(\kappa)$ by $A\in \mathcal{U}$ iff $\kappa\in j(A)$; then $\mathcal{U}$ is a $\kappa$-complete ultrafilter on $\kappa$.

Stronger large cardinal axioms can be characterized, or defined, as the critical points of elementary embeddings satisfying additional closure axioms on the transitive class $M$.

\hypertarget{in_structural_set_theory}{}\subsubsection*{{In structural set theory}}\label{in_structural_set_theory}

Any elementary embedding of models of ZF induces a [[conservative functor|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.

\hypertarget{inconsistency}{}\subsubsection*{{Inconsistency}}\label{inconsistency}

The ``ultimate'' closure property, hence the ``strongest'' large cardinal axiom, would be having a nontrivial elementary embedding $j\colon V\to V$ (i.e. $M$ is all of $V$). Sometimes the critical point of such an embedding, if one exists, is called a \emph{Reinhardt cardinal}. However, having such an e.e. turns out to be inconsistent\ldots{}sort of.

The technicality is that because any e.e. $V\to V$ is a [[proper class]], the proposition ``there does not exist an e.e. $V\to V$'' cannot be stated in ZF (one cannot quantify over proper classes). What we can prove is the following meta-theorem (one instance per formula $\varphi(x,y)$ that might define an e.e.).

\begin{utheorem}
For any formula $\varphi(x,y,z)$ and any set $a$, it is not true that defining $j_a(x)=y \iff \varphi(x,y,a)$ makes $j_a$ into an elementary embedding $V\to V$.

\end{utheorem}
\begin{proof}
Suppose that $\varphi$ and $a$ exist. Fix such a $\varphi$. Fix $\lambda$ as the smallest ordinal such that there exists an $a\in V_\lambda$ such that $\varphi(-,-,a)$ defines an e.e. $V\to V$. Now the statement ``$\lambda$ is the smallest ordinal such that there exists an $a\in V_\lambda$ such that $\varphi(-,-,a)$ defines an e.e. $V\to V$.'' is definable in the language of ZF (definability of the property ``is an e.e. $V\to V$'' is tricky, but true). Therefore, if $b$ is any set such that $j_b$ is an e.e., it preserves the truth of this, so it is also true that $j_b(\lambda)$ is the smallest ordinal such that there exists an $a\in V_{j_b(\lambda)}$ such that $\varphi(-,-,a)$ defines an e.e. $V\to V$. This clearly implies that $j_b(\lambda)=\lambda$.

Now define $\kappa$ to be the smallest ordinal which is a critical point of an e.e. $V\to V$ of the form $j_a$ for some $a\in V_\lambda$. Let $b\in V_\lambda$ be such that $j_b$ is an e.e. $V\to V$ and $\kappa$ is the critical point of $j_b$. The definition of $\kappa$ is again a definable property, so it follows that $j_b(\kappa)$ is the smallest ordinal which is a critical point of an e.e. $V\to V$ of the form $j_a$ for some $a\in V_{j_b(\lambda)} = V_\lambda$. Therefore, $\kappa= j_b(\kappa)$, a contradiction to $\kappa$ being the critical point of $j_b$.

\end{proof}
Now, if we work instead in a theory such as [[NBG]] or [[MK]] which can contain \emph{non-definable} proper classes, in theory there might still be an e.e. $V\to V$ which is not definable. One can also access such an idea by adding a new symbol ``$j$'' 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]].

[[!redirects elementary substructure]] [[!redirects elementary submodel]] [[!redirects elementary morphism]] [[!redirects elementary embeddings]] [[!redirects elementary substructures]] [[!redirects elementary submodels]] [[!redirects elementary morphisms]] [[!redirects elementary extension]]



\end{document}