含量词的公式(∃y)[x2+y2-3=0∧x+y>0]的意思是：存在实数y，使得x2+y2-3=0和x+y>0同时成立。如果将量词从公式中消去，那么可以得到一个等价的无量词公式x2-3≤0∧[x≥0∨2x2-3<0]。这个公式比原来的公式简单而且明确很多。又譬如，哥德巴赫猜想断言：对任意大于2的偶数，存在两个奇素数，其和为给定正偶数。这个断言也可以用含有量词的公式来加以表述。几年前刚刚证明的Fermat大定理指出：对任意大于2的整数n，不存在正整数x,y,z，使得等式xn+yn=zn成立。这个命题同样可以用含量词的公式加以表示。如果能消去上述两个命题中的全称和存在量词，即可得到等价的永真命题，因而也就给出了命题的证明。
量词消去理论是一阶逻辑理论的重要组成部分。在可判定性理论中，为判断含量词命题的真假，人们往往需要消去其中的量词得到一个等价的不含量词的命题，通过对后者真值的判断来获知原命题的真假。然而，量词消去并非平凡的问题，这可以从数学家们证明上述费马大定理的艰辛历程中得到印证。
量词消去问题也没有统一的求解方法。目前主要是根据变量所在环/域的结构和命题中所涉及的运算将量词消去问题分为不同的类型，然后针对每种类型设计特定的量词消去算法。如果一阶逻辑中的任意命题都可以经过有限步运算得出该命题是否为真，则称该一阶逻辑理论是可判定的。带+、*、=和>运算的实闭域以及带+、*和=运算的代数闭域都是一阶逻辑可判定理论的典型范例。在这两种一阶逻辑理论中，多项式扮演着非常重要的角色，可以通过多项式理论将量词消去问题转化为多项式方程（组）的可解性问题，如实闭域上的一阶逻辑判定问题可以转化为求多项式方程（组）的实解问题，而代数闭域上的一阶逻辑判定问题可以转化为求多项式方程（组）的复解问题。
判定问题由D. Hilbert首先提出。根据他的设想，可将数学知识全部纳入严密的公理体系之中，在此基础上寻找一般的机械化方法来判定命题是否成立。但是1931年，在Hilbert的设想提出还不到3年之后，K. Gödel发现的不完备定理就否定了Hilbert的设想。Gödel证明了任何一个形式系统，只要包括了简单的初等数论描述，而且是自洽的，那么它必定包含某些系统内所允许的方法既不能证其为真也不能证其为伪的命题。这一定理对现今十分热门的人工智能领域也产生了重要影响。Gödel不完备定理不仅使数学基础研究发生了划时代的变化，更是现代逻辑史上最重要的一座里程碑。该定理与A. Tarski的形式语言真理论、图灵机和判定问题，是现代逻辑科学在哲学方面的三个标志性成果。
Gödel不完备定理让人们有些失望，但并不是任何有意义的公理系统都是不完备的。Gödel定理成立的前提是要假设所考虑的公理系统可以用来“定义”自然数。那么是否所有系统都能用来定义自然数呢？回答是否定的，也就是说，完备的公理系统是存在的。Tarski证明了实数和复数理论都是完备的一阶公理化系统，并且于1930年提出了针对实闭域上初等代数和初等几何中命题的判定方法。该方法分为变换和判定两步，变换即是对任意给定的公式进行量词消去，判定则是对所得的无量词公式进行真值判断。Tarski将关于两个多项式实根的Sylvester定理推广到了任意多变元方程和不等式情形，利用方程求根的思想处理量词消去和命题判定问题，从而将命题的判定转化为能在有限步内完成的代数运算和命题演算。然而，Tarski方法的复杂度是超指数的，因此它只是一种理论化的方法，无法被广泛应用到具体问题。尽管如此，Tarski的方法还是为判定问题的研究指明了新方向，也开启了针对特定系统寻求判定方法的研究先河。
柱形代数分解（简称CAD）是第一个实用的量词消去算法，由G. E. Collins于1975年提出，因此又被称为Collins算法。该算法可以将n维实空间中的任一半代数集通过投影和提升分解为有限多个互不相交的半代数集，所得半代数集都由同一组多项式定义，而在每个半代数集上定义多项式的符号不变。对含量词的命题进行量词消去即等价于寻找符合量词约束条件的参数胞腔，并将胞腔用多项式方程和不等式表示出来。CAD方法还可以用于半代数系统的实解隔离和实解分类。它和吴文俊的特征列方法、B. Buchberger的Gröbner基方法都是计算机代数系统的基石；后者也可以用于解决代数闭域上的量词消去问题。有关柱形代数分解有大量后续工作，学者从理论复杂度、实际计算效率、实施策略等方向针对量词消去问题对分解方法进行了研究、改进和发展。基于CAD的量词消去算法的复杂度虽然仍是双指数的，但较Tarski的超指数复杂度有了很大的改善，因此可以用于解决适当规模的量词消去问题。
由于量词消去问题在一般情形的复杂度是变元个数的双指数，因此量词消去的研究重点是将量词消去问题进行分类，然后针对各类具体问题设计更优化的算法。
Gauss消去法完全解决了线性多项式方程组的求解问题，该方法可以推广到高次多项式方程组，其核心思想是将方程组的求解问题转化为一元方程的求解问题。本文开始引用的那段充满哲思的玄论就是对中国元代数学名著《四元玉鉴》中用消去法求解四元方程组的一个概括性描述。《四元玉鉴》中只考虑求解四个未知元是由于受当时计算工具（算筹和算板）的限制，实际上书中给出的解方程的思想和方法完全可以扩展到任意多个变元的情形。西方学者还利用Hermite正规形式和Smith正规形式等将这类方法推广，用于研究一般的线性不定方程以及阿贝尔群。通过消去多项式系统中的某些变元，将系统化简至易于处理的特殊形式是求解多项式系统的主要思路。基于这种思路建立发展起来的消去理论和方法已经成为许多与解方程有关的数学分支的基础工具。现代数学更是离不开方程求解。有关超越函数方程、差分方程、微分和积分方程的研究已经并将继续作为基础和应用数学的主要分支向前发展。
19世纪末20世纪初，消去理论作为构造性代数几何的基本工具在欧洲发展活跃，出现了形式多样的结式和判别式。最常用的求解高次方程组的消去法就是基于结式计算的。结式的构造源自18世纪法国数学家é. Bézout，其理论后经J. J. Sylvester，A. L. Dixon，F. S. Macaulay等英国数学家发展完善，成为经典的消去方法。这种方法的主要思想是通过构造各种形式的结式矩阵，将多项式方程组的解投影到一元多项式方程的解。B. L. van der Waerden 在其《现代代数学》的早期版本中对结式消去理论和方法有较为详细的论述。此后，消去理论受到冷遇，被视为过时的理论，在《现代代数学》的新版中 “消去理论”一章也被删除。
随着计算技术的发展，或者更确切地说，随着计算机代数这门交叉学科的兴起，消去理论得以重新展示其威力，特别在方程求解中发挥其专长。现代消去理论和方法相继提出并得到空前发展。基于特征列、Gröbner基和柱形代数分解的消去方法已成为计算机代数领域的三大核心方法。
特征列方法是我国数学家吴文俊在上世纪70—80年代提出的、适用于多项式系统和微分多项式系统的消元与分解方法，其理论基础是美国数学家J. F. Ritt有关微分代数的工作和古代方程术中的算法思想。以吴-Ritt命名的特征列方法可以看作是高斯消去法对非线性情形的推广，所使用的主要运算是高次多项式之间的伪除。该方法后经王东明、高小山等学者发展完善，已作为机械化数学特别是代数计算和几何推理的基本方法写入《计算机代数》和《多项式代数》等研究生教材。
1965年，奥地利数学家B. Buchberger在他的博士论文中提出了以他导师的姓命名的Gröbner基方法。该方法可以在多项式组构成的理想中找到一组基，而这组基中的某些多项式构成三角列，因此可以通过计算Gröbner基将多项式方程组的求解问题转化为一元多项式方程的求解问题。在20余部著作和数千篇论文中得到深入研究和发展，Buchberger的Gröbner基方法理论优美、应用高效，是研究多项式理想的基本工具，也是支撑计算机代数系统的基石。
初等代数与几何的判定问题最早由A. Tarski解决。该问题可以归结为实闭域上的量词消去问题。美国数学家G. E. Collins提出的柱形代数分解方法可以用来完整地解决这一问题，并能为含有多项式等式和不等式的半代数系统的求解和实解分类提供有效工具。柱形代数分解方法的基本思想是通过投影和提升将实空间中的任意半代数集分解为有限多个由同一组多项式定义的、互不相交的半代数集，而在每个半代数集上定义多项式的符号保持不变，再通过选取半代数集上的样本点确定定义多项式在样本点的符号。量词消去、半代数系统求解和实解分类等问题都可以通过柱形代数分解获得解决。