【计算复杂性理论】证明复杂性（六）：其他证明系统简介-Toy模板网

这篇具有很好参考价值的文章主要介绍了【计算复杂性理论】证明复杂性（六）：其他证明系统简介。希望对大家有所帮助。如果存在错误或未考虑完全的地方，请大家不吝赐教，您也可以点击"举报违法"按钮提交疑问。

往期文章：

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

本文简要介绍一下其他值得一提的证明系统。对于不太重要的系统，只介绍它的强度。

一、布尔程序弗雷格系统： B P F \mathrm{BPF} BPF

一般来说弗雷格系统都是定义在德·摩根语言上的。那么我们可不可以给语言中添加新的连接词呢？可以。我们知道，连接词就是布尔函数，所以我们只需要添加一些布尔函数即可。设 $L$ 是不函数的集合，其中函数 $f$ 的元数是 $k_f$ 。 $\forall f\in L$ ，必须满足如下的等价公理（equality axioms）： $\bigwedge\limits_{i=1}^{k_f} p_i\equiv q_i\to f(p_1,\cdots,p_{k_f})\equiv f(q_1,\cdots,q_{k_f})$ 我们称定义在这种语言上的弗雷格系统 $F (L)$ 为相对化弗雷格系统（relatived Frege system），它是可靠的、完备的、推理完备的。

一个布尔程序（Boolean program）是一系列函数符号 $f_1,\cdots,f_s$ ，每个函数 $f_i$ 由公式 $A_i$ 定义，其中 $A_i$ 中可以出现函数 $f_1,\cdots,f_{i-1}$ 。设 $P$ 是一个引入了函数 $f_1,\cdots,f_s$ 的布尔程序，其对应的语言为 $L_P$ 。定义 $F (P)$ 为扩展了相对化弗雷格证明系统 $F(L_P)$ 的系统，它包含了 $f_i(p_1,\cdots,p_{k_f})=A_i(p_1,\cdots,p_{k_f})$ 作为新的公理模式。这种 $F (P)$ 称为 $BP$ 弗雷格系统，记作 $\mathrm{BPF}$ 。

定理1 对于永真式， $\mathrm{G}$ 多项式模拟 $\mathrm{BPF}$ 。

二、等式演算： E C \mathrm{EC} EC

$\mathrm{EC}$ （equational calculus）的每一行是一个等式，符号一般包括 $0,1,+,-,\cdot$ 。这里不赘述它的规则，只简单提一下它在域 $\mathbf{F}_2$ （ $0, 1$ 和其运算构成的域）上等价于弗雷格系统。

三、零点定理： N S \mathrm{NS} NS

这个系统用到了一些代数方面的知识和希尔伯特零点定理（Hilbert’s Nullstellensatz）。这里只提一下。

四、分割平面： C P \mathrm{CP} CP

分割平面（cutting planes, $\mathrm{CP}$ ）证明的每一行是一个形如 $\sum\limits_{i}a_i x_i\ge b$ 的整数不等式。公理为 $x\ge 0$ 和 $-x\ge -1$ ，使得 $0\le x\le 1$ 。有三条推理规则：加法规则、乘法规则和除法规则。分割平面系统反驳初始线性不等式组的可解性。

定理2 $\mathrm{CP}$ 多项式模拟归结（即 $\mathrm{CP}\ge_p\mathrm{R}$ ）。

五、隐式证明系统

我们可以把某些关于自然数的全称一阶逻辑命题（universal first-order statement） $\forall x\Phi(x)$ 转化为一系列关于比特长度 $n=1,2,\cdots$ 来表达的永真式： $\forall x(|x|=n)\Phi(x)$ 。对于相当多的一阶理论 $T$ （包括皮亚诺算术和带选择公理的策梅洛-弗兰克尔公理系统），我们可以把这种全称命题在 $T$ 中的证明转化为对应的一系列永真式的较短的命题证明。这些证明是附带在对应理论的证明系统中的证明。即使对于相对较弱的理论，这些证明系统也可能非常强。

设 $P, Q$ 是两个Cook-Reckhow证明系统。在证明系统 $Q$ 中对永真式 $\tau$ 的证明 $\pi$ 是一个字符串。如果它非常长，比如它有 $l=2^k$ 比特，我们可以把隐式地它表示成一个布尔线路 $\beta$ 。 $\beta$ 有 $k$ 个输入，从 $i\in{\{0,1\}}^k$ 计算 $\pi$ 的第 $i$ 位 $\pi_i$ 。这样的话， $\beta$ 的大小可能指数级地小于 $\pi$ 的大小。但是 $\beta$ 本身并不能形成一个Cook-Reckhow证明系统中的证明。因此，我们还需要一个 $P$ 证明 $\alpha$ 来描述 $\beta$ 确实定义了一个有效的 $Q$ 证明 $\pi$ 的事实。有序对 $(\alpha,\beta)$ 是一个在系统 $[P, Q]$ 中对 $\tau$ 的证明。 $[P, Q]$ 的正式定义这里从略，不过我们可以从上面的描述理解它的它的非正式定义。

对于包含 $\mathrm{R}$ 的证明系统 $P$ ，我们定义隐式 $P$ （implicit $P$ ），记作 $i P$ ，为 $i P = [P, P]$ 。

引理3 (i) $\forall P$ ， $P\le_p[P,\mathrm{R}^*]$ ；(ii) $\forall P\ge_p \mathrm{R}$ ， $iP\equiv_p[iP,P]$ 。

定理4 $iER\ge_p\mathrm{G}$ 。

引理5 $ER\equiv_p[\mathrm{R},\mathrm{R}^*]$ 。

六、OBDD证明系统

OBDD（ordered binary decision diagram，有序二元决策图）是一种特殊的分支程序，用于计算一个布尔函数。在图的每一个路径中，每个变量被访问至多一次并且访问顺序与全局的变量排列顺序一致。对于OBDD $P$ ，令 $f_P$ 为其定义的布尔函数。

OBDD证明系统是一种反驳证明系统。设 $\mathcal{C}$ 是一个子句集。 $\mathcal{C}$ 的一个OBDD反驳是一个OBDD序列 $P_1,\cdots,P_k$ ，使得：

$\forall i\le k$ ，
- 要么 $P_i$ 计算了 $\mathcal{C}$ 中一个子句定义的布尔函数，
- 要么存在 $u, v < i$ 使得 $f_{P_u}\land f_{P_v}\le f_{P_i}$ （即 $f_{P_u}\land f_{P_v}\to f_{P_i}$ ）；
$f_{P_k}$ 等价于 $0$ 。

引理6 OBDD证明系统多项式模拟归结但不能多项式模拟 $\mathrm{LK}_d$ ，对于充分大的 $d\ge 1$ ；任何 $\mathrm{LK}_d$ 都不能多项式模拟OBDD证明系统。不过，弗雷格系统多项式模拟OBDD证明系统。

七、皮亚诺算术作为一种证明系统

皮亚诺算术，记作 $\mathrm{PA}$ ，是一个典型的一阶理论（一阶理论就是某个语言上的公理的集合），不过也可以用于定义有限数学。

$\mathrm{PA}$ 的语言 $L_{\mathrm{PA}}$ 包含常量 $0$ 和 $1$ ，二元函数符号 $+$ 和 $\cdot$ ，以及二元序关系 $\le$ ；等于号 $=$ 是在一阶逻辑中定义的。 $\mathrm{PA}$ 的标准模型（standard model）是带有对语言的标准解释的自然数集 $\N$ 。 $\mathrm{PA}$ 的公理是由构成Robinson理论 $\mathrm{Q}$ 的有限列表组成的：

$x+1\ne 0$ ；
$x+1=y+1\to x=y$ ；
$x + 0 = x$ ；
$x + (y + 1) = (x + y) + 1$ ；
$x\cdot 0=0$ 和 $x\cdot 1=x$ ；
$x\cdot(y+1)=(x\cdot y)+x$ ；
关于离散线性序关系 $\le$ 的一些公理（见https://en.wikipedia.org/wiki/Peano_axioms#Equivalent_axiomatizations）；
$x\le y\equiv (\exists z,x+z=y)$ ；

以及所有（无限个）归纳公理（induction scheme, $\mathrm{IND}$ ）的示例： $[A(0)\land\forall x(A(x)\to A(x+1))]\to\forall x A(x)$ 对于所有 $L_{\mathrm{PA}}$ 公式 $A$ （它可能包含不同于 $x$ 的自由变量）。

定义有界公式类 $\Delta_0$ 为满足下列条件的由 $L_{\mathrm{PA}}$ 公式组成的最小的类：

包含所有无量词的公式；
关于德·摩根语言中的连接词封闭；
关于有界量化（bounded quantification）封闭：若 $A(\boldsymbol{x},y)$ 是一个 $\Delta_0$ 公式并且 $t(\boldsymbol{x})$ 是一个 $L_{\mathrm{PA}}$ 项，那么下面的两个公式都是 $\Delta_0$ 的： $\exists y\le t(\boldsymbol{x})A(\boldsymbol{x},y)\text{ 和 }\forall y\le t(\boldsymbol{x})A(\boldsymbol{x},y)$ 其中 $\exists y\le t(\boldsymbol{x})A(\boldsymbol{x},y)$ 代表 $\exists y,y\le t(\boldsymbol{x})\land A(\boldsymbol{x},y)$ ， $\forall y\le t(\boldsymbol{x})A(\boldsymbol{x},y)$ 代表 $\forall y,y\le t(\boldsymbol{x})\to A(\boldsymbol{x},y)$ 。

定义 $\Sigma_1^0$ 公式为具有 $\exists z B(\boldsymbol{x},z)$ 形式的公式，其中 $B\in\Delta_0$ 。

数理逻辑中有两个经典事实：

一个 $k$ 元关系 $R\subseteq\N^k$ 是递归可枚举（recursively enumerable）的，当且仅当存在一个 $\Sigma_1^0$ 公式 $A(\boldsymbol{x})$ ，其中 $\boldsymbol{x}=x_1,\cdots,x_k$ ，使得 $\forall\boldsymbol{m}\in\N^k$ ， $\boldsymbol{m}\in R\iff\N\models A(\boldsymbol{m})$ 。
对于所有 $\Sigma_1^0$ 公式 $A(\boldsymbol{x})$ 和 $\boldsymbol{m}\in\N^k$ ， $\N\models A(\boldsymbol{x})\iff \mathrm{PA}\vdash A(m_1,\cdots,m_k)$ 。

注意 $R$ 是递归的（recursive）当且仅当 $R$ 和 $\N^k\setminus R$ 都可以在 $\Sigma_1^0$ 中定义。

对于字符串 $w\in{\{0,1\}}^*$ ，定义封闭项 $\lceil w\rceil$ 为：

$\lceil\varepsilon\rceil=0$ （其中 $\varepsilon$ 是空串）；
对于 $w=w_{t-1}\cdots w_1 w_0\in{\{0,1\}}^t,t\ge 1$ ，令 $\lceil w\rceil=2^t+\sum\limits_{j=0}^{t-1}w_j 2^j$ 。

其实就是把 $01$ 串和自然数一一对应。

根据经典事实1，存在一个 $\Sigma_1^0$ 公式 $T a u t (x)$ ，使得 $\forall w\in{\{0,1\}}^*$ ， $w\in\mathrm{TAUT}\iff\N\models Taut(\lceil w\rceil)$ 。并且，根据经典事实2， $w\in\mathrm{TAUT}\iff\mathrm{PA}\vdash Taut(\lceil w\rceil)$ 。注意对于任何公式 $\tau$ ， $\lceil\tau\rceil$ 二进制表示的长度均为 $O(|\tau|)$ 。

这允许我们定义命题证明系统 $P_{\mathrm{PA}}$ 为： $P_\mathrm{PA}(\pi)=\tau\iff\pi\text{是}Taut(\lceil w\rceil)\text{的一个}\mathrm{PA}\text{证明。}$
引理7 $P_\mathrm{PA}$ 是一个Cook-Reckhow证明系统。

事实上， $P_\mathrm{PA}$ 难以置信地强，后面我们会证明它多项式模拟所有我们介绍过的证明系统。

八、补充

理想证明系统（ideal proof system, $\mathrm{IPS}$ ）是一种多项式模拟 $EF$ 的证明系统。
我们前面提到的证明系统都针对的是 $\mathrm{TAUT}$ 这个 $\mathsf{coNP}$ 完全问题。其实我们不必拘泥于 $\mathsf{coNP}$ ；不可 $3$ 着色的图组成的语言也是 $\mathsf{coNP}$ 完全的。不可 $3$ 着色的图可以由Hajós演算（Hajós calculus）构造。并且， $EF$ 有多项式上界当且仅当每个不可 $3$ 着色的图都可以在多项式步内由Hajós演算构造。

参考文献

[1] Krajícěk, Jan. “Proof complexity.” Mathematics and Computation (2019). 这是这篇文章主要的参考文献。这本书可在这里下载。文章来源地址https://www.toymoban.com/news/detail-604019.html

到了这里，关于【计算复杂性理论】证明复杂性（六）：其他证明系统简介的文章就介绍完了。如果您还想了解更多内容，请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章，希望大家以后多多支持TOY模板网！