2.8. 型与量词消去
这一节, 我们来讨论模型中是否有满足我们所想要的性质的对象. 首先, 我们来看型这一概念的定义.
定义 2.8.0.1 (有序元素组的型). 对语言 的结构 中的一个有限有序元素组 , 我们定义其型为 .
评注. 换言之, 我们将 中的 满足的全部性质收集在一起. 然而, 更多的时候我们想脱离具体的 而只看这一集公式, 因此我们需要另外的定义.
定义 2.8.0.2 (理论的完全型). 对语言 的理论 , 一个公式集 若满足存在模型 和其中的有限有序元素组 使得 , 则称 是理论 的完全 型, 全体完全 型的集记为 .
定义 2.8.0.3 (实现与省略). 对语言 中的一族 自由变元句子集 , 若结构 中存在一个有限有序元素组 使得 , 则称 在 中实现了 , 有时也称作 实现了 . 如果不存在实现 的 , 则称 省略了 .
定义 2.8.0.4 (理论的部分型). 对语言 的理论 , 若存在模型 实现一族 自由变元句子集 , 则称 是 的部分 型.
我们接下来指出这些定义的命名中暗示的定理.
定理 2.8.0.5. 一个 是部分型当且仅当它是一个完全型的子集; 一个部分型 是完全型当且仅当它是极大部分型 (换言之向其中加入任何公式后均不再构成部分型).
然而, 部分型最厉害的地方在于, 它也有一个紧致性定理.
定理 2.8.0.6. 一个 是部分型, 当且仅当它的每个有限子集都是部分型.
对于完备理论, 我们还可以加强这个紧致性定理, 只在某一个模型中考虑, 这显然是因为它的所有模型都是初等等价的.
定理 2.8.0.7. 如果有完备理论 的模型 , 则:
1. | 是部分型, 当且仅当它的每个有限子集都在 中被实现. |
2. |
|
证明. 对第一个, 显然只要证明每个有限部分型被实现当且仅当在 中被实现; 这是初等等价性带来的.
构成一个有趣的拓扑空间, 我们将发现紧致性定理确实谈论了这个空间的紧致性.
定义 2.8.0.8 (型的空间). 在 中, 由全体公式 定义的 为基自然生成 上的一个拓扑.
定理 2.8.0.9. 是紧致 完全不连通零维空间, 开闭基就是这些 .
其实, 我们初始版本的紧致性定理也可以变成一个拓扑空间的紧致性.
定义 2.8.0.10. 全体完备一致 理论的集合 上, 由全体句子 定义的 为基自然生成 上的一个拓扑.
定理 2.8.0.11. 是紧致 完全不连通零维空间, 开闭基就是这些 .
我们定义的两种 型有两种可能的扩展定义: 一种是允许更多的变元, 一种是允许临时扩张语言. 我们现在来讨论这两者. 首先, 我们介绍可定义的概念.
定义 2.8.0.12. 对 结构 , 给定 和 , 我们可以定义 的 可定义子集的集族为 . 我们更细致地称公式 与参数 在 上定义了 .
对 , 我们定义其可定义闭包为 , 定义其代数闭包为 .
定理 2.8.0.13. ,
证明. 我们自然可以直接验证, 但这里有一种更优雅的方式, 我们可以指出它们甚至是有限闭包算子.
定义 2.8.0.14. 称闭包算子 是有限的, 若 指出存在有限子集 满足 .
称闭包算子 满足交换性质, 若 时必有 .
一个集合 连同其上一个满足交换性质的有限闭包算子称作一个拟阵. 此时这个闭包算子又常常记为 .
引理 2.8.0.15. 如果一个 是有限、单调、单增的, 且满足 , 则 是有限闭包算子.
现在我们来验证 有限且满足上引理的条件. 事实上, 有限是因为定义只用到有限个参数, 上引理的条件则可通过考虑最小的包括 的有限可定义集, 用其中的全体元素来模糊 即可.
定理 2.8.0.16. 如果 , 且 , 则 , .
推论 2.8.0.17. 若 , 则 .
现在回到对型的处理上.
定义 2.8.0.18. 对指标集 和语言 的结构 中的一个以 为指标的元素组 , 我们定义其型为 .
我们同理定义完全 型与部分 型. 注意, 我们默认了语言的变元集有一子集以 为指标集, 因此必须放弃语言的变元集可数的假设.
对语言 的结构 中的一个有限有序元素组 和子集 , 我们定义其型为 , 这里 是加入了全体 中元素为常元的语言 的公式.
其余定义同理.
这两个延伸定义都是相当自然的. 第一种延伸定义用得较少, 我们现在用第二种延伸定义来讨论集合的型.
定义 2.8.0.19. 对 结构 的子集 , 我们称理论 的部分型与完全型为 的部分型与完全型, 全体完全 型构成的空间记为 . 这里 是 作为扩张语言 的结构的理论.
由于 自动的是完备一致理论, 我们同 一样有以下这些结果.
定理 2.8.0.20. 以下定理对 同样成立.
1. |
|
2. | 公式集是部分型, 当且仅当它的每个有限子集都在 中被实现, 当且仅当它是一个完全型的子集. 完全型是极大部分型. |
3. | 是一个紧致 完全不连通零维空间. |
最后, 我们来给出著名的省略型定理, 它指出非主型总是被某个模型省略. 首先仍然来看基础的定义.
我们先对集合的型定义主型. 固定一个可数语言 的结构 的子集 .
定义 2.8.0.21. 如果完全型 对应的 是开闭集, 则称 是主型. 换言之, 若存在 使得 , 则 是主型. 不是主型的型称作非主型.
定理 2.8.0.22. 每个主型都在 中实现.
定义 2.8.0.23. 如果完全型 对应的 是开闭集, 则称 是主型.
定理 2.8.0.24. 每个主型都在每个 的模型中实现.
定理 2.8.0.25 (省略型定理). 如果有一列非主型 , 则存在 的可数模型 省略其中每个型.
证明. 我们向 中加入一列常元 , 得到一个新的语言 . 令 中全体延伸一开始的理论 的完备理论 形成一个空间 . 事实上由于这始终是可数语言, 它就是 , 因而是个紧致 完全不连通零维空间.
我们用这列 来讨论 的见证性.
定义 2.8.0.26. 称 的理论 对常元组 具有见证性, 若对每个公式 , 时均有一个 使得 .
引理 2.8.0.27. 在 中, 全体对 具有见证性的理论 构成的集合 是余第一纲集.
证明.
接下来, 我们考虑 , 每个 都给出一个 , 它只保留变元为 的那些公式. 、
引理 2.8.0.28. 是连续函数, 且将开闭集映为开闭集.
证明.
接下来, 我们来看看谁不被实现.
引理 2.8.0.29. 对非主型 , 存在余第一纲集 使得对每个 , 此时的任何 均让 不被 实现.
证明.
我们来讨论理论的一种重要性质, 它允许我们用简单的无量词句子代替复杂的可能带量词的任意句子.
定义 2.8.0.30. 我们称理论 具有量词消去, 若对任意公式 均有无量词公式 满足 .
定理 2.8.0.31. 考虑量词消去的理论 的两个模型 .
1. | 任何嵌入 都是初等嵌入. |
2. | 是 的子结构时, 也是 的初等子结构. |
定义 2.8.0.32 (无量词型). 对语言 的结构 中的一个有限有序元素组 , 我们定义其无量词型为 无量词 .
类似定义理论的无量词完全型与无量词部分型, 以及带有定义集 的无量词型等等. 无量词完全 型构成的空间记为 .
定理 2.8.0.33. 给定两个 结构 与 , 指定两个 元组 和 , 则 当且仅当存在同构 , 使得 .
证明. 这里的 指的是 作为 的子集时生成的子结构, 不难观察到它事实上就是全体 变元项 实现在 上后获得的所有 构成的集.
无量词型相等时, 记 , 则 就是我们想要的同构, 这是因为:
1. |
|
2. |
|
定理 2.8.0.34. 对理论 , 以下两个论断等价.
1. | 具有量词消去. |
2. | 任给 两个模型 中的 元组 均有 |
证明. 我们来考虑一个典范的 , 它将 送到 . 我们现在来证明以下链条: 量词消去 判据 是同胚 量词消去.
对于第一个 , 我们其实有加强版本.
断言. 任给量词消去理论 的两个模型 中的 元组 , 均有
对第二个 , 我们只需证明 是双射, 紧致 空间之间的连续双射自然是同胚. 满射是因为 也可以解读为部分型, 单射就是条件.
定义 2.8.0.35 (模型完全).