二阶逻辑 · aiwiki.page

二阶逻辑是一阶逻辑的扩展，它不仅允许对个体对象进行量化，还允许对这些对象的性质和关系进行量化；在某些表述中，也允许对函数进行量化。因此，二阶逻辑的独特之处在于变量的取值范围，而不是公式中量词的数量。同一种二阶语言可以采用不同的解释：全语义使其表达能力远超一阶逻辑，而亨金语义则支持完备且有效的演绎演算。(math.uchicago.edu)

语法与量化

一阶变量通常记作 $x,y,z$ ，其取值范围是论域中的元素。二阶变量通常记作 $X,Y,R$ ，其取值范围是性质或关系。一元关系被解释为论域的一个子集，二元关系被解释为有序对的集合， $n$ 元关系则被解释为 $n$ 元组的集合。每个关系变量都有指定的元数。(math.uchicago.edu)

例如，

\exists X\,\forall x\bigl(X(x)\leftrightarrow P(x)\bigr)

表示存在一种性质 $X$ ，恰好满足 $P$ 的那些对象具有这一性质。相比之下，在一阶公式 $\forall x\,P(x)$ 中， $P$ 是一个固定的谓词符号：该公式量化的是对象，而不是 $P$ 的各种可能解释。(plato.stanford.edu)

有些表述还包含以函数为取值的变量。函数量化也可以用描述函数图像的关系变量来表示，并附加条件，确保每个输入都有唯一的输出。三阶及更高阶语言进一步扩展了这种安排，允许对性质的性质或其他更高类型的对象进行量化。(plato.stanford.edu)

全语义与亨金语义

如何解释二阶量词，是两种方法之间最核心的分歧。

在全语义（也称标准语义）下，一元变量的取值范围是个体论域 $D$ 的整个幂集 $\mathcal P(D)$ 。 $n$ 元关系变量的取值范围则是 $D^n$ 的所有子集。因此，“每一种性质”也包括无法用该语言中的任何公式定义的性质。(mv.helsinki.fi)

在亨金语义下，每一种关系类型都有一个指定的可容许关系集合，其中不必包含论域上的所有关系。这些集合的解释构成模型的一部分。因此，一个全称二阶陈述可能在某个亨金模型中成立，因为它对所有可用的性质都成立；但当所有子集都可用时，它却可能不成立。(mv.helsinki.fi)

相关术语的用法并不统一：任意限制取值范围的解释通常称为一般模型，而亨金模型有时专指满足某组指定的概括公理及其他公理的一般模型。典型的概括原则具有如下形式：

\exists X\,\forall x\bigl(X(x)\leftrightarrow\varphi(x)\bigr),

其中 $X$ 在 $\varphi$ 中不自由出现。它保证由 $\varphi$ 表达的性质是可用的。这类原则本身并不能强制可用性质的集合等于整个幂集。(mv.helsinki.fi)

亨金语义可以用多类一阶逻辑来表示：为个体和关系分别设置不同的类，并用谓词表示关系的应用。这种翻译是其完备性及其他类似一阶逻辑的性质的基础。(ps.uni-saarland.de)

归纳法与范畴性公理化

二阶逻辑的一项主要数学应用，是用单条公理表达数学归纳法。对于常量 $0$ 和后继函数 $S$ ，二阶归纳公理为：

\forall X\left[ \left(X(0)\land \forall x\bigl(X(x)\rightarrow X(S(x))\bigr)\right) \rightarrow \forall x\,X(x) \right].

它表示：凡是在零处成立、且在后继运算下保持成立的性质，都在整个论域中成立。在全语义下，将它与其余的皮亚诺公理结合起来，就能在相差一个同构的意义下唯一刻画自然数。这一性质称为范畴性。(ps.uni-saarland.de)

一阶算术则使用归纳公理模式，每个公式对应其中的一个实例。在亨金语义下，二阶归纳同样只对可用的性质进行量化，因此无法保证同样的外部范畴性。(plato.stanford.edu)

全语义下的二阶公理也能以类似方式将实数刻画为完备有序域：其中的最小上界条件对所有非空有界子集进行量化。这些例子说明了全语义对于确定预期数学结构的重要性。(plato.stanford.edu)

有效性、完备性与紧致性

对于不加限制的全语义，逻辑有效的二阶语句所组成的集合不是递归可枚举的。不存在一个可靠且有效的证明演算，能够恰好推导出所有这类有效语句。这个结论比仅仅说有效性不可判定更强：一阶有效性同样不可判定，但一阶逻辑具有有效且完备的演算。(ps.uni-saarland.de)

范畴性并不能消除哥德尔不完备定理所揭示的现象。它在语义上确定了预期结构，却没有提供一种有效程序来证明关于该结构的每一个真命题。语义上的确定性与有效可证明性是不同的要求。(ps.uni-saarland.de)

在亨金语义下，适当的演算是可靠且完备的。紧致性定理和勒文海姆—斯科伦定理也可以通过向一阶逻辑的翻译迁移过来。在全语义下，它们通常的一阶形式则不再成立。(ps.uni-saarland.de)

一个直观的紧致性反例，是将全语义下的二阶皮亚诺公理与一个常量 $c$ 以及下列语句放在一起：

c\ne 0,\quad c\ne S(0),\quad c\ne S(S(0)),\quad\ldots.

从中选出的任意有限组语句都是可满足的，只需为 $c$ 选取一个足够大的自然数即可。然而，整个语句集合不可满足，因为范畴性排除了与每一个数码都不同的元素。这一构造将范畴性与紧致性的定义结合起来。(ps.uni-saarland.de)

片段与计算应用

**一元二阶逻辑**将二阶变量限制为一元关系，即个体的集合，同时允许使用序关系等固定关系。将有限词表示为带有字母谓词的有序位置结构时，它所能定义的恰好是正则语言。它与有限自动机之间的有效对应提供了判定程序，也为形式验证中的应用奠定了基础。这里的可判定性针对的是某个指定的结构类，而不是不受限制的二阶逻辑。(arxiv.org)

存在二阶逻辑由如下形式的语句组成：

\exists R_1\cdots\exists R_k\,\varphi,

其中 $\varphi$ 是一阶公式。1974 年发表的费金定理指出，在标准编码下，对于有限关系结构，这一片段中可定义的性质恰好是复杂性类 NP 中的性质。这揭示了逻辑可定义性与计算复杂性之间的一项基础性联系。(arxiv.org)

例如，图的三色可着色性可以这样表达：通过存在量化选取三个顶点集合，再用一阶条件要求它们构成顶点集的一个划分，且任何边的两个端点都不属于同一个集合。二阶量化提供候选证书，一阶部分则检验该证书是否满足条件。(arxiv.org)

历史与基础问题

戈特洛布·弗雷格在 1879 年的《概念文字》中引入了二阶量化，并于 1884 年使用了“二阶”一词。莱昂·亨金在 1950 年的研究中，证明了高阶语言在一种广义解释下的完备性，使全语义与一般语义之间的区别成为此后研究的基础。(plato.stanford.edu)

基础层面的讨论关注对所有性质进行量化的地位，以及解释这种量化所需的数学假设。全语义通常在集合论中定义，因此其表达能力依赖于对集合的背景理解。亨金语义使有效演绎成为可能，但一般不能保留全语义对预期无限结构的刻画。在两者之间作出选择，改变的是表达能力、模型与证明之间的关系，而不仅仅是记号。(mv.helsinki.fi)

参考来源

Second-order and Higher-order Logicplato.stanford.edu
A Logical Insight into the Theory of Computationmath.uchicago.edu
Second-order logicmv.helsinki.fi
Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coqps.uni-saarland.de
Completeness in the theory of typescir.nii.ac.jp
Lecture Notes on Monadic First- and Second-Order Logic on Stringsarxiv.org
Existential Second-Order Logic Over Graphs: A Complete Complexity-Theoretic Classificationarxiv.org