跳转到内容

量词消去

维基百科,自由的百科全书

量词消去数理逻辑模型论计算机科学中的一类技巧。我们称一个理论可消去量词,当且仅当对每个公式皆存在另一个不带量词的公式,使得两者在该理论中等价,即:

量词消去在模型论有多种刻划;即使一个理论可消去量词,也不保证存在一个相应的算法

一个理论的量词消去算法系将一个带量词的公式转成一个等价但不带量词的公式。利用这个算法,我们能将任一句子(不带自由变量的公式)转成一个不带变量的句子,后者通常可藉简单的计算判定。因此,量词消去算法的存在性蕴含该理论的可判定性。

若干例子

以下是若干可消去量词的理论:

以及它们之间的许多组合,如带 Presburger 算术的布尔代数等等。量词消去也可用以证明“合并”某些可判定理论可得到新的可判定理论,类似的建构包括有 Feferman-Vaught 定理及项幂。

基本想法

如欲建构地证明一个理论可消去量词,仅须处理一个存在量词配上若干个文字合取的情形;换言之,即证明每个形如 (其中每个都是文字) 的公式都在该理论中等价于一个无量词的公式——诚然,假设已知如何对一串公式的合取消去量词,则若是个公式,可将其写作析取范式

并运用 等价于此一性质。最后,为了消去全称量词 ,其中不带量词,我们将写作析取范式,并运用等价于一性质,遂证得原断言。

文献

  • Wilfrid Hodges. "Model Theory". Cambridge University Press. 1993.
  • Viktor Kuncak and Martin Rinard. "Structural Subtyping of Non-Recursive Types is Decidable". In Eighteenth Annual IEEE Symposium on Logic in Computer Science, 2003.