模型论中的省略类型定理 1. 基本概念：型（type）与实现 在模型论中，给定一阶语言 \(\mathcal{L}\) 和其一个理论 \(T\)，一个 型 是一组公式的集合，这些公式共享有限个自由变量。具体来说，一个 \(n\)-型 是含 \(n\) 个自由变量 \(x_ 1, \dots, x_ n\) 的公式集 \(\Sigma(\bar{x})\)。若存在模型 \(\mathcal{M} \models T\) 和元素 \(\bar{a} \in M^n\) 满足 \(\mathcal{M} \models \phi(\bar{a})\) 对所有 \(\phi \in \Sigma\) 成立，则称 \(\mathcal{M}\) 实现 了型 \(\Sigma\)。 2. 完全型与型空间 若一个型 \(\Sigma(\bar{x})\) 是 极大一致的 （即对任意公式 \(\phi(\bar{x})\)，要么 \(\phi \in \Sigma\) 要么 \(\neg \phi \in \Sigma\)），则称其为 完全型 。所有完全 \(n\)-型构成的集合记为 \(S_ n(T)\)，称为 型空间 ，其拓扑基由集合 \([ \phi] = \{ p \in S_ n(T) \mid \phi \in p \}\) 生成。 3. 省略型定理的直观描述 省略型定理关注：能否构造一个模型，使其 不实现 某个指定的型。若型 \(\Sigma\) 是 非主型 （即不被任何单个公式蕴含），则存在 \(T\) 的模型省略 \(\Sigma\)，即该模型中没有任何元组满足 \(\Sigma\) 的所有公式。 4. 关键定义：主型与非主型 型 \(\Sigma(\bar{x})\) 是 主型 （或孤立型），若存在公式 \(\phi(\bar{x})\) 使得 \(T \cup \{\phi(\bar{x})\}\) 逻辑蕴含 \(\Sigma\) 的所有公式（即 \(\phi\) 是 \(\Sigma\) 的 生成公式 ）。 若型不是主型，则称为 非主型 （或省略型）。 5. 定理的精确表述 省略型定理 ：设 \(T\) 是可数语言中的一致理论，\(\Sigma(\bar{x})\) 是一个非主 \(n\)-型。则存在 \(T\) 的可数模型 \(\mathcal{M}\)，其省略 \(\Sigma\)，即对任意 \(\bar{a} \in M^n\)，存在 \(\phi \in \Sigma\) 使得 \(\mathcal{M} \not\models \phi(\bar{a})\)。 6. 证明思路（亨金构造法） 扩展语言：向语言中加入可数个新常数符号 \(\{c_ 1, c_ 2, \dots\}\)，用于构建模型的域。 构造完全理论：通过枚举所有公式，逐步添加公式到理论中，确保： （1）最终理论一致； （2）对每个存在公式 \(\exists x \psi(x)\)，添加某个 \(\psi(c_ i)\)； （3）避免实现 \(\Sigma\)：对每个元组的新常数，添加一个公式 \(\neg \phi(\bar{c})\)，其中 \(\phi \in \Sigma\)。 利用非主型的性质：因 \(\Sigma\) 无生成公式，总可避免满足整个 \(\Sigma\)。 从完全理论生成模型：项模型由新常数构成，其满足所有添加的公式，从而省略 \(\Sigma\)。 7. 推广与应用 可数模型定理 ：若 \(T\) 只有可数模型，则每个可数模型省略所有非主型。 型省略与模型分类 ：例如，无原子布尔代数的可数模型均同构，因其省略所有主型。 与洛文海姆-斯科伦定理的关系 ：省略型定理进一步约束模型的结构，用于研究模型的唯一性。 8. 示例：稠密线性序的无端点模型 理论 \(T\) 描述可数无端点稠密线性序（如 \(\mathbb{Q}\)）。其完全 1-型包括： 主型：由公式 \(x = c\) 生成（被所有元素实现）； 非主型：如“\(x\) 是无穷大”型（无生成公式）。 通过省略型定理，可构造 \(T\) 的模型省略此类非主型，但此时所有可数模型均同构于 \(\mathbb{Q}\)，故实际上每个非主型均被省略。