二階邏輯

在逻辑和数学中，二阶逻辑是一阶逻辑的扩展，一阶逻辑是命题逻辑的扩展^{[註 1]}。二阶逻辑接着被高阶逻辑和类型论所扩展。

一阶逻辑和二阶逻辑都使用了论域（有时叫做“域”或“全集”）的想法。论域是可以在其上量化的个体元素的集合。一阶逻辑只包括取值为论域的个体元素的变量和量词。例如在一阶句子∀x(x ≠ x + 1)中变量x被用来表示一个任意的个体。二阶逻辑扩展了一阶逻辑，通过增加取值在个体的集合上变量和量词。例如，二阶句子${\displaystyle \forall S\forall x{\Big (}x\in S\vee x\notin S{\Big )}}$声称对于所有个体的集合S和所有的个体x，要么x在S中要么不在（这是二值原理）。最一般的二阶逻辑还包括量化在函数上的变量，和在下面语法章节解说的变量。

二阶逻辑的表达能力

二阶逻辑比一阶逻辑更有表达力。例如，如果论域是所有实数的集合，我们可以在一阶逻辑中断言每个实数都有一个加法逆元：∀x ∃y(x + y = 0)，但是需要二阶逻辑来断言实数的集合的上确界性质，它声称实数的所有有界的、非空集合都有上确界。如果论域是所有实数的集合，下列二阶逻辑句子表达了最小上界性质：

${\displaystyle \forall A{\Big [}(\exists w(w\in A)\land \exists z\,\forall w(w\in A\rightarrow w\leq z))\rightarrow \exists x\,\forall y([\forall w(w\in A\rightarrow w\leq y)]\leftrightarrow x\leq y){\Big ]}}$ 

在二阶逻辑中，有可能写出声称“论域是有限的”或“论域有可数势的”这样的形式句子。要说论域是有限的，可使用声称从论域到自身的所有单射函数都是满射的句子。要声称论域有可数势，可以使用声称在所有的论域的两个無限子集之间存在双射的句子。从向上勒文海姆–斯科伦定理得出在一阶逻辑内不可能特征化有限性或可数性。

语形

二阶逻辑的语法规定那些表达式是合式公式。除了一阶逻辑的语形之外，二阶逻辑包括了很多新「种类」（有时叫做「类型」）的变量。包括：

• 取值在个体的集合上的一类变量。如果S是此类变量而t是一阶项，则表达式t ∈ S（也写为S(t)或 St）是原子公式。个体的集合还可以写为论域上的一元关系。
• 对于所有自然数k，有取值在所有在个体上的k元关系的一类变量。如果R是这样的k元关系变量而t₁,..., t_k是一阶项，则表达式R(t₁,...,t_k)是原子公式。
• 对于所有自然数k，存在取值在接受论域的k个元素并返回这个论域的一个元素的函数上一类变量。如果f是这样的k元函数符号而t₁,...,t_k是一阶项，则表达式f(t₁,...,t_k)是一阶项。

对于刚才定义的每类变量，允许使用全称和/或存在量词来建造公式。所以有很多种类的量词，每类变量两个。

在二阶逻辑中的「句子」同一阶逻辑一样也是没有（任何种类的）自由变量的合式公式。

在「一元二阶逻辑」中，只增加了给论域的子集的变量。有所有种类的变量的二阶逻辑有时叫做「完全二阶逻辑」来区别于一元（monadic）二阶逻辑。

同于一阶逻辑，二阶逻辑可以在特定二阶语言中包含非逻辑符号。但是它们是受限制于它们形成的所有项必须要么是一阶项（它可以代换一阶变量）要么是二阶项（它可以代换适当种类的二阶变量）。

语义

二阶逻辑的语义建立每个句子的意义。不像只有一个标准语义的一阶逻辑，二阶逻辑有两个常用的不同语义：「标准语义」和「Henkin语义」。在这些语义中，一阶量词和逻辑连结词的解释是同于一阶逻辑的。只有在二阶量词变量的新量词需要定义语义。

在标准语义中，量词取值于适当种类的“所有”集合或函数上。所以一旦确立了一阶变量的论域，余下的量词的意义就固定了。这种语义给予了二阶逻辑强大的表达能力，本文采用了这种语义。

在Henkin语义中，每个二阶变量种类都有它自己取值的特定论域，它可以是所有此类的所有集合或函数的真子集。Leon Henkin（1950）定义了这种语义并证明了对一阶逻辑成立的哥德尔完全性定理和紧致性定理，在有Henkin语义的二阶逻辑中继续有效。这是因为Henkin语义几乎等同于多种类一阶语义，它通过增加额外的变量种类来模拟二阶逻辑的新变量。带有Henkin语义的二阶逻辑不比一阶逻辑有更大表达能力。Henkin语义经常用在二阶算术的研究中。

演绎系统

逻辑的演绎系统是确定哪些公式序列构成有效证明的一组推理规则和逻辑公理。很多演绎系统可以用于二阶逻辑，尽管它们都不能针对标准语义（见後）是完备的。每个这种系统都是可靠的，这以为它们可以证明的任何句子在适当的语义中都是逻辑有效的。

可用的最弱的演绎系统由标准的一阶逻辑演绎系统（比如自然演绎）扩充上对二阶项的代换规则^{[註 2]}。这种演绎系统常用于二阶算术的研究中。

Shapiro (1991)和Henkin（1950）考虑的演绎系统想扩充的一阶演绎系统增加了内涵公理和选择公理二者。这些公理对于二阶语义是可靠的。它们对于Henkin语义是可靠的，只要考虑的是满足内涵和选择公理的Henkin模型^{[註 3]}。

为什么二阶逻辑不能归约成一阶逻辑

一个乐观的人可能尝试按下述方法把二阶逻辑归约成一阶逻辑。把论域从所有实数的集合扩展为所有实数集合的集合。向语言增加一个新的二元谓词：成员资格关系。这样，二阶的句子就成为一阶的了。

但要注意这个论域被断言为包括实数的「所有」集合。这个需求没有被简约到到一阶句子! 真有某种方式来完成这种简约吗?经典的Löwenheim-Skolem定理蕴含了这是没有的。这个定理蕴含了有某个「R」的可数无限子集，它的成员我们称为“内在数”，和某个内在数集合的可数无限搜集，它的成员我们称为“内在集合”，而由内在数和内在集合组成的这个论域满足实数和实数集合所满足的所有一阶句子。特别是，它有效的满足一种最小上界公理：

有“内在”上界的所有非空“内在”集合都有最小“内在”上界。

所有内在数的集合的可数性（联合上这些形成稠密的有序集合的事实）必然的蕴含了这个集合不满足完全的最小上界公理。所有“内在”集合的集合的可数性必然的蕴含了它不是所有“内在”数的集合的“所有”子集的集合（因为康托尔定理蕴含了可数无限集合的所有子集的集合是不可数无限集合）。这个构造密切关联于斯科伦悖论。

所以实数和实数的集合的一阶理论可以有很多模型，其中一些是可数的。但是实数的二阶理论只有一个模型。这可以从只有一个阿基米德完备有序域的经典定理，和所有阿基米德完备有序域的在二阶逻辑中可表达的事实得出。这证实了实数的二阶理论不能简约到一阶理论，在实数的二阶理论之後一个模型但对应的一阶理论有很多模型的意义上。

有很多极端例子证实带有标准语义的二阶逻辑要比一阶逻辑表达能力强。有一个有限二阶理论其唯一的模型是实数的，如果连续统假设成立，而它没有模型如果连续统假设不成立。这个理论由把实数刻画为完备阿基米德有序域加上声称这个域是第一个不可数势的公理的所有有限理论构成，这个例子展示了二阶逻辑中的一个句子是否是相容的是非常微妙的问题。

下一节中描述二阶逻辑的另外的限制。

二阶逻辑和元逻辑结论

作为哥德尔不完全性定理的必然结果，你不要打算让二阶公式的“可证明性”能给出同时满足下面三个想要的特性的语言的标准释义（或简化的一个标准语义）:

• （可靠性）每个可证明的二阶逻辑句子是普遍有效的，就是在所有域上有效。

• （完备性）每个普遍有效的二阶公式是可证明的。

• （实效性）有一个证明检验算法。（这第三个条件经常被接纳不过它没有被明确的规定。）

有时候这表达为二阶逻辑不容许完备的证明论。

在这方面二阶逻辑不同于一阶逻辑，至少这是逻辑学家避免使用它的一个理由。（确切的说，蒯因有时以此作为不把二阶逻辑作为逻辑看待的理由）。按照George Boolos所指出的，虽然这种不完备性只进入了多元二阶逻辑中：在n-元谓词上量化的逻辑，这裡的n > 1。但是限制于一元谓词的一元二阶逻辑不只是完备的和相容的（consistent）而且是可判定性的--就是说，每个真定理的证明不只是可能的而且可以通过机械方法确定的达到。在这方面，一元二阶逻辑比多元一阶逻辑更加进步：一元二阶逻辑是完备的，相容的和可判定的，但多元一阶逻辑，尽管是相容的和完备的，它不再是可判定的（参见停机问题）。

在1950年Leon Henkin用Henkin语义给出对二阶逻辑的充分的（就是说完备的和可靠的）和简洁的证明。在标准和Henkin语义之间唯一区别是，在Henkin语义中谓词变量的域是（这个域的）个体的集合的一个任意集合，而不是（这个域的）个体的所有集合的集合。他的这个证明同对一阶函数演算做的证明在一起进行的。这两个结论包含在他的学位论文中。

二阶逻辑的历史和有争议的价值

当谓词逻辑被弗雷格（独立的和更有影响力的皮尔士，他提出了术语“二阶逻辑”）介绍给数学社区的时候，他确实使用不同的变量来区分在物体上量化和在属性和集合上的量化；但是他自己没有去区分出两类不同的逻辑。在发现罗素悖论之後，认识到了他的系统有些毛病。最终逻辑学家建立了以各种方式做限制的弗雷格逻辑—现在叫做一阶逻辑—除去了这个问题：集合和谓词在一阶逻辑中不能被单独量化。现在标准的逻辑的阶数等级就是从那时开始的。

发现了集合论可以在一阶逻辑的设施内公式化为公理化系统（损失了某种完备性，但是不至于象罗素悖论那么糟糕），并且真就这么做了（参见Zermelo-Fraenkel集合论），因为集合是数学的关键。算术、分体论和各种其他强力逻辑理论可以被公理化的公式化，而不用使用比一阶量化更多的逻辑设施，随着哥德尔和Skolem忠于一阶逻辑，导致了对二（或更高）阶逻辑的工作的普遍放弃。

这种舍弃由一些逻辑学家活跃的推动着，最著名的是蒯因。蒯因推进了这种观点，在谓词语言句子比如Fx中，x被认为是一个变量或指称一个物体的名字，所以可以被量化，如“对于所有的东西，情况是. . .”。但是F被认为是一个不完整句子的“一个缩写”，不是一个物体（甚至不是抽象的物体如性质）的名字。例如，它可能意味着“ . . .是个狗”，认为在这种事物上可以做量化是没有什么意义的。（这种立场同弗雷格自己对概念-物体区别的讨论是非常一致的）。所以要使用一个谓词作为变量就要让它占据只有个别的变量可以占据的一个名字的位置。这种推理被Boolos拒绝了。

近年来二阶逻辑有某种程度的恢复，由George Boolos把二阶量化解释为在同一阶量化一样的域上的复数量化所支持。Boolos进一步指出句子的非一阶可表达性，比如“有些罪犯只相互倾慕”和“有些Fianchetto人进入仓库而没有任何别人陪同”。这只能用二阶量化的完全力量来表达。（实际上这不是真的，因为一般性的量化和偏序的（或分支的）量化同样足以表达特定类的非一阶可表达的句子而不使用二阶量化)。

但是，已经说过在有些数学分支中比如拓扑学中，需要二阶逻辑的能力来做完整的表达。这方面的工作已经由Stephen G. Simpson在逆数学的名义下完成了。已经证明了二阶逻辑不只对表达经典数学的某些重要部分是必须的，而且它也可以用做模型论和数学基础的工具。

存在性片段在有限结构上的能力

单类二阶逻辑（MSO）的存在性片段（EMSO）是没有全称量词的二阶逻辑。在词${\displaystyle w\in \Sigma ^{*}}$ 之上，所有的MSO公式都可以转换成确定的有穷自动机。它可以再转换成EMSO公式。所以EMSO和MSO在这种词上是等价的。对于树作为输入，这个结果同样成立。但是，在有限网格${\displaystyle \Sigma ^{++}}$ 之上，这个性质不再成立，因为瓦片系统识别的语言不闭合于补集之下。因为全称量词等价于否定的存在量词，它不能被表达，全称和存在量词的交替生成了在${\displaystyle \Sigma ^{++}}$ 上的更大的一类语言。

应用于复杂性理论

二阶逻辑的各种形式的表达力密切的连系于计算复杂性理论。特别是：

• NP是用存在性二阶逻辑可表达的语言集合。
• co-NP是用全称二阶逻辑可表达的语言的集合。
• PH是用二阶逻辑可表达的语言的集合。
• PSPACE是用带有增加的传递闭包算子的二阶逻辑可表达的语言的集合。
• EXPTIME是用带有增加的最小不动点算子的二阶逻辑可表达的语言的集合。

在这些语言类之间的联系直接影响了逻辑的相对的表达力；例如，如果PH=PSPACE，则向二阶逻辑增加的传递闭包算子不使它更有表现力。

注释

1. Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.
2. Such a system is used without comment by Hinman (2005).
3. These are the models originally studied by Henkin (1950).

参考文献

• Henkin, L. Completeness in the theory of types. Journal of Symbolic Logic. 1950, 15: 81–91. 
• Hinman, P. Fundamentals of Mathematical Logic. A K Peters. 2005. ISBN 978-1-56881-262-5. 
• Shapiro, S. Foundations without Foundationalism: A Case for Second-order Logic. Oxford University Press. 2000. ISBN 978-0-19-825029-6. 
• Rossberg, M. (PDF). V. Hendricks et al, eds. (编). First-order logic revisited. Berlin: Logos-Verlag. 2004 [2008-01-03]. （原始内容 (PDF)存档于2008-04-07）.  （页面存档备份，存于互联网档案馆）
• Vaananen, J. Second-Order Logic and Foundations of Mathematics. Bulletin of Symbolic Logic. 2001, 7 (4): 504–520 [2008-01-03]. doi:10.2307/2687796. （原始内容于2020-03-21）.  （页面存档备份，存于互联网档案馆）