二階邏輯

维基百科，自由的百科全书

在数理逻辑中，二阶逻辑是命题逻辑或一阶逻辑的扩展，它包含在谓词位置上(而不是像一阶逻辑那样只能在项的位置上)的变量，和约束它们的量词。所以:

$\forall F\ F(\mathrm{jones}) \lor \neg F(\mathrm{jones})\,$

我们可以表达关于 Jones 的二值原理: 对于所有性质，Jones 要么有它要么没有它。

作为另一个例子，我们用一阶逻辑可以把一个句子/断定写成:

$\exists x\ P(x)$

但是我们不能对谓词做同样的事情。就是说，下列表达式:

$\exists P\ P(x)$

不是一阶逻辑的句子。但它是二阶逻辑的合法的句子。

二阶逻辑允许有各种解释；它经常被认为包含在域的子集上，或在来自这个域到自身的函数上的量化，而不只是在这个域的个别成员之上。例如，如果这个域是所有实数的集合，通过如下书写你可以在一阶逻辑中断言每个实数的加性逆元的存在性

$\forall x\ \exists y\ x+y=0$

但你需要使用二阶逻辑来断言实数的最小上界性质:

$\forall A\subseteq R\ [\cdots\cdots]$

并在点的位置插入一个陈述，如果 A 是非空并且它在 R 中有一个上界，则A 在 R 中有一个最小上界。

(数学符号表)

[编辑] 为什么二阶逻辑不能简约成一阶逻辑

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

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

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

所有内在数的集合的可数性(联合上这些形成稠密的有序集合的事实)必然的蕴含了这个集合不满足完全的最小上界公理。所有内在集合的集合的可数性必然的蕴含了它不是所有内在数的集合的所有子集的集合(因为康托定理蕴含了可数无限集合的所有子集的集合是不可数无限集合)。

在一阶和二阶逻辑之间的另一个深刻的差别是下一节的主题。

[编辑] 二阶逻辑和元逻辑结论

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

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

(完备性)每个普遍有效的二阶公式是可证明的。

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

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

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

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

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

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

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

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

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

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

[编辑] 存在性片段在有限结构上的能力

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