量词消去

量词消去是模型论中的性质. 一个理论具有量词消去表明, 任意一阶语句都等价于某不含量词的语句. 一个初等的例子是 $\mathbb{R}$ 上如下两个语句等价:$$\exists x(a\ne 0\wedge a{x}^2+bx+c=0)\text{ 和 }(a\ne 0)\wedge (b^2-4ac\ge 0).$$

1定义

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

2判别法

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

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

对于其任两个模型 $\mathcal{M}$, $\mathcal{N}$, 任两个 $\overline{a}\in M^n$, $\overline{b}\in N^n$, 如果它们的 $0$ 阶型相同, 则它们的型相同.

证明. 若 $T$ 满足量词消去, 则对于任意公式 $\phi \in \mathrm{tp}(\overline{a})$, 存在不含量词者 $\chi$ 使得 $T\models \phi \leftrightarrow \chi$, 故 $\chi \in \mathrm{tp}(\overline{a})$, 即 $\chi \in {\mathrm{tp}}_0(\overline{a})$, 也就是说属于 ${\mathrm{tp}}_0(\overline{b})$, 从而 $\phi \in \mathrm{tp}(\overline{b})$. 另一边的包含关系同理.

另一方面, 条件 (2.1) 说的是 Stone 空间 $S_n(T)$ 被 $\mathcal{A}=\{F_{\chi }\mid \chi \text{ 不含量词}\}$ 分离, 而由 Stone 空间是射有限空间, $\mathcal{A}$ 在有限交和有限并下封闭, 故 $\mathcal{A}$ 等于所有的闭开集组成的集合, 从而任意 $F_{\phi }\in \mathcal{A}$, 也就是说 $F_{\phi }=F_{\chi }$, 即 $T$ 具有量词消去.

$\square$

命题 2.2. 如果所有 $T$ 的 $\omega$-饱和模型满足:

它们之间的 $0$-同构是 $\omega$-同构,

那么 $T$ 具有量词消去.

证明. 对于 $T$ 的任两个模型 $\mathcal{M}$, $\mathcal{N}$, 以及 $\overline{a}\in M^n$, $\overline{b}\in N^n$ 满足它们的 $0$ 阶型相同, 即 ${\mathrm{tp}}_0(\overline{a})={\mathrm{tp}}_0(\overline{b})$, 分别取 $\omega$-饱和初等扩张 ${\mathcal{M}}^{\prime }$, ${\mathcal{N}}^{\prime }$, 则有 $\overline{a}{\cong }_0\overline{b}$, 故由条件得, 在 ${\mathcal{M}}^{\prime }$, ${\mathcal{N}}^{\prime }$ 中有 $\overline{a}{\cong }_{\omega }\overline{b}$, 即 $\mathrm{tp}(\overline{a})=\mathrm{tp}(\overline{b})$. 由命题 (2.1) 即得 $T$ 具有量词消去.

$\square$

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

3例子与应用

代数闭域理论

代数闭域理论 $\mathsf{ACF}$ 具有量词消去:

命题 3.1. 理论 $\mathsf{ACF}$ 的所有 $\omega$-饱和模型形如 $F$, 使得超越度 $\mathrm{trdeg}(F/F_0)\ge {\aleph }_0$, 其中 $F_0$ 是基域$$F_0=\{\begin{array}{ll}\overline{\mathbb{Q}},& \mathrm{char}F=0.\\ {\overline{\mathbb{F}}}_p,& \mathrm{char}F=p.\end{array}$$由于 $0$-同构保证特征一样, 从而自动给出 $\omega$-同构. 由命题 (2.2) 得到 $\mathsf{ACF}$ 具有量词消去.

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

•	利用量词消去可以说明代数闭域的所有模型都是存在封闭模型, 从而可以证明 Hilbert 零点定理. 参见: Hilbert 零点定理
•	利用量词消去可以说明代数闭域 $K$ 上的可定义集和可构造集重合. 这给出了 Chevalley 定理的证明. 参见: Chevalley 定理 (可构造集)

实闭域理论

实闭域理论 $\mathsf{RCF}$ 也具有量词消去, 从而具有模型完备. 因为任何实闭域都包含代数实数域 $\mathbb{R}\cap {\mathbb{Q}}^{\mathrm{alg}}$, 故得到 $\mathsf{RCF}$ 是完备的理论.

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

参见: 平方和问题

无界稠密全序理论

无界稠密全序理论 $\mathsf{DLO}$ 也具有量词消去:

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

术语翻译

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