人工智能/逻辑/表示/二阶逻辑
首次发布于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.
[请联系作者提供其他建议。]
可计算性和复杂性 | 多元量词 | 类型论