因此,关于证明系统 \mathcal{P} 提出的一个自然问题是,是否有可能识别重言式 H 的类别,这些重言式 H 是“困难的”,因为任何证明 \phi \in H 有效的 \mathcal{P} 证明相对于 \phi 的大小必定是不可行的长。 Haken(1985)对于称为解析的系统获得了肯定的答案,许多自动定理证明器都基于该系统。 Haken 的证明利用了 Cook 和 Reckhow (1979) 的观察,即我们可以在命题逻辑中制定鸽子洞原理 (PHP),即将 n+1 只鸽子分配到 n 个洞,必须将两只鸽子分配到某个洞,使用原子字母 P_{ij} 来表示鸽子 i 被放入 j 洞。
\text{PHP}_n = \bigwedge_{0 \leq i \leq n} \ \bigvee_{0 \leq j \lt n} P_{ij} \rightarrow \bigvee_{0 \leq i \lt m \leq n} \bigvee_{0 \leq j \lt n} (P_{ij} \楔形 P_{mj})
因此,它形式化了 PHP 的 n 鸽子版本,因此是每个 n 的同义反复。因此 \text{PHP}_n 在任何完整的命题逻辑证明系统中都是可证明的。
Haken 表明,任何 \text{PHP}_n 的解析证明的大小必须至少为 n 的指数。由此可见,分辨率不受多项式限制。然而,后来 Buss (1987) 证明,系统 \mathcal{P}_1 (以及像 \mathcal{P}_2、\mathcal{P}_3 这样的系统可以有效地模拟 \mathcal{P}_1)确实承认 \text{PHP}_n 的证明,其大小为 n 的多项式。证明复杂性的后续研究方向之一是确定 PHP 或相关组合原理也很难实现的其他证明系统。例如,参见 Buss (2012)、Segerlind (2007)。
4.4 描述复杂性
逻辑和计算复杂性之间的另一种联系是由称为描述复杂性理论的学科提供的。正如我们所看到的,从计算复杂性理论的意义上来说,问题 X 被认为是“复杂的”,与算法决策的难度成正比。另一方面,描述性复杂性使问题变得“复杂”,与描述其实例所需的逻辑资源成正比。换句话说,X 的描述复杂性是根据相对于适当的有限结构背景类定义其实例所需的公式类型来测量的。
描述性复杂性始于这样的观察:由于计算问题是由有限的组合对象(例如字符串、图形、公式等)组成的,因此可以将它们的实例描述为一阶模型理论的传统意义上的有限结构。特别是,给定问题 X,我们将其每个实例 x \in X 与关系签名 \tau 上的有限结构 \mathcal{A}_x 关联起来,其非逻辑词汇将取决于构成 X 的对象类型。 [45]
给定这样的签名 tau,我们将 \text{Mod}(\tau) 定义为所有具有有限域的 tau 结构的类。在描述复杂性理论的背景下,逻辑 \mathcal{L} 被视为一阶逻辑语言的扩展,具有一类或多类附加表达式,例如高阶量词或定点运算符。这些在语义上被视为逻辑符号。如果 \mathcal{L} 是这样一个逻辑,而 \tau 是一个签名,我们写 \text{Sent}_{\mathcal{L}(\tau)} 来表示使用 \mathcal{L} 中的逻辑符号和 \tau 中的关系符号构造的格式良好的句子类。句子 \phi \in \text{Sent}_{\mathcal{L}(\tau)} 据说定义了一个问题 X,以防万一 X 与满足 \phi 的一组 \tau 结构同延 – 即
\{\mathcal{A}_x \mid x \in X \} = \{\mathcal{A} \in \text{Mod}(\tau) \mid \mathcal{A} \models \phi \}
如果 \textbf{C} 是一个复杂度类,那么逻辑 \mathcal{L} 据说可以捕获 \textbf{C},以防万一对于 \textbf{C} 中的每个问题 X \,都有一个签名 \tau 和一个公式 \phi \in \text{Form}_{\mathcal{L}(\tau)} ,其中 定义 X。
第 3 节中考虑的许多主要复杂性类别已经获得了描述性特征,其中一些在表 2 中进行了总结。第一个这样的特征是针对二阶存在逻辑 (\mathsf{SO}\exists) 建立的。该系统的语言包括 \exists Z_1 \ldots \exists Z_n \phi(\vec{x},Z_1,\ldots,Z_n) 形式的公式,其中变量 Z_i 是二阶的,并且 \phi 本身不包含其他二阶量词。 Fagin (1974) 确立了以下观点:
定理 4.2 \textbf{NP} 由逻辑 \mathsf{SO}\exists 捕获。
这一结果提供了重要复杂性类别的第一个独立于机器的特征之一,即其公式不参考特定的计算模型,例如 \mathfrak{T} 或 \mathfrak{A}。这些特征的可用性通常被用来为 \textbf{NP} 等类的数学鲁棒性提供额外的证据。
定理 4.2 概括为构成多项式层次结构的类的表征。例如,逻辑 \Sigma^1_i 和 \Pi^1_i 统一捕获复杂度类 \Sigma^P_i 和 \Pi^P_i (其中 \mathsf{SO}\exists = \Sigma^1_1 )。此外,\mathsf{SO}(即完整的二阶逻辑)捕获\textbf{PH}本身。另一方面,还可以证明一阶逻辑(\mathsf{FO})仅捕获一个非常弱的复杂性类别,称为 \textbf{AC}^0,由可通过恒定深度的多项式大小电路决定的语言组成。
为了表征其他类,必须考虑扩展一阶逻辑表达能力的其他方法,例如添加最小不动点或传递闭包运算符。例如,考虑一个公式 \psi(R,\vec{x}),其中 n 元关系 R 仅出现正数(即在偶数个否定的范围内),并且 \vec{x} 的长度为 m。如果 A 是结构 \mathcal{A} 的域,那么这样的公式将产生 \Phi_{\psi(R,\vec{x})} 类型的单调映射,从 A^n 的幂集到由 \Phi_{\psi(R,\vec{x})}(B) = 定义的 A^m 幂集 \{\vec{a} \in A^m \mid \mathcal{A}^R_B \models \psi(R,\vec{a}) \} 其中 \mathcal{A}^R_B 表示符号 R 被解释为 B \subseteq A^n 的模型,否则与 \mathcal{A} 类似。在这种情况下,映射 \Phi_{\psi(R,\vec{x})} 存在一个最小不动点 – 即集合 F \subseteq A^n 使得 \Phi_{\psi(R,\vec{x})}(F) = F 并且包含在具有此属性的所有其他集合中(例如,参见, 莫斯科瓦基斯 1974)。让我们用 \text{Fix}^{\mathcal{A}}(\psi(R,\vec{x})) 表示这个集合。[46]
逻辑 \textsf{FO}(\texttt{LFP}) 现在可以定义为一阶逻辑的扩展,对于关系变量出现的每个公式 \psi(R,\vec{x}) 使用新的关系符号 \texttt{LFP}_{\psi({R,\vec{x}})} 仅积极地使用 \texttt{LFP}_{\psi({R,\vec{x}})}(\vec{t}) 形式的新原子公式。这些公式解释如下: \mathcal{A} \models \texttt{LFP}_{\psi({R,\vec{x}})}(\vec{t}) 当且仅当 \vec{t}^{\mathcal{A}} \in \text{修复}^{\mathcal{A}}(\psi(R,\vec{x}))。逻辑 \textsf{FO}(\texttt{TC}) 类似地通过添加传递闭包运算符 \texttt{TC}_{\psi(\vec{x})}(\vec{x}) 来定义,该运算符包含项 \vec{t} 以防万一 \vec{t}^{\mathcal{A}} 处于 \mathcal{A} 中由 \psi(\vec{x}) 表示的关系的传递闭包中。逻辑 \textsf{SO}(\texttt{LFP}) 和 \textsf{SO}(\texttt{TC}) 的定义类似,通过将这些运算符添加到 \textsf{SO} 并允许它们应用于包含二阶变量的公式。
我们现在可以陈述描述性复杂性理论的另一个主要结果:
定理 4.3 (Immerman 1982; Vardi 1982) \textbf{P} 由 \textsf{FO}(\texttt{LFP}) 相对于有序模型捕获(即模型 \mathcal{A} 用于将 \leq 解释为 A 上的线性顺序的结构)。
Immerman (1999, p. 61) 将定理 4.3 描述为“增强了我们的直觉,即多项式时间是一类,其基本性质超出了通常定义它的机器模型”。结合定理 4.2,它还提供了 \textbf{P} \neq \textbf{NP}? 的逻辑重构。问题本身 – 即 \textbf{P} \neq \textbf{NP} 当且仅当存在一类可在存在二阶逻辑中定义的有序结构,而该有序结构不能由 \textsf{FO}(\texttt{LFP}) 的公式定义。
另一方面,在定理 4.3 的表述中对有序结构的限制被认为是必不可少的,因为 \textbf{P} 中存在简单可描述的语言 – 例如
\sc{PARITY} = \{w \in \{0,1\}^* : w \text{ 包含奇数个 1}\}
– 如果不使用 \leq 则无法在 \textsf{FO}(\texttt{LFP}) 上定义。更一般地说,存在一种在无序结构上捕获 \textbf{P} 的逻辑的问题是目前描述复杂性中主要的开放问题之一。例如,参见(Ebbinghaus 和 Flum 1999)和(Chen 和 Flum 2010)。
复杂性等级逻辑参考
\textbf{AC}^0 \mathsf{FO} (伊默曼 1999)
\textbf{NL} \textsf{FO}(\texttt{TC}) (Immerman 1987)
\textbf{P} \textsf{FO}(\texttt{LFP}) (Immerman 1982), (Vardi 1982)
\textbf{NP}\textsf{SO}\存在(Fagin 1974)
\Sigma^P_i \textsf{SO}\Sigma^1_i (Stockmeyer 1977)
\Pi^P_i\textsf{SO}\Pi^1_i (Stockmeyer 1977)
\textbf{PH} \textsf{SO} (斯托克迈尔 1977)
\textbf{PSPACE}\textsf{SO}(\texttt{TC}) (Immerman 1987)
\textbf{EXP}\textsf{SO}(\texttt{LFP}) (Immerman 1999)
表 2. 复杂性类别的描述性特征。
4.5 有界算术
逻辑和计算复杂性之间的另一种联系是由一阶算术理论提供的,这些理论在形式上类似于熟悉的系统,例如原始递归算术和皮亚诺算术。形式算术和可计算性理论之间的联系自 20 世纪 40 年代以来就为人所知——例如标准算术模型中由 \Delta^0_1-formulas 和 \Sigma^0_1-formulas 定义的自然数集分别对应于递归和递归可枚举集,\textrm{I}\Sigma^0_1 的可证明总函数对应于本原递归函数,而 \mathsf{PA} 对应于 \epsilon_0-递归函数(例如,参见 Schwichtenberg 2011)。从 20 世纪 70 年代起,人们获得了许多类似的结果,将多项式层次结构的层次与一类统称为有界算术的一阶理论联系起来。
在研究算术和复杂性理论之间的关系的过程中,除了考虑集合之外,考虑函数通常也是有用的。例如,我们可以考虑类 \textbf{FP} =_{\text{df}}\Box^P_1 函数可通过确定性图灵机在多项式时间内计算。类似地,我们将 \Box^P_{n+1} 定义为可通过确定性图灵机在多项式时间内计算的函数类,并使用 \textbf{PH} 级别 \Sigma^P_n 中的集合的预言机。与 \textbf{PH} 的情况一样,不知道层次结构 \Box^P_1 \subseteq \Box^P_2 \subseteq \ldots 是否崩溃。
Cobham (1965) 用类似于定义原始递归函数的函数代数对 \textbf{FP} 进行了原始描述,提供了形式算术与复杂性之间的第一个联系。所讨论的类是由以下基函数类 \mathcal{F}_0 生成的:
z(x) = 0, s_0(x) = 2 \cdot x, s_1(x) = 2 x + 1, \pi^i_n(x_1, \dots ,x_n) = x_i, x \# y = 2^{\lvert x\rvert \cdot \lvert y\rvert}
我们还定义了以下原始递归的变体:
定义 4.1 函数 f(\vec{x},y) 据说是由 g(\vec{x})、h_0(\vec{x},y,z)、h_1(\vec{x},y,z) 和 k(\vec{x},y) 通过符号上的有限递归定义的,以防万一
\begin{对齐} f(\vec{x},0) &= g(\vec{x})\\ f(\vec{x},s_0(y)) &= h_0(\vec{x},y,f(\vec{x},y)) \\ f(\vec{x},s_1(y)) &= h_1(\vec{x},y,f(\vec{x},y)) \end{对齐}
和 f(\vec{x},y) \leq k(\vec{x},y) 对于所有 \vec{x},y。
我们将可通过符号上的有限递归定义的函数类 \mathcal{F} 定义为包含 \mathcal{F}_0 且在组合和上述方案下封闭的最小类。科巴姆原始结果的一个细微变化现在可以表述如下:
定理 4.4 (Cobham 1965; Rose 1984) f(\vec{x}) \in \textbf{FP} 当且仅当 f(\vec{x}) \in \mathcal{F}。
与定理 4.2 和 4.3 一样,定理 4.4 很重要,因为它提供了重要复杂性类别的另一种独立于机器的表征。然而,回想一下,科巴姆的工作正值可行性概念的数学地位仍在争论之中。因此,询问 \mathcal{F} 的定义是否可以理解为提供可行可计算性的独立动机分析也是合理的,类似于人们常说的丘奇和图灵提供的有效可计算性分析。
相对于第 1.1 节中讨论的标准,认为基函数 \mathcal{F}_0 是可行可计算的,并且该属性在组合下得到保留似乎是合理的。现在假设 f(x,y) 是通过 g(x)、h_0(x,y,z)、h_1(x,y,z) 和 k(x,y) 符号的有限递归来定义的。在这种情况下, f(x,y) = h_i(x,\lceil \frac{y}{2} \rceil,f(x,\lceil \frac{y}{2} \rceil)) 取决于 y \gt 0 是偶数 (i = 0) 还是奇数 (i = 1)。由此可见,计算 f(x,y) 值所需的递归深度将与 \log_2(y) 成正比——即与 y 的二进制表示的长度成正比,而不是 y 本身,因为当 f(x,y+1) 通过普通原始递归定义为 h(x,y,f(x,y)) 时。这表明当函数通过符号上的有限递归定义时,可行性也得到保留。
仅仅基于前理论基础,很难促使将函数 x \# y 包含在 \mathcal{F}_0 中,并将条件 f(x,y) \leq k(x,y) 包含在定义 4.1 中。对于 \mathcal{F} 定义的这些特征,可以看出精确地具有将多项式界限放置在辅助函数上的效果,辅助函数可以在刚刚描述的长度有界递归期间计算。另一方面,由于 Leivant (1994)(使用字符串上正二阶可定义性的形式)和 Bellantoni 和 Cook (1992)(使用传统原始递归方案的结构修改),在 \textbf{FP} 的类似功能表征中避免了对多项式增长率的间接引用。
在现在称为 \text{I}\Delta_0 (最初由 Parikh (1971) 以名称 \textsf{PB} 引入)的一阶算术理论的表述中,也避免了直接引用多项式增长率。 \text{I}\Delta_0 是在一阶算术的传统语言上制定的 - 即 \mathcal{L}_a = \{0,s,+,x,\lt\} - 并由 Robinson 的 \mathsf{Q} 公理以及 \mathsf{PA} 算术归纳方案的限制组成 \Delta_0-公式 – 即仅包含 \forall x \leq t 或 \exists x \leq t 形式的有界量词,其中 t 是不包含 x 的项。
在此之前,Bennett (1962) 已经证明存在一个 \Delta_0 公式 \varepsilon(x,y,z),它定义了相对于算术标准模型的幂函数的图形。 \text{I}\Delta_0 证明 \varepsilon(x,y,z) 满足求幂的标准定义方程。但也可以证明,该理论并未在以下意义上证明该定义或任何其他定义下的幂运算的总体性: