模型论中的省略型定理 我们先从“型”这个概念开始。在模型论中，一个“型”可以看作是对一个（或一组）尚未确定的元素可能具有的所有性质的描述。更精确地说，设 M 是一个 L-结构，A 是 M 的一个子集。对于一个变量组 x，一个（关于 A 的）n-型 p(x) 是一组公式 φ(x)，其参数来自 A，并且这个集合在 M 的某个初等扩张中是可实现的（即存在元素 b 使得 M 满足所有 φ(b)）。如果这个型在 M 本身中就可实现，我们称 M 实现了 p。如果 M 没有实现 p，我们就说 M 省略了 p。 接下来是“局部可实现”的概念。一个型 p(x) 在理论 T 中是局部可实现的，如果对于 p(x) 的任意有限子集 p_ 0(x)，都存在一个模型 M_ 0 满足 T，并且 M_ 0 实现了 p_ 0(x)。换句话说，这个型的每一个有限部分都能找到模型来实现它。这是型可实现的必要条件，但远非充分条件。 现在我们可以引入“省略型定理”本身了。这个定理提供了一个充分条件，保证一个理论存在一个模型，它省略了某个给定的型。定理的经典表述如下：设 T 是一个可数的完全一阶理论，p(x) 是一个 n-型。如果 p(x) 在 T 中不是孤立的（即不存在一个公式 ψ(x) ∈ p(x) 使得 T ∪ {ψ(x)} 能推导出 p(x) 中的所有公式），那么 T 存在一个可数模型 M，该模型省略了 p(x)，即 M 中没有元素组满足 p(x) 中的所有公式。 理解这个定理的关键在于“孤立公式”的概念。一个型 p 如果被一个公式 ψ 所孤立，那么 ψ 就像是这个型的“指纹”或“代表”，任何满足 ψ 的元素都必然满足整个型 p。因此，如果一个型不是孤立的，就意味着你找不到这样一个强有力的公式来“锁定”整个型，这就为构造一个有意避开实现该型的模型留下了空间。证明通常使用亨金构造的一种变体，在逐步构建模型论域的同时，小心地避免实现目标型中的任何公式。 最后，我们来看一个重要的推广：可数理论 T 可以同时省略一组可数个型 {p_ i (x_ i)}，只要每个型 p_ i 在 T 中都不是孤立的。这个推广的省略型定理在模型论中具有深远的影响，例如，它可以用来证明任何可数的模型都可以初等嵌入到一个可数的质模型（omitting types theorem is a key step in proving the existence of prime models for countable atomic theories）。