数学中有两个非常特别的符号∃和∀，它们分别代表存在和任意。这两个符号与其限定变量一起，如∃x和∀y，称为存在量词和全称量词。存在和全称量词在数学中必不可少，但在很多时候我们都不希望它们出现，因为含有量词的数学问题往往都非常棘手、难以处理。量词符号∃和∀源自英文单词Exist和All的缩写E和A的镜像。这种镜像表示不仅简明对称，而且将两个特殊符号和常用变量区分开来。

譬如，含量词的公式(∃y)[x²+ y²-3=0∧x+y>0]的意思是：存在实数y，使得x²+y²-3=0和x+y>0同时成立。如果将量词从公式中消去，那么可以得到一个等价的无量词公式x²-3≤0∧[x≥0∨2x²-3<0]。这个公式比原来的公式简单而且明确很多。又譬如，哥德巴赫猜想断言：对任意大于2的偶数，存在两个奇素数，其和为给定正偶数。这个断言也可以用含有量词的公式来加以表述。几年前刚刚证明的Fermat大定理指出：对任意大于2的整数n，不存在正整数x,y,z，使得等式xⁿ+yⁿ=zⁿ成立。这个命题同样可以用含量词的公式加以表示。如果能消去上述两个命题中的全称和存在量词，即可得到等价的永真命题，因而也就给出了命题的证明。

量词消去理论是一阶逻辑理论的重要组成部分。在可判定性理论中，为判断含量词命题的真假，人们往往需要消去其中的量词得到一个等价的不含量词的命题，通过对后者真值的判断来获知原命题的真假。然而，量词消去并非平凡的问题，这可以从数学家们证明上述费马大定理的艰辛历程中得到印证。

量词消去问题也没有统一的求解方法。目前主要是根据变量所在环/域的结构和命题中所涉及的运算将量词消去问题分为不同的类型，然后针对每种类型设计特定的量词消去算法。如果一阶逻辑中的任意命题都可以经过有限步运算得出该命题是否为真，则称该一阶逻辑理论是可判定的。带+、*、=和>运算的实闭域以及带+、*和=运算的代数闭域都是一阶逻辑可判定理论的典型范例。在这两种一阶逻辑理论中，多项式扮演着非常重要的角色，可以通过多项式理论将量词消去问题转化为多项式方程（组）的可解性问题，如实闭域上的一阶逻辑判定问题可以转化为求多项式方程（组）的实解问题，而代数闭域上的一阶逻辑判定问题可以转化为求多项式方程（组）的复解问题。

图1 David Hilbert（1862—1943）

判定问题由D. Hilbert首先提出。根据他的设想，可将数学知识全部纳入严密的公理体系之中，在此基础上寻找一般的机械化方法来判定命题是否成立。但是1931年，在Hilbert的设想提出还不到3年之后，K. Gödel发现的不完备定理就否定了Hilbert的设想。Gödel证明了任何一个形式系统，只要包括了简单的初等数论描述，而且是自洽的，那么它必定包含某些系统内所允许的方法既不能证其为真也不能证其为伪的命题。这一定理对现今十分热门的人工智能领域也产生了重要影响。Gödel不完备定理不仅使数学基础研究发生了划时代的变化，更是现代逻辑史上最重要的一座里程碑。该定理与A. Tarski的形式语言真理论、图灵机和判定问题，是现代逻辑科学在哲学方面的三个标志性成果。

图2 Kurt Gödel（1906—1978）

Gödel不完备定理让人们有些失望，但并不是任何有意义的公理系统都是不完备的。Gödel定理成立的前提是要假设所考虑的公理系统可以用来“定义”自然数。那么是否所有系统都能用来定义自然数呢？回答是否定的，也就是说，完备的公理系统是存在的。Tarski证明了实数和复数理论都是完备的一阶公理化系统，并且于1930年提出了针对实闭域上初等代数和初等几何中命题的判定方法。该方法分为变换和判定两步，变换即是对任意给定的公式进行量词消去，判定则是对所得的无量词公式进行真值判断。Tarski将关于两个多项式实根的Sylvester定理推广到了任意多变元方程和不等式情形，利用方程求根的思想处理量词消去和命题判定问题，从而将命题的判定转化为能在有限步内完成的代数运算和命题演算。然而，Tarski方法的复杂度是超指数的，因此它只是一种理论化的方法，无法被广泛应用到具体问题。尽管如此，Tarski的方法还是为判定问题的研究指明了新方向，也开启了针对特定系统寻求判定方法的研究先河。

图3 Alfred Tarski（1901—1983）

柱形代数分解（简称CAD）是第一个实用的量词消去算法，由G. E. Collins于1975年提出，因此又被称为Collins算法。该算法可以将n维实空间中的任一半代数集通过投影和提升分解为有限多个互不相交的半代数集，所得半代数集都由同一组多项式定义，而在每个半代数集上定义多项式的符号不变。对含量词的命题进行量词消去即等价于寻找符合量词约束条件的参数胞腔，并将胞腔用多项式方程和不等式表示出来。CAD方法还可以用于半代数系统的实解隔离和实解分类。它和吴文俊的特征列方法、B. Buchberger的Gröbner基方法都是计算机代数系统的基石；后者也可以用于解决代数闭域上的量词消去问题。有关柱形代数分解有大量后续工作，学者从理论复杂度、实际计算效率、实施策略等方向针对量词消去问题对分解方法进行了研究、改进和发展。基于CAD的量词消去算法的复杂度虽然仍是双指数的，但较Tarski的超指数复杂度有了很大的改善，因此可以用于解决适当规模的量词消去问题。

图4 George E. Collins（1928—2017）

由于量词消去问题在一般情形的复杂度是变元个数的双指数，因此量词消去的研究重点是将量词消去问题进行分类，然后针对各类具体问题设计更优化的算法。

（本文经王东明教授审阅，图片均来源于网络）

（杨静）

来源：阿狗数学AlgoMath