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 (省略型定理). 如果有一列非主型 , 则存在 的可数模型 省略其中每个型.

这个定理的证明非常奇妙, 因为它用到了理论空间的 Baire 性质, 这是 Baire 定理所允许的.

证明. 我们向 中加入一列常元 , 得到一个新的语言 . 令 中全体延伸一开始的理论 的完备理论 形成一个空间 . 事实上由于这始终是可数语言, 它就是 , 因而是个紧致 完全不连通零维空间.

我们用这列 来讨论 的见证性.

定义 2.8.0.26. 的理论 对常元组 具有见证性, 若对每个公式 , 时均有一个 使得 .

引理 2.8.0.27. 中, 全体对 具有见证性的理论 构成的集合 是余第一纲集.

证明.

接下来, 我们考虑 , 每个 都给出一个 , 它只保留变元为 的那些公式. 、

引理 2.8.0.28. 是连续函数, 且将开闭集映为开闭集.

证明.

接下来, 我们来看看谁不被实现.

引理 2.8.0.29. 对非主型 , 存在余第一纲集 使得对每个 , 此时的任何 均让 不被 实现.

证明.

最后, 这个定理的证明水到渠成. 第一个引理给出一个余第一纲集 , 第三个引理对每个 给出一个余第一纲集 , Baire 纲定理指出它们全部交起来不空, 因此不妨假定其中有一个理论 . 由于它对 有见证性, 我们有 的可数模型 . 显然这个模型省略了每个 .

我们来讨论理论的一种重要性质, 它允许我们用简单的无量词句子代替复杂的可能带量词的任意句子.

定义 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 (模型完全).