66、命题逻辑中的证明复杂度与系统研究

命题逻辑中的证明复杂度与系统研究

在逻辑和计算复杂性的研究中，命题逻辑的证明复杂度是一个关键领域。它涉及到如何用布尔公式序列表示句子，以及证明各种重言式的难度。

布尔公式表示句子

在证明复杂度的研究里，了解哪些句子可以用布尔公式序列来表示至关重要。由于能够定义 NC1 集合，所以也能表示全称 - NC1 句子。逻辑中我们关注重言式，重言式虽由布尔公式表示，但可看作前面有全称量词。说一个公式被所有真值赋值满足，等同于说带全称量词的命题公式为真。因为这些隐式量词只在有限域上取值，所以需要无限的布尔公式序列来表示一阶逻辑中的句子。句子和命题公式序列的关系是：句子为真当且仅当所有命题公式都是重言式。

例如，对于真算术句子 ∀x∀y(x ≤ y ∨ y ≤ x) ，就可以用上述方式表示。给定一阶逻辑的句子 φ，将表示 φ 的布尔公式序列称为 φ 到命题逻辑的翻译。“翻译”这个词是合理的，因为我们通常希望在翻译中保留 φ 的部分语法结构，这有助于证明谓词逻辑和命题演算中证明之间的有趣关系。而且，实际上可以将全称 - P 句子翻译成命题公式序列，全称量词能将 NC1 谓词提升为 P 谓词，从而可以在命题逻辑中表示基本类型的句子。

命题证明系统

命题演算中最重要的部分是证明。我们有各种有趣的重言式，想知道证明它们的难度。命题逻辑有多种公理化方法，在这些公理化方法中，本质上可以用大小最多为指数级（关于重言式大小 n）的证明来证明每个大小为 n 的重言式，但指数级大的证明用处不大。关键问题是哪些重言式有多项式大小的证明，当然，这只对无限的重言式序列有意义。

比如，我们会问鸽巢原理重言式 PHPn 是否有多项式大小的证明。这个界限应该是关