初等嵌入

初等嵌入保留带参数的一阶信息：把 $\mathcal{M}$ 的元素搬进 $\mathcal{N}$ 之后，凡是一阶语言能以这些元素为参数提出的问题，不管量词嵌套多深，两边答案都一致。

关键在于存在见证。普通嵌入只保证搬过去的元素之间的原子关系不变，但大结构可能用新增元素满足某个存在式，而小结构内部没有相应见证。初等性排除了这项落差：以小结构元素为参数的存在要求，只要在大结构中可实现，在小结构中也必须可实现。

初等等价只比较不带参数的句子；初等嵌入还要让一个指定映射保留每组参数的公式真值。因此，仅知道两个结构满足相同句子，并不能判断某个给定映射是否初等。

有理数有序域 $(\mathbb{Q},+,\cdot ,<)$ 包含于实数有序域，包含映射保持加法、乘法与序，是普通嵌入；但公式 $\phi (x)=\mathrm{\exists }y(y\cdot y=x)$ 取参数 $2\in \mathbb{Q}$ 后，在 $\mathbb{R}$ 中真、在 $\mathbb{Q}$ 中假，故不是初等嵌入。

只保留序语言 $\{<\}$ 时，$(\mathbb{Q},<)$ 到 $(\mathbb{R},<)$ 的包含映射却是初等的。核验分两步：无端点稠密线性序的量词消去公理库稠密线性序的量词消去Quantifier elimination for dense linear orders · DLO 量词消去在无端点稠密线性序中，以所有下界小于所有上界消去存在量词，并构造避开有限禁点的见证。把任意带有理数参数的公式换成同语言的无量词公式；包含映射保持这些参数间的大小、相等与其布尔组合，因此保持消去后的公式，也就保持原公式。这项证明同时使用两者都是 DLO 模型以及语言只有 $<$，不能套用到前面的有序域例子。

另一族系统性的正例来自超积公理库超积Ultraproduct按超滤子诱导的等价关系对一族结构的直积取商所得的结构。：Łoś 定理公理库Łoś 定理Łoś theorem · Fundamental theorem of ultraproducts超积中一阶公式成立，当且仅当其分量成立的指标集合属于所用超滤子。保证任意结构到其超幂的对角嵌入初等。

边界处有两组必须分开的概念。其一，初等等价 $\mathcal{M}\equiv \mathcal{N}$（满足相同句子）严格弱于初等嵌入的存在：$(\mathbb{R},<)$ 与 $(\mathbb{Q},<)$ 初等等价，但基数原因使 $\mathbb{R}$ 连单射进 $\mathbb{Q}$ 都不可能；即使两结构同构，具体给定的嵌入也可以不初等——$(2\mathbb{Z},<)\subseteq (\mathbb{Z},<)$ 中两结构同构（各自都是离散无端点线性序，且 $n\mapsto 2n$ 是同构），而包含映射不初等，因为"$0$ 与 $2$ 之间存在元素"在大结构中真、在子结构中假。初等性是对映射的属性，不是对结构对的属性。其二，验证初等性可用下面的见证条件。

Tarski–Vaught 检验 ​

先假定 $\mathcal{M}$ 是 $\mathcal{N}$ 的子结构：它包含常元、对函数运算封闭，并把关系解释限制在 $M$ 上。此时 $\mathcal{M}\preccurlyeq \mathcal{N}$ 当且仅当对每个公式 $\psi (x,\overline{y})$ 和每组参数元组 $\overline{a}\in M^{|\overline{y}|}$，

见证 $b$ 要来自小论域，但这个检验中的公式仍在大结构 $\mathcal{N}$ 中求值。[4]

初等子结构显然满足该条件。反向对公式归纳：原子式由子结构条件保持并反映，布尔步骤随即成立。若 $\mathcal{N}\models \mathrm{\exists }x\psi (x,\overline{a})$，检验给出 $b\in M$ 且 $\mathcal{N}\models \psi (b,\overline{a})$；对 $\psi$ 的归纳假设便给出 $\mathcal{M}\models \psi (b,\overline{a})$，故小结构也满足存在式。反过来，小结构的见证经归纳假设仍是大结构的见证。存在量词与布尔步骤涵盖全部公式，从而证明初等性。

初等嵌入是模型论的中心运算。向下与向上的 Löwenheim–Skolem 定理公理库Löwenheim–Skolem 定理Löwenheim–Skolem theorem有无限模型的一阶理论在适当基数上存在较小或较大的模型。产出的正是给定结构的各种基数的初等子结构与初等扩张，Tarski–Vaught 检验加 Skolem 函数是其引擎；初等链的并定理公理库初等链与ω饱和扩张Elementary chain theorem · Omega-saturated elementary extension证明初等链的并保持一阶真值，迭代实现有限参数类型构造ω饱和扩张，并给出可数语言仍迫使不可数模型的例子。通过公式归纳处理存在见证，继而迭代实现有限参数类型，完整构造ω饱和扩张；可数语言不保证该扩张可数。经由超幂，初等嵌入连接紧致性论证与非标准分析——实数到超实数的嵌入初等，故"传递原理"成立：一阶性质在标准与非标准世界间自由往返。

进阶边界： 在集合论中，带有额外闭包条件的非平凡初等嵌入 $j:V\to M$ 用来刻画可测基数等大基数；其临界点和目标模型的闭包性质决定公理强度。这里涉及真类、超滤与良基超幂等额外框架，不能把普通结构之间的初等嵌入结论直接照搬过去。