省略型定理

模型论中的定理，是证明模型存在或构造模型的一种方法。

设是一阶语言L的模型。∑(x，…，x)是L中一公式集，其中自由变元都在x，…，x中。如果存在a，…，a∈A使得对每一φ(x，…，x)∈∑(x，…，x)都有φ(x，…，x)［a，…，a］，

则称∑在中可满足或称实现∑。否则称省略∑。如果存在L的模型能实现∑，则称∑为协调的。如果∑(x．…，x)是极大的协调公式集，则称∑(x，…，x)为一个型。

设T是L中的理论，∑(x，…，x)是L中的公式集。如果T有一模型能实现∑(x，…，x)，称∑(x，…，x)与T协调。如果存在L中的公式φ(x，…，x)，能使｛φ｝与T协调，并且每一φ(x，…，x)∈∑(x，…，x)，都有Tx，…，x(φ(x，…，x)→φ(x，…，x))，则称T局部实现∑。如果T不能局部实现∑，则称T局部省略∑。易证：如果T有一模型省略∑，则T局部省略∑。

省略型定理设T是可数语言L中的协调理论，∑(x，…，x)是L中的公式集。如T局部省略∑，则T有一可数模型省略∑。

广义省略型定理 设T是可数语言L中的协调理论，∑(x，…，x)是L上的公式集(r=1，2，3…)。如果T局部省略第一∑，则T有一可数模型省略每一∑。

省略型定理与力迫法有密切联系，二者有共同的基础。