量词消去

量词消去是模型论中的性质. 一个理论具有量词消去表明, 任意一阶语句都等价于某不含量词的语句. 一个初等的例子是 上如下两个语句等价:

1定义

定义 1.1. 一个理论 具有量词消去, 如果对于所有公式 , 存在一个不含量词的公式 使得

2判别法

除了直接证明某个理论具有量词消去, 也可以使用如下判别法:

命题 2.1. 理论 满足量词消去当且仅当:

对于其任两个模型 , , 任两个 , , 如果它们的 相同, 则它们的型相同.

证明. 满足量词消去, 则对于任意公式 , 存在不含量词者 使得 , 故 , 即 , 也就是说属于 , 从而 . 另一边的包含关系同理.

另一方面, 条件 (2.1) 说的是 Stone 空间 分离, 而由 Stone 空间射有限空间, 在有限交和有限并下封闭, 故 等于所有的闭开集组成的集合, 从而任意 , 也就是说 , 即 具有量词消去.

命题 2.2. 如果所有 -饱和模型满足:

它们之间的 -同构-同构,

那么 具有量词消去.

证明. 对于 的任两个模型 , , 以及 , 满足它们的 阶型相同, 即 , 分别取 -饱和初等扩张 , , 则有 , 故由条件得, 在 , 中有 , 即 . 由命题 (2.1) 即得 具有量词消去.

利用判别法 (2.2), 可以证明代数闭域理论 , 无界稠密全序理论 等具有量词消去.

3例子与应用

代数闭域理论

代数闭域理论 具有量词消去:

命题 3.1. 理论 的所有 -饱和模型形如 , 使得超越度 , 其中 基域由于 -同构保证特征一样, 从而自动给出 -同构. 由命题 (2.2) 得到 具有量词消去.

它有如下交换代数方面的应用:

利用量词消去可以说明代数闭域的所有模型都是存在封闭模型, 从而可以证明 Hilbert 零点定理.

参见: Hilbert 零点定理

利用量词消去可以说明代数闭域 上的可定义集可构造集重合. 这给出了 Chevalley 定理的证明.

参见: Chevalley 定理 (可构造集)

实闭域理论

实闭域理论 也具有量词消去, 从而具有模型完备. 因为任何实闭域都包含代数实数域 , 故得到 完备的理论.

利用这个事实, 可以给出平方和问题的证明.

参见: 平方和问题

无界稠密全序理论

无界稠密全序理论 也具有量词消去:

命题 3.2. 理论 的任两个模型都是 -同构的. 由命题 (2.2) 得到 具有量词消去.

术语翻译

量词消去英文 quantifier elimination德文 Quantorenelimination法文 élimination des quantificateurs拉丁文 eliminatio quantificatorum古希腊文 ἀνάλειψις ποσοδείκτων