【计算复杂性理论】证明复杂性（五）：量化命题演算（Quantified Propositional Calculus）

往期文章：

• 【计算复杂性理论】证明复杂性（Proof Complexity）（一）：简介
  
• 【计算复杂性理论】证明复杂性（二）：归结（Resolution）与扩展归结（Extended Resolution）证明系统
• 【计算复杂性理论】证明复杂性（三）：弗雷格（Frege）与扩展弗雷格（Extended Frege）证明系统
• 【计算复杂性理论】证明复杂性（四）：相继式演算（Sequent Calculus）

量化命题演算的特点就是引入了命题量词。设$\mathbf{p}$是一个变量元组，$\alpha$是以$\mathbf{p}$和$x$为变量的命题公式，则定义$\forall x\alpha (\mathbf{p},x)$为$\alpha (\mathbf{p},0)\wedge \alpha (\mathbf{p},1)$，定义$\exists x\alpha (\mathbf{p},x)$为$\alpha (\mathbf{p},0)\vee \alpha (\mathbf{p},1)$。

注意，命题量词不同于一阶逻辑中的量词。一阶逻辑中的量词是不可替代的，有些含量词的公式不能用不含量词的公式表示；但含命题量词的命题公式则是可以被不含命题量词的命题公式替代的，也就是说，命题两次不会增加公式的表达能力。不过，命题量词允许我们缩短公式，比如$\underset{\mathbf{p}}{\bigvee }\alpha (\mathbf{p})$（其中$\mathbf{p}$的取值范围是 { 0 , 1 } n {\{0,1\}}^n {0,1}n）的大小为$\Omega (2^n|\alpha |)$，但与其等价的一个量化命题公式$\exists p_1\cdots \exists p_n\alpha (\mathbf{p})$的大小仅为$O(n)+|\theta |$。

定义1（${\Sigma }_n^q$和${\Pi }_n^q$）

1. 类${\Sigma }_0^q={\Pi }_0^q$由不含量词的命题公式构成。

2. 类${\Sigma }_{i+1}^q$和${\Pi }_{i+1}^q$是满足下列条件的最小类：

   • ${\Sigma }_i^q\cup {\Pi }_i^q\subseteq {\Sigma }_{i+1}^q\cap {\Pi }_{i+1}^q$；
   • ${\Sigma }_{i+1}^q$和${\Pi }_{i+1}^q$对$\vee ,\wedge$运算封闭；
   • 若$\varphi \in {\Sigma }_{i+1}^q$则$\neg \varphi \in {\Pi }_{i+1}^q$；
   • 若$\varphi \in {\Pi }_{i+1}^q$则$\neg \varphi \in {\Sigma }_{i+1}^q$；
   • ${\Sigma }_{i+1}^q$对存在量化（existential quantification）封闭；
   • ${\Pi }_{i+1}^q$对全称量化（universal quantification）封闭。

3. 量化命题公式是出现在某个${\Sigma }_i^q$中的任何公式；${\Sigma }_{\infty }^q$是所有量化命题公式组成的类。

我们现在在$\mathrm{LK}$的基础上定义量化命题演算系统：相继式演算$\mathrm{G}$系统。

定义2 $\mathrm{G}$通过允许在相继式中出现量化命题公式和使用下面两条规则来扩展$\mathrm{LK}$系统：

• $\forall$引入：$$\text{左边：}\begin{array}{c}A(B),\Gamma \to \Delta \\ \forall xA(x),\Gamma \to \Delta \end{array}\text{ 和 右边：}\begin{array}{c}\Gamma \to \Delta ,A(B)\\ \Gamma \to \Delta ,\exists xA(x)\end{array}$$
• $\exists$引入：$$\text{左边：}\begin{array}{c}A(B),\Gamma \to \Delta \\ \exists xA(x),\Gamma \to \Delta \end{array}\text{ 和 右边：}\begin{array}{c}\Gamma \to \Delta ,A(B)\\ \Gamma \to \Delta ,\forall xA(x)\end{array}$$其中$B$是任何公式，并且要求$p$不出现在$\forall$引入右边规则的结论和$\exists$引入左边规则的结论中。

证明系统${\mathrm{G}}_i$是$G$的只允许出现${\Sigma }_i^q$公式的子系统。

${\mathrm{G}}_i^{\ast }$是${\mathrm{G}}_i$的只允许出现树形证明的子系统。

注意${\mathrm{G}}_0=\mathrm{LK}$且${\mathrm{G}}_0{\equiv }_p{\mathrm{G}}_0^{\ast }$。但${\mathrm{G}}_i$和${\mathrm{G}}_i^{\ast }$（$i>0$）的关系是未知的。

定理3 ${\mathrm{G}}_1^{\ast }{\equiv }_{p}EF$。

定理4 $\forall i>0$，${\mathrm{G}}_i$多项式模拟${\mathrm{G}}_{i+1}^{\ast }$对${\Sigma }_i^q$公式的证明。

定理5 设$\Gamma \to \Delta$是一个逻辑有效的相继式，包含具有前束范式形式的量化命题公式。则它有一个树形、无切割的$\mathrm{G}$证明，该证明含有一个相继式$S$使得

• 在$S$之前的证明过程中不出现量词推理（quantifier inference）；
• 在$S$之后的证明过程中不出现命题推理（propositional inference）。

参考文献

[1] Krajícěk, Jan. “Bounded Arithmetic, Propositional Logic and Complexity Theory.” Cambridge University Press, 1995. 这是这篇文章主要的参考文献。这本书可在这里下载。