人工智慧/邏輯/表示/二階邏輯
首次釋出於2007年12月20日星期四；實質性修訂於2009年3月4日星期三
二階邏輯是謂詞邏輯的擴充套件，除了像“對於所有物件（在論域中）”這樣的量詞之外，它還包含像“對於所有物件的性質（在論域中）”這樣的量詞。這種對語言的增強增加了其表達能力，而沒有新增新的非邏輯符號，例如新的謂詞符號。對於經典的外延邏輯（如本條目中），性質可以與集合等同起來，因此二階邏輯為我們提供了量詞“對於所有物件的集合”。
對二階邏輯語義有兩種方法。它們在對短語“對於所有物件的集合”的解釋上有所不同。這個短語是否具有我們可以參考的固定含義，或者我們需要考慮這個短語可能具有的各種含義？在第一種情況下（將被稱為標準語義），我們正在預設某些數學概念。在第二種情況下（將被稱為一般語義），假設的要少得多。在這種情況下，要被認為是有效的，一個句子需要在“對於所有物件的集合”短語的所有允許含義下都為真。
在符號邏輯中，公式 (Px → Px) 將為真，無論將論域中的哪個物件分配給變數 x。也就是說，除了 ∀x(Px → Px) 將為真之外，無論用來解釋謂詞符號 P 的論域的哪個子集是什麼。但這不就意味著公式 ∀P ∀x(Px → Px) 為真，無論什麼？
在一階語言中，有些東西我們可以說，有些東西我們不能說。例如，假設我們想要表達關於自然數算術的事實。也就是說，我們想要表達關於結構 (N; 0, S, <, +, ×) 的事實，該結構由自然數集合 N = {0, 1, ...} 以及常見的算術運算和關係組成。我們希望使用一個一階語言，其中量詞 ∀ 解釋為“對於所有自然數”，而 ∃ 解釋為“對於某個自然數”。此外，我們在語言中包含一個常量符號 0 來表示數字零，一個一元函式符號 S 來表示後繼運算（應用於自然數時，得到下一個自然數），一個二元謂詞符號 < 來表示 N 上的排序關係 <，以及兩個二元函式符號 + 和 × 來分別表示加法和乘法。
有了這種語言，我們現在可以象徵我們知道關於自然數的許多事實。例如，我們可以形成句子 ∀x(x < Sx)，表達了每個數字都小於下一個數字的事實。但是，如果我們想要表達“良序性質”，即任何非空自然數集都有一個最小成員，就會出現困難。如果 P 是一個新的單元謂詞符號，那麼
∃x Px → ∃x(Px & ∀y(Py → (y = x v x < y)))
表達了 P 如果對任何數字都為真，那麼 P 對某個最小數字為真的想法。當我們將謂詞符號 P 解釋為對某些特定集合中的數字為真時，這個公式在結構 (N; 0, S, <, +, ×) 中為真——無論該集合是什麼——它說明，如果該集合是非空的，則該集合有一個最小成員。透過現在新增量詞 ∀P
∀P[∃x Px → ∃x(Px & ∀y(Py → (y = x v x < y)))]
我們得到了良序性質的形式化。
二階邏輯的語言透過允許對謂詞符號和函式符號進行量化來擴充套件了一階邏輯的語言。如以上示例所示，在用於算術的二階語言中，我們可以說自然數是有序的。我們知道良序性質無法用任何一階句子表達，因為 (N; 0, S, <, +, ×) 的非標準模型永遠不會是有序的。因此，使用二階邏輯是一種真正的擴充套件。也就是說，我們可以將一些自然語言句子，例如“關係 < 是一個良序”，翻譯成二階邏輯語言，這些句子無法翻譯成一階邏輯語言。
再舉一個例子，我們可以（使用選擇）說論域是無限的，方法是說論域上存在一個傳遞關係，使得每個元素都與某些事物具有這種關係，但與自身沒有這種關係
∃R[∀x ∀y ∀z(Rxy & Ryz → Rxz) & ∀x[¬Rxx & ∃y Rxy]
這裡，二階量詞“∃R”表達了論域上某個二元關係的存在。因為唯一的謂詞符號 R 在這個量詞的作用域內，所以這個句子沒有開放解釋的謂詞符號。眾所周知，沒有一階句子可以將其模型恰好設定為無限結構。
更詳細地說，以下是二階語言的含義：從一個一階語言開始，並透過對每個正整數 n 無限供應 n 元謂詞變數，以及對每個正整數 n 無限供應 n 元函式變數來增強它。（函式變數可以避免，但那是另一回事。）形成良構公式的規則是顯而易見的；特別是，對於任何變數，無論是單個變數、謂詞變數還是函式變數，都允許進行全稱量化和存在量化。
回到自然數的例子，我們可以用二階句子表達 Peano 歸納公理
∀X[X0 & ∀y(Xy → XSy) → ∀y Xy]
這個句子表達了 X 如果對 0 為真，並且它的真值在某個數字 y 處保證了它在 y 的後繼處的真值，那麼 X 對所有自然數都為真的想法，無論 X 可能對哪個數字集為真。
對於涉及帶有其通常排序的實數集 R 的示例，我們可以用二階句子表達最小上界性質
∀X[∃y∀z(Xz → z ≤ y) & ∃z Xz → ∃y∀y′(∀z(Xz → z ≤ y′) ↔ y ≤ y′)]
以上例子來自數學情境。還有一種有趣的可能性，即自然語言句子似乎需要二階公式才能將其形式化。喬治·布洛斯建議了這樣一個例子，“有些批評家只互相欣賞”。這個句子斷言存在一個具有特定屬性的個人集；它並不意味著，例如，存在兩個互相欣賞並且不欣賞其他人的批評家。
上一節中隱含了二階句子在結構中的真值的概念。考慮一個結構 M = (A, R, ...) ，它由一個非空集合 A 作為論域，以及解釋非邏輯符號的 A 上的一些關係和函式組成。那麼我們希望將形式為 ∀P φ（其中 P 是一個 k 元謂詞變數）的二階句子在該結構中視為真，如果對於 A 中 k 元組的每個集合 Q，我們都有當 P 被分配了關係 Q 時，φ 在該結構中為真。
更正式地說，我們需要歸納地定義二階公式 φ 在結構 M = (A, R, ...) 中在對 φ 中自由變數的分配 s 下被滿足的含義，這將寫成 M ⊨ φ[s]。該定義與一階情況完全一樣，除了針對二階量詞的附加子句。對於一個 k 元謂詞變數 P，
M ⊨ ∀P φ[s] 當且僅當對於 A 上的每個 k 元關係 Q，我們有 M ⊨ φ[s′]
其中 s′ 僅在將關係 Q 分配給謂詞變數 P 方面與 s 不同。（這裡“當且僅當”縮寫為“當且僅當”。）類似地，對於一個 k 元函式變數 F，
M ⊨ ∀F φ[s] 當且僅當對於 A 上的每個 k 元函式 G，我們有 M ⊨ φ[s′]
其中 s′ 僅在將函式 G 分配給函式變數 F 方面與 s 不同。觀察到，在 1 元謂詞變數的情況下，該定義指的是 A 的所有子集，即 A 的整個冪集。正是這個特點導致了二階語言非凡的語義強度。
對於二階句子 σ（即沒有自由變數的公式），賦值 s 就變得無關緊要了，我們可以明確地談論 σ 在結構 M 中的真值或假值（也就是說，我們可以說 M 是或不是 σ 的模型）。特別是，第 1 節中從自然語言到二階邏輯語言的翻譯示例現在可以被視為實現了它們預期的目的。線性序公理和句子
∃x Px → ∃x(Px & ∀y(Py → (y = x v x < y))) 在結構 (A, <) 中為真，當且僅當關係 < 良序集 A。句子
∃R[∀x ∀y ∀z(Rxy & Ryz → Rxz) & ∀x[¬Rxx & ∃y Rxy]
在一個結構中為真，當且僅當論域是一個無限集。這個例子表明緊緻性定理不適用於二階邏輯。如果我們把上面的句子稱為 λ∞，並且我們讓 λn 是“宇宙中至少有 n 個不同的東西”的一階句子，那麼集合
{¬λ∞, λ2, λ3, λ4, … }
沒有模型，儘管每個有限子集都有一個模型。
皮亞諾公理的合取
∀x(¬0 = Sx) 和 ∀x∀y(Sx = Sy → x = y)
以及皮亞諾歸納公理
∀X[X0 & ∀y(Xy → XSy) → ∀y Xy]
在一個結構 (A, f, e) 中為真，當且僅當該結構同構於 (N, S, 0)，即帶有後繼運算 S 和區別元素 0 的自然數。這三個句子的合取提供了一個範例，即一個範疇性的句子，也就是說，它只有一個模型，直到同構。相比之下，一個一階句子只有在它的模型是有限的情況下才能是範疇性的。
類似地，實數的有序域，(R, 0, 1, +, ×, <)，可以根據有序域的一階公理以及表達最小上界性質的二階句子，同構地進行刻畫。眾所周知，這些句子的任何模型都必須同構於實數的有序域。這個例子表明，Löwenheim-Skolem 定理不適用於二階邏輯。
前面的例子表明，兩個常見的數學結構，(N, S, 0) 和 (R, 0, 1, +, ×, <) 是二階可刻畫的。也就是說，每個結構都有一個唯一的二階公理，它是該公理的唯一模型，直到同構。人們可能會問，還有哪些其他的結構是二階可刻畫的。當然，直到同構，這樣的結構最多隻有可數個，因為每個結構都需要一個句子。
接下來，假設在這些例子中，我們對所有非邏輯符號（即所有謂詞符號和函式符號）進行存在量化。其中 π(0, S,) 是三個皮亞諾公理的合取，句子 ∃x ∃F π(x, F) 是等式二階語言中的一個句子，也就是說，它根本沒有非邏輯符號。
等式語言的結構僅僅由一個非空的論域組成；沒有關係、函式或區別元素。這樣的結構當然由它的基數決定，直到同構。對於等式語言中的句子 σ，令它的譜是它為真的基數類。例如，一個有效句子的譜是所有非零基數的類。一個不可滿足句子的譜是空的。¬σ 的譜是 σ 的譜的補集（相對於所有非零基數的類）。句子的合取和析取產生譜的交集和並集。等式語言中的一個句子由它的譜決定，直到邏輯等價。
我們從皮亞諾公理得到的句子 ∃x ∃F π(x, F) 在可數無限基數中為真，而在其他任何基數中都不為真。因此它的譜是一個單例。說一個基數 κ 是二階可刻畫的，如果存在一個等式二階語言的句子，它在基數 κ 中為真，而只在 κ 中為真。（非零有限基數都是一階可刻畫的。）我們已經看到，可數無限基數是二階可刻畫的。類似地，我們可以證明，連續統的勢是二階可刻畫的。其中 ρ(0, 1, +, ×, <) 是刻畫實數的有序域直到同構的二階句子，句子
∃x ∃y ∃F ∃G ∃R ρ(x, y, F, G, R)
是等式二階語言中的一個句子，它在連續統的勢中為真，而在其他任何基數中都不為真。
人們可能會問，還有哪些其他的基數是二階可刻畫的。見 S. Garland 1974 年的論文，對這個問題進行了探討。當然，這樣的基數最多隻有可數個，因為每個基數都需要一個句子。
不難看出，最小不可數基數是二階可刻畫的。我們可以使用一個句子，它說宇宙是無限的，但不可數，並且任何不可數子集都與整個宇宙等勢。因此，我們在等式二階語言中得到了句子 κ 和 λ，它們分別刻畫了最小不可數基數和連續統的勢。如果連續統假設為真，則句子 κ ↔ λ 是一個有效句子，否則不是。我們可以得出結論，並非所有涉及二階邏輯的問題都一定可以在 ZFC 中解決。
廣為研究的理論 PA，即一階皮亞諾算術，當然是由使用以下內容得到的：代替二階歸納公理 ∀X[X0 & ∀y(Xy → XSy) → ∀y Xy]，使用相應的第一個序模式
φ(0) & ∀y(φ(y → φ(Sy)) → ∀y φ(y)
其中 φ 可以是任何合適的一階公式。該模式的效果是眾所周知的；它確保任何包含 0 且在後繼運算下封閉的可定義集合都必須包含所有東西。
假設，類似地，我們從實數的有序域的二階公理化開始，並將二階最小上界公理替換為相應的模式。結果是一個無限的一階公理集，它確保任何非空且有界的可定義集合都有最小上界。這些公理的模型被稱為實閉有序域。有趣的是，這個概念最初是由代數學家而不是邏輯學家提出的。
衡量二階邏輯強度的指標之一是其有效句子集的複雜性。令 V¹ 為一階邏輯的有效句子集，令 V² 為二階邏輯的有效句子集。更具體地說，在一階邏輯中，只有一個 2 位謂詞符號 P，我們知道有效句子集 V¹(P) 是一個完全可計算列舉集（即一個完全遞迴可列舉集）。（這裡我們可以分配哥德爾數並將 V¹(P) 視為自然數集，或者等價地，我們可以直接將其視為有限字母上的詞集。）Tarski 指出，等式一階語言（沒有任何非邏輯符號）的有效句子集 V¹(=) 是可判定的。
為了比較，令 V²(=) 為等式二階語言的有效句子集。這個集合的複雜性如何？
令 π 為皮亞諾公理和加法和乘法遞迴方程的合取。因此 π 是算術語言中的一個二階句子，帶有 0、S、+ 和 ×。句子 π 是範疇性的；它唯一的模型是 (N, 0, S, +, ×)，直到同構。因此，對於算術語言中的句子 σ，σ 在算術中為真，當且僅當條件 (π → σ) 為有效。這表明 V²(0, S, +, ×) 不能是算術的（即，不能在一階算術中可定義），否則算術中的真值將是可定義的，違反了 Tarski 定理。現在我們可以對所有非邏輯符號進行量化；一個句子 φ(P) 為有效，當且僅當句子 ∀P φ(P) 為有效。結論是 V²(=) 不是算術的。
這很有趣，但這僅僅是冰山一角。首先，我們可以證明 V²(=) 不是分析的，即不能在算術中用二階公式定義。Tarski 定理的證明，即證明算術的真的一階句子集不是在一階算術中可定義的，也證明了算術的真二階句子集不是在二階算術中可定義的。其餘的論證保持不變。稍後我們會看到，事實證明比這還要複雜。
在完全不同的方向上，R. Fagin 已經證明了計算複雜性主題和有限結構上的二階可定義性之間令人驚訝的聯絡。例如，一個有限圖可以被視為一個對 (V, E)，它由一個非空的頂點集 V 和 V 上的對稱邊關係 E 組成。圖可以用三種顏色正確著色的語句可以用二階句子表示：存在子集 R、G、B，它們以這樣一種方式對 V 進行劃分，即由邊連線的兩個頂點永遠不會是相同的顏色。這個句子是 Σ-1-1，也就是說，它具有以下形式
[存在二階量詞] [一階公式].
眾所周知，三著色是一個圖的 NP 性質。也就是說，它是一個由非確定性圖靈機在多項式時間內可識別的性質。（存在一個非確定性圖靈機 M 和一個多項式 p，使得當 (V, E)（以適當的方式編碼）被給予 M 時，如果 (V, E) 是三著色的，那麼 M 的某些計算將在 p(n) 步內接受圖，其中 n 度量 (V, E) 的大小，而如果 (V, E) 不是三著色的，那麼 M 的任何計算都不會接受圖。）
Fagin 證明，這不是一個孤立的例子；有限圖的每個 NP 性質都可以用二階邏輯的 Σ-1-1 句子定義。反之，任何 Σ-1-1 句子定義一個 NP 性質。並且，代替圖，我們可以使用有向圖或其他有限結構。Fagin 定理指出，有限結構的一個性質是 NP 性質，當且僅當它可以用 Σ-1-1 二階句子定義。
3. 一般語義
[edit | edit source]上一節討論的“標準語義”的一個關鍵特徵是，對於一個一位謂詞變數 X，量詞 ∀X 遍及論域的整個冪集。我們已經看到，這個特徵賦予了二階語言很高的表達能力。
但是，我們真的希望量詞 ∀X 遍及實際的冪集嗎？謂詞主義者會反對說，冪集運算沒有意義。即使是古典數學家也會承認，冪集運算有一些模糊的特徵。連續統假設的獨立性說明了這樣一種模糊性。如果我們的目標是研究數學基礎，那麼最好不要認為我們已經完全瞭解了冪集。
二階邏輯的一般語義的概念避免了任何關於冪集運算是一個固定且易於理解的資源的假定。相反，量詞 ∀X 的範圍必須直接指定。
對於一個二階語言，一般預結構是指一個通常意義上的結構（一個論域加上對非邏輯符號的解釋），以及額外的集合
* The n-place relation universe for each positive integer n. This must be a collection of n-ary relations on the universe of discourse. In particular, the 1-place relation universe must be some collection of subsets of the universe. Thus it is part (perhaps all, perhaps not) of the power set of the universe. * The n-place function universe for each positive integer n. This must be a collection of n-place functions on the universe of discourse.
對於一個一般預結構 M，有一個自然的方法來定義一個二階公式 φ 在結構 M 中在對 φ 中的自由變數進行賦值 s 時被滿足的含義，這仍然將被寫成 M ⊨ φ[s]。二階量詞現在被定義為遍及相應的宇宙。對於一個 k 位謂詞變數 P，
如果對於 k 元關係宇宙中的每個 k 元關係 Q，都有 M ⊨ φ[s′]，其中 s′ 與 s 僅在將關係 Q 分配給謂詞變數 P 時有所不同，則 M ⊨ ∀P φ[s]。類似地，對於 k 元函式變數 F，
如果對於 k 元函式宇宙中的每個 k 元函式 G，都有 M ⊨ φ[s′]，其中 s′ 與 s 僅在將函式 G 分配給函式變數 F 時有所不同，則 M ⊨ ∀F φ[s]。在二階句子 σ（即沒有自由變數的公式）的情況下，賦值 s 不再相關，我們可以明確地談論 σ 在一般預結構 M 中的真或假（也就是說，我們可以說 M 是或不是 σ 的模型）。
但是對於二階邏輯，我們並不真正希望一元關係宇宙成為宇宙子集的任意集合。我們可能不知道關於冪集運算的一切，但我們知道一些關於它的東西。實際上，使用一般預結構相當於將二階語言視為一個多排序的一階語言。
我們知道宇宙中的一些子集，因為我們可以定義它們。也就是說，假設 φ 是一個公式，其中只有變數 u 出現自由。那麼 φ 在 M 中定義的集合是由所有 M 的成員 a 組成的集合，使得當 a 分配給 u 時，φ 在 M 中得到滿足。這個想法可以擴充套件。假設 φ 只有自由變數 u、v、w、x、Y 和 Z（其中 Y 是 m 元謂詞變數，而 Z 是 n 元函式變數）。假設 c 和 d 是 M 的（個體）宇宙 |M| 的成員，E 在 M 的 m 元關係宇宙中，而 F 在 M 的 n 元函式宇宙中。那麼 φ 從引數 c、d、E 和 F 在 M 中定義的二元關係是 |M| 中元素對 <a, b> 的集合，使得當其變數 u、v、w、x、Y 和 Z 分別分配 a、b、c、d、E 和 F 時，φ 在 M 中得到滿足。也就是說，它是二元關係
{<a, b> | M ⊨ φ(u, v, w, x, Y, Z) [a, b, c, d, E, F]}
顯然，這個概念可以推廣到從任意數量的引數定義 k 元關係的情況。
那麼，將注意力限制在閉合於可定義性的一般預結構上是合理的。因此，在剛才描述的情況下，預期 M 的 2 元關係宇宙包含 φ 從預結構中的引數定義的二元關係。也就是說，我們期望句子
∀w ∀x ∀Y ∀Z ∃R ∀u ∀v [Ruv ↔ φ(u, v, w, x, Y, Z)]
在 M 中為真。稱這種句子為理解公理。
二階語言的一般結構（也稱為 Henkin 結構）是指所有理解公理（對於所有公式）都為真的一個一般預結構。（這裡 φ 可能包含對謂詞變數的量化，因此即使是非謂詞理解公理也應該為真。在第 5 節中，我們考慮“完全理解”的替代方案。）在一般結構中，那些一元關係宇宙是單個宇宙的實際冪集，依此類推。（稱這種一般結構為絕對的。）但可能還有其他的。
我們透過考慮所有一般結構來獲得二階語言的一般語義（也稱為 Henkin 語義）。也就是說，對於一個句子 σ 來說，它在一般語義中有效，它必須在所有一般結構中為真。這比說 σ 在標準語義中有效的要求更強。一個在標準語義中有效的句子在那些一元關係宇宙是單個宇宙的完整冪集等等的一般結構中為真。但這樣的句子 σ 可能在某些一般結構中為假（也就是說，¬σ 可能有一個一般模型）。
一般語義的主要特點是“僅僅是”型別的結果：具有一般語義的二階邏輯僅僅是一階邏輯（多排序）加上理解公理。因此，一個句子在一般語義中有效當且僅當它被理解公理集在（一階邏輯中）邏輯蘊涵。
這種對一階邏輯的約簡立即產生了以下結果
* (Enumerability) In a second-order language with finitely many non-logical symbols, the set of sentences that are valid in the general semantics is computably enumerable. This holds because the set of comprehension axioms is a computable set (i.e., a recursive set). * (Compactness) A set of sentences has a general model if every finite subset has a general model. * (Löwenheim–Skolem) If a set of sentences has a general model, then it has a countable general model.
在這三種情況下，都與第 2 節中討論的標準語義情況形成鮮明對比。此外，可以為二階邏輯給出一種演繹演算（從一階邏輯改編而來，並透過理解公理進行增強），該演算對於一般語義將是完備的。
為了比較，公理化集合論（例如 ZFC）是一個一階理論；集合論的模型必須提供一個冪集運算。但集合論的語言具有一定的高階方面，因為它允許我們談論集合、集合的集合，等等。
在所有關係都是可定義的結構 M 的極端情況下（例如，具有一個點宇宙的結構），一般語義將與標準語義一致。
4. 高階邏輯
[edit | edit source]無需止步於二階邏輯；可以繼續下去。我們可以向語言新增“超謂詞”符號，它們以單個符號（變數或常量）和謂詞符號作為引數。然後我們可以允許對超謂詞符號進行量化。然後我們可以繼續更進一步。
（讀者要注意，文獻中有兩種不同的階數計數方式。根據一種方案，三階邏輯允許超謂詞符號自由出現，而四階邏輯允許它們被量化。根據另一種方案，三階邏輯已經允許對超謂詞符號進行量化。）
我們在 ω 步之後達到型別論的級別。並且可以想象繼續進入超限。
我們已經看到，雖然一階邏輯有效公式集 V¹ 是可計算列舉的，但二階邏輯（具有標準語義）的相應集合 V² 則要複雜得多。這種現象不會繼續到更高階。
冪集運算在某種意義上可以在二階邏輯中定義。考慮一個帶有單一謂詞符號 I（表示個體）、單一謂詞符號 S（表示集合）和二元謂詞符號 E（表示成員關係）的語言。那麼，要表達 S 是 I 的冪集的想法，我們可以使用以下四個句子的合取（稱之為 σ）： ∀x(Ix + Sx) 其中“+”表示異或 ∀x ∀y (Exy → Ix & Sy) ∀x ∀y (Sx & Sy & ∀t(Etx ↔ Ety) → x = y) (外延性) ∀X ∃y(Sy & ∀t(It → (Ety ↔ Xt))) (理解)。
顯然，σ 在任何結構中都為真，該結構的宇宙是一個集合 A 及其冪集 P(A) 的不相交併集，並且將 A 分配給 I，將 P(A) 分配給 S，並將成員關係 ∈ 分配給 E。相反地，令 M 為 σ 的任意模型（在標準語義中）。令 f 為從 M 的 I 解釋到一個與它的冪集不相交的集合 A 的一對一函式（總是有這樣的集合）。透過為 M 的 S 解釋中的每個 s 定義以下內容，將 f 擴充套件到 M 的整個宇宙：
f(s) = {f(i) | M ⊨ E [i, s]}
（也就是說，f(s) 是 M 認為屬於 s 的 A 中的元素集合）。那麼 f 是從 M 到一個結構的同構，該結構的宇宙是一個集合 A 及其冪集 P(A) 的不相交併集，並且將 A 分配給 I，將 P(A) 分配給 S，並將成員關係 ∈ 分配給 E。所以粗略地說，σ 定義了“在同構意義上”的冪集運算。
類似地，我們可以“在同構意義上”定義 I × I 的冪集，即 I 上的二元關係集。依此類推。
冪集運算在二階邏輯中的這種可表達性允許在二階邏輯中模擬高階邏輯。更具體地說，我們有 Hintikka (1955) 的以下結果：對於高階邏輯中的每個公式 φ（在一個帶有有限多個非邏輯符號的語言中），我們可以有效地找到一個二階邏輯中的句子 ψ（在等式語言中），使得 φ 有效當且僅當 ψ 有效。句子 ψ 透過首先擴充套件語言來構造，方法是新增符號來表示各種型別的宇宙（個體、個體集，……）以及這些宇宙中的成員關係。然後，φ 的有效性等價於二階公式的有效性
宇宙排列正確 → φ*
其中 φ* 是 φ 的一個合適的相對化。最後，我們可以加上全稱量詞來獲得等式語言中的句子 ψ。
因此，十七階邏輯的有效性集可計算地約簡為 V²(=)，即等式語言中二階有效性集。（實際上，這兩個集合是可計算同構的。）所以在這個方面，高階邏輯的複雜性不會隨著階數的增加而增加。由此得出，集合 V²(=) 具有高度複雜性。我們可以擴充套件我們之前的觀察結果，它在二階算術中不可定義；它在更高階的算術中也不可定義。Montague 在 1965 年將此擴充套件到超限。當時，他被聽到說集合 V²(=) 不在任何 Kleene 層次結構中，“過去、現在或將來”。
我們可以用二階邏輯表達冪集運算（並且可以迭代該過程）這一事實使二階邏輯獲得了集合論表達能力的很大一部分。Quine 聲稱二階邏輯不是真正的邏輯，而是偽裝的集合論。Robert Vaught 評論說，研究二階邏輯就像研究“集合論的標準模型”。
如果我們對句子的量詞形式施加限制，V²(=) 的複雜性不會發生太大變化。前面對高階邏輯的約簡產生了 Π-1-2 句子，因此我們可以得出結論，等式語言中有效的 Π-1-2 句子集是可計算地同構於完整的 V²(=)。這大約是最好的結果。有效的 Π-1-1 句子集是一個完全可計算列舉集；一旦我們去掉全稱二階量詞，我們就開始看一階公式。等式語言中有效的 Σ-1-1 句子集是一個完全 co-c.e. 集，即一個可計算列舉集的補集。（句子 ∃Pφ(P) 在每個非零基數中都為真當且僅當基本句子 φ(P) 具有每個有限大小的模型，這是一個 co-c.e. 性質。並且對於圖靈機，我們可以有效地分配一個具有每個有限大小的模型的基本句子當且僅當該機器永遠不會停止。）等式語言中有效的 Σ-1-2 句子集也是可計算地同構於完整的 V²(=)，但這一事實需要一種不同的證明。
5. 二階數論系統
[edit | edit source]算術語言（包含 0、S、<、+ 和 ×）對於數學基礎非常重要。我們可以將通常的 Peano 公理作為公理，包括二階歸納公理。在標準語義中，Peano 公理的唯一模型（同構除外）是通常的算術模型。因此，這些公理生成的理論（在標準語義中）僅僅是真算術的二階理論。
但是，假設我們考慮一般語義。Peano 公理有一般模型，這些模型可能在以下兩種方式（或兩種方式都）中與通常的模型不同。我們可以利用緊緻性定理構建 Peano 公理的非標準一般模型，其中包含無限大的數字。我們還可以找到 Peano 公理的一般模型，其中集合的宇宙小於個體宇宙的完全冪集（即，不是絕對的一般模型）。實際上，任何可數的一般模型都必須是這種型別。
在一般模型的背景下，我們為選擇添加了額外的公理模式
∀n ∃X φ(n,X) → ∃Y ∀n φ(n, {t | Ynt})
在需要時加上全稱量詞。（這裡，寫成 φ(n, {t | Ytn}) 的公式是從 φ(n,X) 獲得的，透過將每個項 Xu 替換為項 Ynu。）
Peano 公理足夠強大，可以為我們提供配對函式。因此，對於一個一般模型，其 1 元關係宇宙完全決定了它對於每個 k 的 k 元關係宇宙。
傳統術語是將二階數論稱為分析。這個名稱來源於這樣一個事實，即可以將實數識別為自然數的集合。然後，關於自然數集的二階量詞可以被視為關於實數的量詞。這個名稱的適當性尚待商榷，但其用法已得到充分確立。因此，對於分析模型，我們將指的是具有選擇的 Peano 公理的一般模型。作為一個一般模型，任何分析模型當然必須滿足所有理解公理；稍後我們將考慮削弱這一要求。
令 A2 為 Peano 公理與選擇生成的理論（在一般語義中）。那麼 A2 是真二階算術的一個完整的可計算列舉子集。A2 包含所有真 Σ-0-1 語句。它不包含所有真 Π-0-1 語句。
我們可以透過限制對那些僅在之前描述的兩種方式中的第二種方式與通常模型不同的分析模型的關注來獲得更強的理論。也就是說，定義一個分析的 ω-模型是一個分析模型，其中個體宇宙是實際的自然數集，符號 0 和 S 具有其通常的解釋。（因此，符號 <、+ 和 × 具有其通常的解釋。）分析的 ω-模型的集合宇宙因此必須是自然數冪集的一部分（可能全部），但它必須滿足完全理解。
考慮 ω-模型的動機可以表述如下。我們對自然數集有一個清晰的理解——或者我們喜歡這樣認為。但我們對自然數集的冪集並沒有類似的理解。因此，將我們確信的部分固定住，但對我們不那麼確信的部分保持開放解釋是合理的。
一個分析的 ω-模型完全由其集合宇宙決定。因為我們有可在一階定義的配對函式，所以集合宇宙將決定二元關係宇宙，等等。Löwenheim-Skolem 論證將表明，存在具有可數集合宇宙的分析 ω-模型。
在任何分析的 ω-模型中，真一階語句恰好是那些在通常模型中為真的語句。但是 ω-模型在二階語句上可能不同。令 Aω 為 ω-模型的理論，即在所有分析的 ω-模型中為真的語句集。那麼 Aω 擴充套件了 A2。它是一個完整的 Π-1-1 集。它包含所有真 Π-1-1 語句；它不包含所有真 Σ-1-1 語句。
對於 ω-規則，我們指的是從前提 φ(0)、φ(1)、φ(2)、… 推斷 ∀x φ(x) 的無窮推理規則。假設我們將此規則新增到通常的邏輯裝置中，並觀察從 Peano 公理和選擇中可以推斷出什麼。使用 ω-規則的“推斷”通常是無窮的，但它必須是良基的。不難看出，以這種方式可推斷的任何語句都在 Aω 中。反之，一個完備性定理成立：Aω 中的每個語句都有一個上述型別的推斷。
在 1961 年的一篇論文中，Andrzej Mostowski 描述了一種方法，可以進一步邁進一步，走向更強的理論。假設我們願意考慮不只是順序型別 ω 已經被充分理解，甚至考慮成為良序的概念。定義分析的 β-模型是一個 ω-模型，它具有以下附加屬性：模型中看起來像是良序的序關係實際上是良序的。也就是說，分析的 ω-模型 M 是一個 β-模型，如果 M 中的每個序關係（在自然數上）都具有以下屬性：M 中的非空集總是有最小成員，那麼它實際上是一個良序。
然後，在所有 β-模型中為真的語句集 Aβ 被證明是一個完整的 Π-1-2 集。它包含所有真 Π-1-2 語句；它不包含所有真 Σ-1-2 語句。顯然，我們有包含關係
A2 ⊆ Aω ⊆ Aβ ⊆ 真二階算術。
例如，ZF 集合論的傳遞 ∈-模型的數論部分將始終是分析的 β-模型。但是，我們可以構建一個 β-模型，而無需強假設。事實上，存在一個最小的 β-模型，並且它可以用一種類似於 Gödel 定義可構造集類 L 的方式來構建。
最後，應該提到，在某些情況下，具有非完全理解的二階算術理論是合適的。例如，人們可以取由 Peano 公理以及僅針對一階公式的理解公理給出的理論 ACA。這些理論已被證明可用於研究“逆向數學”。參考文獻
* Boolos, George, 1975. “On Second-Order Logic,” The Journal of Philosophy, 72: 509–527. Also in Logic, Logic, and Logic, by George Boolos, Cambridge, MA: Harvard University Press, 1998, pp. 37–53. * Church, Alonzo, 1956. Introduction to Mathematical Logic, Volume 1. Princeton: Princeton University Press. * Church, Alonzo, 1972. “Axioms for Functional Calculi of Higher Order,” in Logic and Art: Essays in Honor of Nelson Goodman, Richard S. Rudner and Israel Scheffler (eds.), Indianapolis and New York: Bobbs-Merrill Company, pp. 197–213. * Enderton, Herbert B., 2001. A Mathematical Introduction to Logic, second edition. San Diego: Academic Press. * Fagin, Ronald, 1974. “Generalized First-Order Spectra and Polynomial-Time Recognizable Sets,” in Complexity of Computation, Richard M. Karp (ed.), SIAM-AMS Proceedings, vol. 7, Providence: American Mathematical Society, pp. 43–73. * Garland Stephen J., 1974. “Second-Order Cardinal Characterizability,” in Axiomatic Set Theory, Thomas J. Jech (ed.), Proceedings of Symposia in Pure Mathematics, vol. 13, part 2, Providence: American Mathematical Society, pp. 127–146. * Grzegorczyk, Andrzej, A. Mostowski, and C. Ryll-Nardzewski, 1958. “The Classical and the ω-Complete Arithmetic,” The Journal of Symbolic Logic, 23: 188–205. * Henkin, Leon, 1950. “Completeness in the Theory of Types,” The Journal of Symbolic Logic, 15: 81–91. * Hintikka, K. Jaakko, 1955. “Reductions in the Theory of Types,” in Two Papers on Symbolic Logic, Acta Philosophica Fennica, No. 8, Helsinki, pp. 57–115. * Montague, Richard, 1965. “Reductions of Higher-Order Logic,” in The Theory of Models, J. W. Addison, Leon Henkin, and Alfred Tarski (eds.), Amsterdam: North-Holland Publishing Co., pp. 251–264. * Mostowski, Andrzej, 1961. “Formal System of Analysis Based on an Infinitistic Rule of Proof,” in Infinitistic Methods, Warsaw: Państwowe Wydawnictwo Naukowe, and Oxford, London, New York, and Paris: Pergamon Press, pp. 141–166. * Orey, Steven, 1956. “On ω-Consistency and Related Properties,” The Journal of Symbolic Logic, 21: 246–252. * Shapiro, Stewart, 1991. Foundations without Foundationalism: A Case for Second-Order Logic. Oxford: Oxford University Press. * Simpson, Stephen, 1999. Subsystems of Second Order Arithmetic. Berlin: Springer. * Väänänen, Jouko, 2001. “Second-Order Logic and Foundations of Mathematics,” The Bulletin of Symbolic Logic, 7: 504–520.
* Second Order Logic, at the Arché wiki, University of St. Andrews.
[請聯絡作者提供其他建議。]
可計算性和複雜性 | 多元量詞 | 型別論