二階邏輯

在邏輯和數學中，二階邏輯是一階邏輯的擴展，一階邏輯是命題邏輯的擴展。二階邏輯接着被高階邏輯和類型論所擴展。

一階邏輯和二階邏輯都使用了論域（有時叫做「域」或「全集」）的想法。論域是可以在其上量化的個體元素的集合。一階邏輯只包括取值為論域的個體元素的變量和量詞。例如在一階句子∀x(x ≠ x + 1)中變量x被用來表示一個任意的個體。二階邏輯擴展了一階邏輯，通過增加取值在個體的集合上變量和量詞。例如，二階句子$\forall S\forall x{\Big (}x\in S\vee x\notin S{\Big )}$聲稱對於所有個體的集合S和所有的個體x，要麼x在S中要麼不在（這是二值原理）。最一般的二階邏輯還包括量化在函數上的變量，和在下面語法章節解說的變量。

二階邏輯的表達能力

二階邏輯比一階邏輯更有表達力。例如，如果論域是所有實數的集合，我們可以在一階邏輯中斷言每個實數都有一個加法逆元：∀x ∃y(x + y = 0)，但是需要二階邏輯來斷言實數的集合的上確界性質，它聲稱實數的所有有界的、非空集合都有上確界。如果論域是所有實數的集合，下列二階邏輯句子表達了最小上界性質：

$\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語義經常用在二階算術的研究中。

演繹系統

邏輯的演繹系統是確定哪些公式序列構成有效證明的一組推理規則和邏輯公理。很多演繹系統可以用於二階邏輯，儘管它們都不能針對標準語義（見後）是完備的。每個這種系統都是可靠的，這以為它們可以證明的任何句子在適當的語義中都是邏輯有效的。

可用的最弱的演繹系統由標準的一階邏輯演繹系統（比如自然演繹）擴充上對二階項的代換規則。這種演繹系統常用於二階算術的研究中。

Shapiro (1991)和Henkin（1950）考慮的演繹系統想擴充的一階演繹系統增加了內涵公理和選擇公理二者。這些公理對於二階語義是可靠的。它們對於Henkin語義是可靠的，只要考慮的是滿足內涵和選擇公理的Henkin模型。

為什麼二階邏輯不能歸約成一階邏輯

一個樂觀的人可能嘗試按下述方法把二階邏輯歸約成一階邏輯。把論域從所有實數的集合擴展為所有實數集合的集合。向語言增加一個新的二元謂詞：成員資格關係。這樣，二階的句子就成為一階的了。

但要注意這個論域被斷言為包括實數的「所有」集合。這個需求沒有被簡約到到一階句子! 真有某種方式來完成這種簡約嗎?經典的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）是沒有全稱量詞的二階邏輯。在詞$w\in \Sigma ^{*}$之上，所有的MSO公式都可以轉換成確定的有窮自動機。它可以再轉換成EMSO公式。所以EMSO和MSO在這種詞上是等價的。對於樹作為輸入，這個結果同樣成立。但是，在有限網格$\Sigma ^{++}$之上，這個性質不再成立，因為瓦片系統識別的語言不閉合於補集之下。因為全稱量詞等價於否定的存在量詞，它不能被表達，全稱和存在量詞的交替生成了在$\Sigma ^{++}$上的更大的一類語言。

應用於複雜性理論

二階邏輯的各種形式的表達力密切的連繫於計算複雜性理論。特別是：

• NP是用存在性二階邏輯可表達的語言集合。
• co-NP是用全稱二階邏輯可表達的語言的集合。
• PH是用二階邏輯可表達的語言的集合。
• PSPACE是用帶有增加的傳遞閉包算子的二階邏輯可表達的語言的集合。
• EXPTIME是用帶有增加的最小不動點算子的二階邏輯可表達的語言的集合。

在這些語言類之間的聯繫直接影響了邏輯的相對的表達力；例如，如果PH=PSPACE，則向二階邏輯增加的傳遞閉包算子不使它更有表現力。

參考文獻

• 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. First-Order Logic, Second-Order Logic, and Completeness (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）.  （頁面存檔備份，存於互聯網檔案館）