量词消去

量词消去是指一个理论中的每个公式都等价于一个不含量词的公式，这是一种强大的结构特征，能够产生判定过程并清晰地描述可定义集。

Definition

如果一个理论中的每个公式，在模该理论的意义下，都等价于一个具有相同自由变量的无量词公式，则该理论允许量词消去；这意味着可定义集恰好是由原子公式定义的布尔组合。

Scope

本主题涵盖量词消去的定义、确立量词消去的标准、模型完备性（model completeness）的相关概念，以及稠密线性序、代数闭域、实闭域和普雷斯伯格算术（Presburger arithmetic）的典型示例，以及这些示例所蕴含的可判定性结果。

Core questions

• 何时可以系统地从理论公式中移除量词？
• 量词消去如何描述结构的定义集？
• 为什么量词消去通常能产生可判定性？
• 哪些经典代数理论允许量词消去？

Key theories

量词消去检验

只需从原子公式和否定原子公式的合取中消去一个存在量词，将该性质简化为可管理的局部条件，通常通过子结构的嵌入来检验。

代数闭域和实闭域

代数闭域和实闭域的理论允许量词消去，因此它们的可定义集分别是可构造集和半代数集，从而恢复了经典几何。

塔斯基判定过程

实闭域的量词消去提供了一种算法，用于判定有序域语言中关于实数的任何一阶语句的真假，因此初等代数和几何是可判定的。

Clinical relevance

量词消去将逻辑问题转化为代数问题：它提供了计算机代数和验证中使用的判定过程，其几何内容，例如实数上可定义集的半代数性质，将模型论与实代数几何和o-极小性（o-minimality）联系起来。

History

量词消去在20世纪20年代和30年代被斯科伦（Skolem）、兰福德（Langford）和普雷斯伯格（Presburger）用于判定特定理论，塔斯基（Tarski）为实闭域确立了量词消去，从而产生了其著名的初等代数和几何判定过程。罗宾逊（Robinson）通过模型完备性（model completeness）重新阐述了相关思想，使该技术成为应用模型论的常用工具。

Key figures

• Alfred Tarski
• Thoralf Skolem
• Abraham Robinson
• Mojzesz Presburger

Seminal works

• marker2002
• hodges1993
• tarski1951

Frequently asked questions

为什么量词消去能使理论可判定？

一个语句没有自由变量，因此消去其量词后会留下一个无量词语句，该语句由关于常量的原子语句构成，其真假可以直接检验。如果消去是有效的，这将提供一个算法来判定每个语句。

每个理论都允许量词消去吗？

不。许多理论不允许，有时可以通过在语言中添加可定义谓词来获得量词消去。量词消去是一种特殊且有用的性质，是那些对其可定义集有特别透明描述的理论的特征。