查看“︁二階邏輯”︁的源代码

{{Refimprove|time=2020-01-28T10:19:58+00:00}}
{{Expert|time=2019-09-24}}

在[[逻辑]]和[[数学]]中，'''二阶逻辑'''是[[一阶逻辑]]的扩展，一阶逻辑是[[命题逻辑]]的扩展{{NoteTag|Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.}}。二阶逻辑接着被[[高阶逻辑]]和[[类型论]]所扩展。

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

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

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

== 语形 ==
二阶逻辑的语法规定那些表达式是合式[[公式 (数理逻辑)|公式]]。除了一阶逻辑的语形之外，二阶逻辑包括了很多新「种类」（有时叫做「[[类型论|类型]]」）的变量。包括：
* 取值在个体的集合上的一类变量。如果''S''是此类变量而''t''是一阶项，则表达式''t'' ∈ ''S''（也写为''S''(''t'')或 ''St''）是原子公式。个体的集合还可以写为论域上的[[一元关系]]。
* 对于所有自然数''k''，有取值在所有在个体上的''k''元关系的一类变量。如果''R''是这样的''k''元关系变量而''t''<sub>1</sub>,..., ''t''<sub>''k''</sub>是一阶项，则表达式''R''(''t''<sub>1</sub>,...,''t''<sub>''k''</sub>)是原子公式。
* 对于所有自然数''k''，存在取值在接受论域的''k''个元素并返回这个论域的一个元素的函数上一类变量。如果''f''是这样的''k''元函数符号而''t''<sub>1</sub>,...,''t''<sub>''k''</sub>是一阶项，则表达式''f''(''t''<sub>1</sub>,...,''t''<sub>''k''</sub>)是一阶项。
对于刚才定义的每类变量，允许使用全称和/或存在量词来建造公式。所以有很多种类的量词，每类变量两个。

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

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

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

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

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

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

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

可用的最弱的演绎系统由标准的一阶逻辑演绎系统（比如[[自然演绎]]）扩充上对二阶项的代换规则{{NoteTag|Such a system is used without comment by Hinman (2005).}}。这种演绎系统常用于[[二阶算术]]的研究中。

Shapiro (1991)和Henkin（1950）考虑的演绎系统想扩充的一阶演绎系统增加了内涵公理和选择公理二者。这些公理对于二阶语义是可靠的。它们对于Henkin语义是可靠的，只要考虑的是满足内涵和选择公理的Henkin模型{{NoteTag|These are the models originally studied by Henkin (1950).}}。

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

但要注意这个论域被断言为包括实数的「所有」集合。这个需求没有被简约到到一阶句子! 真有某种方式来完成这种简约吗?经典的[[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]]）是没有全称量词的二阶逻辑。在词<math>w \in \Sigma^*</math>之上，所有的MSO公式都可以转换成[[有限状态自动机|确定的有穷自动机]]。它可以再转换成EMSO公式。所以EMSO和MSO在这种词上是等价的。对于树作为输入，这个结果同样成立。但是，在有限网格<math>\Sigma^{++}</math>之上，这个性质不再成立，因为[[瓦片系统]]识别的语言不[[闭包 (数学)|闭合]]于[[补集]]之下。因为全称量词等价于否定的存在量词，它不能被表达，全称和存在量词的交替生成了在<math>\Sigma^{++}</math>上的更大的一类语言。

== 应用于复杂性理论 ==
二阶逻辑的各种形式的表达力密切的连系于[[计算复杂性理论]]。特别是：
* [[NP（复杂度）|NP]]是用存在性二阶逻辑可表达的语言集合。
* co-NP是用全称二阶逻辑可表达的语言的集合。
* [[PH（复杂度）|PH]]是用二阶逻辑可表达的语言的集合。
* [[PSPACE]]是用带有增加的[[传递闭包]]算子的二阶逻辑可表达的语言的集合。
* [[EXPTIME]]是用带有增加的[[最小不动点]]算子的二阶逻辑可表达的语言的集合。
在这些语言类之间的联系直接影响了逻辑的相对的表达力；例如，如果'''PH'''='''PSPACE'''，则向二阶逻辑增加的传递闭包算子不使它更有表现力。

== 注释 ==
{{NoteFoot}}

== 参考文献 ==
{{Reflist}}
{{ReflistH}}
* {{cite journal en
 | author = Henkin, L.
 | url = http://links.jstor.org/sici?sici=0022-4812%28195006%2915%3A2%3C81%3ACITTOT%3E2.0.CO%3B2-I
 | title = Completeness in the theory of types
 | journal = Journal of Symbolic Logic
 | volume = 15
 | year = 1950
 | pages = 81–91
 }}
* {{cite book en
 | author = Hinman, P.
 | title = Fundamentals of Mathematical Logic
 | publisher = A K Peters
 | year = 2005
 | ISBN = 978-1-56881-262-5
 }}
* {{cite book en
 | author = Shapiro, S.
 | title = Foundations without Foundationalism: A Case for Second-order Logic
 | publisher = Oxford University Press
 | year = 2000
 | ISBN = 978-0-19-825029-6
 }}
* {{cite conference
 |author       = Rossberg, M.
 |url          = http://www.st-andrews.ac.uk/~mr30/papers/RossbergCompleteness.pdf
 |title        = First-Order Logic, Second-Order Logic, and Completeness
 |book-title   = First-order logic revisited
 |editor       = V. Hendricks ''et al'', eds.
 |publisher    = Logos-Verlag
 |location     = Berlin
 |date         = 2004
 |dead-url     = yes
 |archive-url  = https://web.archive.org/web/20080407051012/http://www.st-andrews.ac.uk/~mr30/papers/RossbergCompleteness.pdf
 |archive-date = 2008-04-07
 |access-date  = 2008-01-03
}} {{Wayback|url=http://www.st-andrews.ac.uk/~mr30/papers/RossbergCompleteness.pdf |date=20080407051012 }}
* {{cite journal en
 | author = Vaananen, J.
 | url = http://www.math.ucla.edu/~asl/bsl/0704/0704-003.ps
 | title = Second-Order Logic and Foundations of Mathematics
 | journal = Bulletin of Symbolic Logic
 | volume = 7
 | issue = 4
 | year = 2001
 | pages = 504–520
 | doi = 10.2307/2687796
 | access-date = 2008-01-03
 | archive-date = 2020-03-21
 | archive-url = https://web.archive.org/web/20200321025624/https://www.math.ucla.edu/~asl/bsl/0704/0704-003.ps
 | dead-url = no
 }} {{Wayback|url=http://www.math.ucla.edu/~asl/bsl/0704/0704-003.ps |date=20200321025624 }}
{{ReflistF}}


{{数理逻辑|state=expanded}}
[[Category:形式逻辑系统| ]]