二阶逻辑与高阶逻辑 second-order and higher-order (Jouko Väänänen)

首次发表于 2019 年 8 月 1 日

二阶逻辑在数学哲学中扮演着微妙的角色。它比一阶逻辑更强大，因为它将“对于所有属性”纳入语法中，而一阶逻辑只能说“对于所有元素”。同时，它可以说是比集合论更弱的，因为它的量词一次只能涵盖一个有限的域，而集合论则采用普遍主义的方法，其量词涵盖所有可能的域。这种比一阶逻辑更强大/比集合论更弱的二元性是一个活跃的辩论源泉，尤其因为集合论通常被认为是基于一阶逻辑的。二阶逻辑如何同时更强大和更弱？为了充分利用二阶逻辑的强度，并确切解释“对于所有属性”，人们早期提出了一个建议，即必须假设一个一阶集合论背景，以便充分利用二阶逻辑的强度和“对于所有属性”的确切解释。这似乎削弱了二阶逻辑的声称强度，以及其作为数学的主要基础的角色。它似乎还将二阶逻辑与二阶逻辑可能希望绕过的集合论方面联系起来：更高的无穷，独立结果以及找到新的令人信服的公理的困难。撇开哲学问题不谈，毫无疑问，并通过一系列有趣的结果得到证明，二阶逻辑是逻辑学家工具箱的重要组成部分。

1. 引言

二阶逻辑 [1] 是由弗雷格在他的《概念符号》（1879）中引入的，他还在（1884: §53）中创造了“二阶”（“zweiter Ordnung”）这个术语。它在逻辑学中广泛使用，直到 20 世纪 30 年代，当集合论开始成为数学基础时。很难准确地说为什么会发生这种情况，但与二阶和高阶逻辑（包括类型理论）相比，集合论在基于一个二元谓词 x∈y 的简单性方面具有优势。哲学家们对二阶逻辑的优点，特别是与集合论的比较，至今仍在讨论中（Shapiro 1991）。与此同时，二阶逻辑已成为计算机科学逻辑学的标准工具，尤其是有限模型理论。理论计算机科学的核心问题，如 P = NP?问题，可以看作是有限环境中关于二阶逻辑的问题。

最终，二阶逻辑只是另一种形式语言。通过在我们选择的数论作为数学元理论中进行工作，可以给予它标准处理，使得语法、语义和证明理论变得精确。虽然可以使用二阶逻辑本身作为元理论，但这会更加复杂，因为二阶逻辑比集合论发展得更少。

在初等数学中，一阶逻辑和二阶逻辑之间的区别最容易理解。让我们考虑数论。我们研究的对象是自然数 0、1、2...及其算术。使用一阶逻辑，我们可以通过使用原子表达式 x=y、x+y=z 和 x×y=z 结合命题运算 ∧、¬、∨、→以及量词 ∀x 和 ∃x 来阐述关于数论的陈述。这里的变量 x、y、z...被认为是自然数的范围。使用二阶逻辑，我们可以表达更多：我们有变量 x、y、z...，就像一阶逻辑中的数字一样。此外，我们还有变量 X、Y、Z...用于数字的属性和数字之间的关系，以及量词 ∀X 和 ∃X 用于这些变量。我们有一阶逻辑的原子表达式，还有形式为 X(y1,...,yn)的新的原子表达式。

一个有趣且广泛研究的问题出现了：自然数的哪些属性可以用一阶逻辑表达，哪些可以用二阶逻辑表达？如果在两种情况下都给出了合适的证明系统，那么这个问题同样有趣，即使将“表达”替换为“证明”。我们可以将自然数替换为其他数学背景，例如实数、复数等等。

只需使用常数 0 和一元函数 n↦n+（其中 n+表示 n+1），我们可以用二阶逻辑表达归纳公理

(1)∀X([X(0)∧∀y(X(y)→X(y+))]→∀yX(y)),

自然数。这与公理 ∀x¬(x+=0)和 ∀x∀y(x+=y+→x=y)一起，以同构的方式刻画了具有继承操作的自然数。在一阶逻辑中，任何具有可数无穷模型的理论也具有不可数模型（根据上升 Löwenheim Skolem 定理）。因此，(1)不能用一阶逻辑表达。另一个典型的二阶表达式是实数的线性顺序 ≤ 的完备性公理：

(2)∀X([∃yX(y)∧∃z∀y(X(y)→y≤z)]→∃z∀y(∃u(X(u)∧y≤u)∨z≤y)),

这个与有序域的公理一起，以同构的方式刻画了实数有序域。在一阶逻辑中，任何具有无穷模型的可数理论也有一个可数模型（通过下降的 Löwenheim-Skolem 定理）。因此，(2)不能用一阶逻辑来表达。

对于早期的逻辑学家来说，使用二阶逻辑与一阶逻辑并列似乎是很自然的，好像没有太大的区别。这包括了 Russell、Löwenheim、Hilbert 和 Zermelo。基本上只有 Skolem 强调了这种区别（关于一阶逻辑的出现，请参见 Moore 1988）。1929 年，Gödel 证明了他的完备性定理，第二年证明了他的不完备性定理。逐渐明显的是，二阶逻辑与一阶逻辑非常不同。第一个指标之一是不完备现象。Gödel 证明了任何有效的数论公理化都是不完备的。另一方面，在二阶逻辑中，有一个简单的有限范畴化（因此是完备的）的结构（N，+，×）的公理化（参见与（1）相关的讨论）。这表明，对于二阶逻辑来说，就像对于一阶逻辑一样，不可能有这样一个完备的公理化。在一阶逻辑的情况下被称为 Gödel 的完备性定理的东西在二阶逻辑中根本不成立。

当 Henkin 证明了关于所谓的一般模型的二阶逻辑的完备性定理时，情况有所改变（§9）。现在可以像一阶逻辑一样使用二阶逻辑，只要记住语义是基于一般模型的。二阶逻辑表征数学结构的能力不适用于一般模型（除了内部范畴性的形式—见 §10）。任何具有无限一般模型的二阶理论都有所有无限基数的一般模型，因此在一般模型的背景下不能是范畴性的。我们将在 §9 中讨论一般模型和相关的 Henkin 模型。

2. 二阶逻辑的句法

二阶逻辑中的词汇与一阶逻辑中的词汇一样，即一组关系、函数和常量符号的集合。每个关系和函数符号都有一个正的自然数作为它的元数。

二阶逻辑有几种变量。它有用小写字母 x，y，z，...表示的个体变量，可能带有下标。它有用大写字母 X，Y，Z，...表示的属性和关系变量，可能带有下标。最后，它有用大写字母 F，G，H，...表示的函数变量，可能带有下标。有时函数变量被省略，因为毕竟函数是特殊类型的关系。每个关系和函数变量都有一个阶数，它是一个正的自然数。

值得注意的是，尽管我们有属性变量，但我们没有用于属性的属性的变量。这样的变量将成为第三阶逻辑形式化的一部分，参见第 12 节。

二阶逻辑的术语按以下递归方式定义：常量符号和个体变量是术语。如果 t1，...，tn 是术语，U 是一个 n 元函数符号，F 是一个 n 元函数变量，则 U(t1，...，tn)和 F(t1，...，tn)是术语。请注意，术语表示个体，而不是关系或属性。因此，X 本身不是一个术语，但 x 是。

二阶逻辑的原子公式是从术语中定义的，如下所示：如果 t 和 t'是术语，则 t=t'是一个原子公式。如果 R 是一个 n 元关系符号，t1,...,tn 是术语，则 R(t1,...,tn)是一个原子公式。如果 X 是一个 n 元关系变量，则 X(t1,...,tn)也是一个原子公式。X(t1,...,tn)的直观含义是元素 t1,...,tn 在关系 X 中或由 X 所断言。我们不允许形式为 X=Y 的原子公式，尽管它们具有明显的含义。我们通过使用量词来实现相同的效果。

定义 1 二阶逻辑的公式定义如下：原子公式是公式。如果 ϕ 和 ψ 是公式，则 ¬ϕ，ϕ∧ψ，ϕ∨ψ，ϕ→ψ 和 ϕ↔ψ 是公式。如果 ϕ 是公式，x 是个体变量，X 是关系变量，F 是函数变量，则 ∃xϕ，∀xϕ，∃Xϕ，∀Xϕ，∃Fϕ 和 ∀Fϕ 是公式。

有趣的是，在二阶逻辑中，我们实际上可以将恒等式 t=t'定义为 ∀X(X(t)↔X(t'))，并通过蕴涵的性质证明熟知的恒等公理。

一个重要的特例是二阶逻辑，其中不允许使用函数变量，而要求关系变量是单调的（也称为一元的），即具有一元数目。

我们没有将 X=Y 视为一个原子公式（尽管我们可以这样做），但在引入量词后，我们可以使用

(3)∀x1…∀xn(X(x1,…,xn)↔Y(x1,…,xn))

作为 X=Y 的替代。将 X=Y 作为基本的原子公式的优点是，使用(3)会带来额外的量词。有时候，将公式中的量词数量最小化是有趣的。此外，(3)使得 X=Y 的身份具有外延性的风味，与可能不同的内涵解释形成对比。

在通常的方式中，定义了变量在公式中的自由和约束出现的概念。如果一个公式没有自由变量，则称其为句子。在公式中，一个术语对于一个变量的自由性的概念与一阶逻辑中的定义相同。

3. 二阶逻辑的语义学

为了定义二阶逻辑的语义，我们必须达成对我们的元语言的共识。这个事实与二阶逻辑无关，而是语义学的一般特征（Tarski 1933 [1956]）。二阶逻辑最常用的元语言是集合论。因此，我们给出了对二阶逻辑的集合论解释，将“属性”解释为集合。这是最常见的选择，突出了二阶逻辑的主要特征。我们不能用集合来解释所有的属性，例如自己与自己相同的属性。但是，如果个体变量的取值范围被视为一个集合，那么我们可以有意义地将该域中的个体属性解释为集合。如果我们想在一个太大而无法成为集合的域中解释二阶逻辑，我们可以使用集合论中的类的概念（有关类的更多信息，请参见集合论条目）。

我们在一阶逻辑中使用相同的 L-结构（或等价地，L-模型）的概念。也就是说，一个 L-结构 M 具有一个域 M，它是任意非空集合，对于 L 的任何常量符号 c，有一个解释 cM∈M，对于 L 的任何 n 元关系符号 R，有一个解释 RM⊆Mn，以及对于 L 的任何 n 元函数符号 H，有一个解释 HM:Mn→M。

约定：每当我们使用大写 Fraktur 字母（如 M、N 等）来命名一个结构时，我们使用相应的大写 Italic 字母（如 M、N 等）来命名该结构的域。

给定一个 L-结构 M，一个赋值是一个从变量到 M 的域的函数 s，满足以下条件：如果 x 是一个个体变量，则 s(x)∈M；如果 X 是一个关系变量，其元数为 n，则 s(X)⊆Mn；如果 F 是一个函数变量，其元数为 n，则 s(F):Mn→M。我们使用 s(P/X)来表示赋值，除了 X 处的值已经改变为 P 之外，其余与 s 相同。类似地，s(a/x)和 s(f/F)。

注意，0 元关系变量本质上是命题。在赋值下，它们的解释是真值（真、假）。0 元函数变量本质上是个体变量，因为赋值将 0 元函数符号映射到 M 的一个元素上。

在模型 M 下，术语 t 在解释 s 下的值 tM⟨s⟩ 的定义与一阶逻辑相同。

在 M 中定义了句子 ϕ 的真实性概念 M⊨ϕ，首先通过定义辅助概念 M⊨sϕ 来满足 M 中的句子 ϕ 的分配 s（有关 Tarski 真实性定义的详细信息，请参见条目）：

定义 2（Tarski 的真实性定义）二阶逻辑的真实性定义通过以下子句扩展了一阶逻辑的真实性定义：

  1. 当且仅当(tM1⟨s⟩,…,tMn⟨s⟩)∈s(X)，M⊨sX(t1,…,tn)。

  2. M⊨s∃Xϕ 当且仅当 M⊨s(P/X)ϕ 对于某些 P⊆Mn 成立。

  3. M⊨s∃Fϕ 当且仅当 M⊨s(f/F)ϕ 对于某些 f:Mn→M 成立。

并且对于全称量词也是类似的。对于一个句子 ϕ，我们定义 M⊨ϕ 意味着对于所有（或者某些）s，M⊨sϕ 成立，然后说 ϕ 在 M 中为真。

在上述定义的第 1 条中，我们遵循常见做法，将谓词 X(t1,...,tn)给予集合论解释。将 X 解释为 Mn 的子集后，我们将谓词 X(t1,...,tn)解释为成员关系(tM1⟨s⟩,...,tMn⟨s⟩)∈s(X)。在第 2 条中，我们将属性和关系的量化解释为对笛卡尔积 Mn 的子集的量化。相应地，在第 3 条中，我们将函数的量化解释为在集合论意义下的函数集 Mn→M 的量化。

现在，我们已经定义了二阶逻辑的语义，我们可以定义公式 ϕ 成立的含义，以及两个公式 ϕ 和 ψ 在逻辑上等价的含义。与一般逻辑类似，我们说 ϕ 是（逻辑上）成立的，如果对于所有的 M 和 s，M⊨sϕ 都成立。同样，我们定义 ϕ 和 ψ 在逻辑上等价，ϕ≡ψ，如果 ϕ↔ψ 是成立的。如果对于所有的句子 ϕ，M⊨ϕ⟺N⊨ψ，则称模型 M 和 N 在二阶逻辑中等价，用符号表示为 M≡L2N。

真值定义涉及到“存在某个 P⊆Mn”和“存在某个 f:Mn→M”的概念。由于我们将集合论作为元语言，我们可以将其解释为集合论的意义上。因此，我们将“存在某个 P⊆Mn”解释为“存在某个集合 P⊆Mn”，将“存在某个 f:Mn→M”解释为“存在某个集合，它是一个函数 f:Mn→M”。

对于无限的 M，Mn 的子集的集合和 Mn→M 的函数集都是出名的复杂。目前的集合论（ZFC）甚至无法确定无限集合的子集有多少个。而一阶逻辑的情况则完全不同。相对而言，“存在某个 a∈M”的概念是没有问题的。当然，根据 M 的不同，“存在某个 a∈M”也可能是相当棘手的。为了反映在找到一个 P⊆Mn 或者一个 f:Mn→M 时所涉及的困难，我们有时会说我们“猜测”一个 P⊆Mn 或者一个 f:Mn→M。

当我们将集合论作为一阶逻辑语义的元理论时，对元理论的依赖程度比将集合论作为二阶逻辑语义的元理论时要低。解释这种差异的核心概念是绝对性。详见第 6 节。

3.1 二阶逻辑的 Ehrenfeucht-Fraïssé 游戏

Ehrenfeucht-Fraïssé 游戏是一种博弈论工具，用于研究两个模型在多大程度上相似（有关逻辑和游戏的条目中有关于 Ehrenfeucht-Fraïssé 游戏的一般介绍）。两个同构模型会非常相似，但通常我们对非同构模型的相似性感兴趣。二阶逻辑的 Ehrenfeucht-Fraïssé 游戏表征了 A≡L2N，即在 A 和 B 中完全相同的二阶句子为真，就像一阶逻辑的 Ehrenfeucht-Fraïssé 游戏表征了一阶元等价 A≡N。有关一阶模型论的条目中有关于元等价的更多内容。

为简单起见，在本节中，我们禁止使用函数和常量符号以及函数变量。假设 A 和 B 是相同有限关系词汇的两个模型。在我们用 G2n(A,B)表示的游戏中，两个玩家 I 和 II 轮流选择 A 的子集（或元素）或 B 的子集（或元素）。在游戏的第 i 轮中，玩家 I 可以选择 A 上的关系 Ai（或 A 的元素 ai），然后玩家 II 必须选择与 Ai 具有相同元数的 B 上的关系 Bi（或 B 的元素 bi），反之亦然：玩家 I 可以选择 B 上的关系 Bi（或 B 的元素 bi），然后 II 选择与 Bi 具有相同元数的 A 上的关系 Ai（或 A 的元素 ai）。经过 n 轮后，所玩元素（ai，bi）对形成 A×B 上的二元关系 R。如果该关系是由所玩的关系 Ai 和 Bi 扩展的结构 A 和 B 的部分同构，即它保持原子公式及其否定，我们称 II 获胜。当且仅当对于每个 n∈N，玩家 II 在 G2n(A,B)中有一个获胜策略时，模型 A 和 B 满足相同的二阶句子。如果存在一个 n，使得如果 A∈K 且玩家 II 在 G2n(A,B)中有一个获胜策略，则 B∈K，那么模型类（即具有固定词汇的模型类，闭合于同构）K 在二阶逻辑中是可定义的。

第一阶版本 G1n(A,B)，其中玩家只玩个别元素，即没有关系被玩，对于一阶逻辑来说非常有用。不幸的是，游戏 G2n(A,B)要复杂得多。除了在 A≅B 的平凡情况下，很难为玩家 II 发明获胜策略。如果玩家 I 在 A 上玩一个二元关系 R，玩家 II 应该能够在 B 上玩一个二元关系 R'，使得无论玩家 I 在游戏的其余部分提出什么挑战，甚至涉及新的二元关系，关系 R 和 R'看起来都是相似的。如果 V=L，那么可数的二阶等价模型（具有有限词汇）实际上是同构的（Ajtai 1979）。详见第 10 节。因此，在可数模型中，玩家 II 没有其他获胜策略，只有同构。也许这就解释了为什么这个游戏在二阶逻辑中不像在一阶逻辑中那么有用。然而，如果我们限制在单调二阶逻辑中，也就是在 Ehrenfeucht-Fraïssé 游戏中将游戏限制为一元谓词，情况就会改变。一元谓词只是将模型分成两部分。如果玩家 I 将 A 分成两部分，玩家 II 应该在 B 中找到一个类似的分割。这更合理，实际上有对玩家 II 有用的策略。在有限环境中的例子请参见第 16 节。

4. 二阶公式的性质

在一阶逻辑中我们习惯使用的许多句法操作在二阶逻辑中同样适用。其中之一是相对化操作，我们希望将一个公式表达的内容限制在宇宙的一个固定部分。例如，我们可以考虑使用某个一元谓词 U 表示自然数集合的模型。然后我们将我们的算术公理相对化到谓词 U 上。模型的另一部分可能用于自然数集合的幂集。然后我们将我们的幂集公理（见第 5.3 节）相对化到那部分，依此类推。

如果 M 是一个结构，且 A⊆M，则 MA 是通过将关系 RM 和函数 FM 限制在 A 上获得的。这并不总是导致一个结构，但如果导致了，就称为 M 相对于 A 的相对化。假设 ϕ=ϕ(x1,…,xn,X1,…,Xm,F1,…,Fk)是一个二阶公式，U 是一个一元关系变量。存在一个二阶公式 ϕU，将 ϕ 相对于 U 相对化，使得对于所有使得 MUM 是一个结构的 M：

M⊨ϕU⟺MUM⊨ϕ.

直观上，ϕU 关于 UM 所说的是 ϕ 关于 M 所说的。为了从 ϕ 获得 ϕU，我们将所有的一阶量词限制在 U 的元素上，将二阶量词限制在 U 上的子集、关系和函数上。

基于量词结构的层次结构是比较不同系统中概念可定义性的有用方法。在一阶逻辑中，很早就观察到公式可以转化为逻辑等价的前尼克斯标准形式，其中所有量词出现在公式的开头。这在二阶逻辑中也是可能的，证明基本上是相同的。此外，使用等价性（这类似于集合论中的选择公理，我们将在第 5.4 节中返回，因为在下面的公式中，关系 Y 在某种意义上为每个 x 选择一个 X，并将它们放在一起形成一个关系 Y - 有关选择公理的更多内容，请参见选择公理条目。）

∀x∃Xϕ≡∃Y∀xϕ′，

其中 Y 的元数比 X 的元数高一，ϕ′是通过将 ϕ 中的每个 X(t1,...,tn)替换为 Y(x,t1,...,tn)获得的，可以将每个二阶逻辑公式转化为逻辑等价的标准形式。

(4)Q1X1…QnXnϕ，

其中每个 Qi 要么是 ∃，要么是 ∀，ϕ 是一阶的。

表 1：二阶逻辑公式的层次结构。

通过限制 Prenex 标准形式（4）的量词序列 Q1X1…QnXn 可以包含的类型，我们得到 Σ1n-、Π1n-和 Δ1n-公式的类别，如表 1 所示。例如，二阶公式（1）和（2）是 Π11-公式。

在上面我们只考虑了绑定关系变量的量词，但如果我们绑定了函数变量，情况完全相同。

这些公式类具有一些明显的闭包性质：在逻辑等价的情况下，它们都在 ∧、∨ 和一阶量词下是封闭的。此外，从所有 n≥1 的意义上说，这个层次结构是适当的。

(5)Σ1n⊈Π1n 和 Π1n⊈Σ1n，

这可以通过对角线化论证来证明。Δ1n 类在 ∧、∨、¬ 和一阶量词下是封闭的。根据克雷格的插值定理，Δ11 公式在逻辑上等同于一阶公式 [2]。

从某种意义上讲，Π11，或者等价地说 Σ11，已经具有二阶逻辑的全部能力，尽管上述的层次结构结果（5）表明这不可能是字面上的真实。为了看到这一点，即看到将二阶逻辑归约为其 Π11 部分意味着什么，设 L 是一个词汇表，E 是一个二元关系符号，U 是一个一元关系符号，两者都不在 L 中。让 θ 是二阶 Π11 公式

(6)∀X(ϕ1∧ϕ2∧ϕ3)，

在这里

ϕ1 是 ∀x∀y(∀z(E(z,x)↔E(z,y))→x=y) ϕ2 是 ∀x∀y(E(x,y)→(U(x)∧¬U(y))) ϕ3 是 ∀x(X(x)→U(x))→∃y∀z(X(z)↔E(z,y)).

容易看出 [3]，θ 的模型在同构的情况下等同于模型 M，其中 M=UM∪P(UM)，UM∩P(UM)=∅，对于所有的 a,b∈M，EM(a,b)↔a∈b。在这样的模型中，UM 上的单调二阶公式 ϕ 可以简化为 M 上的一阶公式 ϕ∗。这种简化，由 Hintikka（1955）提出并由 Montague（1963）进一步发展，表明 Π11-公式足以表达带有额外谓词的任何二阶属性。这个思想可以扩展到三阶及更高阶逻辑。

因此，检验二阶句子 ϕ 的有效性可以递归地简化为检验 Σ11 句子 θ→ϕ∗ 的有效性。同样，检验二阶句子 ϕ 是否具有基数为 κ 的模型可以简化为询问 Π11 句子 θ∧ϕ∗ 是否具有基数为 2κ 的模型。这意味着整个二阶逻辑的 Löwenheim 数 [4] 和 Hanf 数 [5] 与 Π11 片段的相同。

总结起来，初步检查层次 Σ1n 和 Π1n 的二阶公式在表达能力上随着 n 的增加而严格增长，但更仔细的分析揭示出，即使能力有些隐含且需要揭示，第一层 Σ11∪Π11 已经具有所有层次 Σ1n、Π1n 的能力。

在集合论中，存在 Σn-和 Πn-公式的 Levy 层次（Lévy 1965）。其中所有量词都是有界的公式，即形如 ∀x∈y 或形如 ∃x∈y（其中 x 和 y 是某些元素），被称为 Σ0 或等价的 Π0。形如 ∀xϕ 的公式，其中 ϕ 是 Σn，被称为 Πn+1。形如 ∃xϕ 的公式，其中 ϕ 是 Πn，被称为 Σn+1。这是一个严格的层次结构，大致原因与二阶 Σ1n-和 Π1n-公式的层次结构严格相同。但目前没有已知的方法将任意公式的真实性简化为 Σ1∪Π1 层次上的公式的真实性。事实上，如果对集合论的 Σn∪Πn-公式适当定义决策问题、Löwenheim-Skolem 数和 Hanf 数，决策问题会变得越来越复杂，并且随着 n 的增加而获得的数值也会越来越大（参见定理 4；Väänänen 1979）。

在第二阶逻辑中，层次结构 Σ1n∪Π1n 和集合论中的层次结构 Σn∪Πn 在第 7 节中进行了比较。

5. 第二阶逻辑的臭名昭著的能力

5.1 将第二阶逻辑与一阶逻辑区分开来

二阶逻辑具有一些显著的特点，我们将在此详细揭示。在上面，我们通过（1）来描述了自然数的结构。这种应用二阶逻辑的方式可能是最著名且最重要的。现在，我们稍微更一般地重新表述它，以便获得更多的能力。假设 U 是一个一元关系变量（“自然数集合”），G 是一个一元函数变量（“后继函数”），z 是一个个体变量（“零”）。让 θPA(U,G,z)是以下句子：

(7)U(z)∧∀x(U(x)→(U(G(x))∧¬G(x)=z))∧∀x∀y((U(x)∧U(y)∧G(x)=G(y))→x=y)∧∀X([X(z)∧∀x((U(x)∧X(x))→X(G(x)))]→∀x(U(x)→X(x))),

那么，当且仅当(N,A,g,a)与一个结构(M,N,s,0)同构，其中 N⊆M 且 s(n)=n+1 时，(N,A,g,a)⊨θPA(U,G,z)。因此，我们使用二阶逻辑来表达 θPA(U,G,z)的任何模型的 U 部分，以及函数 G 和个体 z 与自然数 N 及其后继函数和零是同构的。有很多方法可以看出，没有任何一阶句子可以具有这种性质。例如，根据紧致性定理，这样的句子还将具有一个非标准模型，其中某个元素与序列 z，G(z)，G(G(z))，G(G(G(z)))中的每个元素都不同。这样的模型不能与自然数 N 及其后继函数和零同构。因此，我们可以得出结论，紧致性定理在二阶逻辑中的形式与一阶逻辑不同。

在模型 θPA(U,G,z)中，公式 θ+(U,G,z,H)

{∀x(U(x)→H(x,z)=x)∧∀x∀y(U(x)→(U(y)→H(x,G(y))=G(H(x,y))))

和公式 θ×(U,G,z,H,J)

{∀x(U(x)→J(x,z)=z)∧∀x∀y(U(x)→(U(y)→J(x,G(y))=H(J(x,y),x)))

定义唯一的函数 m+n=H(m,n) 和 m⋅n=J(m,n)。如果且仅如果在 (N,+,⋅,0) 中，一个一阶算术句子 ϕ(+,⋅,0) 为真，则

∀U∀G∀z∀H∀J((θPA(U,G,z)∧θ+(U,G,z,H)∧θ×(U,G,z,H,J))→(ϕ(H,J,z))U)

是有效的。我们知道在（N，+，⋅，0）中，一阶句子的真实性是不可判定的，甚至是非算术的，这是由哥德尔（1931 [1986: 144–195]）和塔斯基（1933 [1956]）的结果所证明的。这表明二阶逻辑不能完全地通过有效手段公理化，或者在空词汇中甚至是可判定的。也就是说，没有一个可判定的具有无限模型的二阶理论。这与一阶逻辑形成了鲜明的对比，在一阶逻辑中，以下理论是可判定的：空词汇的一阶逻辑，一元谓词的一阶逻辑，稠密线性序，Pressburger 算术（（N，+，0）的一阶理论），实闭域（（R，+，⋅，0，1）的一阶理论），代数闭域的理论，以及（C，+，⋅，0，1）的一阶理论。在二阶逻辑中，这些相应的二阶理论都是不可判定的。然而，如果我们将二阶逻辑限制为一元二阶逻辑，我们将得到许多重要的可判定理论（见 §8）。

5.2 完备性定理的崩溃

完备性定理是我们对一阶逻辑理解的基石之一。一阶逻辑的许多扩展也有完备性定理，尤其是通过广义量词“存在不可数多个”和无穷语言 Lω1ω 扩展的一阶逻辑。我们现在将看到，对于二阶逻辑来说，没有希望有一个完备性定理。在第 9.1 节中，我们将修改语义，以便证明完备性定理。

在完备性定理失败的背后，事实上是二阶逻辑——几乎可以说是根据定义——能够说一个集合是另一个集合的幂集。这意味着以下内容：设 L 是一个词汇表。设 E 是一个二元关系符号，U 是一个一元关系符号，两者都不在 L 中。设 θPow(U,E)是二阶公式（6）。让我们考虑以下的合取式

(8)θPA(U,G,z)∧θPow(U,E)。

这个公式的模型，在同构的意义下，形式为(M,∈,N,g,a)，其中 P(N)=M，N∩P(N)=∅，而 N 是可数无穷的。因此，这些模型必然是不可数的。这表明，与一阶逻辑不同，二阶逻辑具有只有不可数模型的句子。因此，正如我们在上面已经指出的那样，二阶逻辑的下降 Löwenheim-Skolem 定理失败了。将(8)与 §5.1 中的观察结果结合起来，得到以下结果（通过有效性，我们指的是有效公式的哥德尔数的集合）：

定理 3（Hintikka 1955; Montague 1963）在二阶逻辑中的有效性不能通过（N,+,⋅,0）进行二阶定义。

因此，二阶逻辑中的有效性对于任何 n 都不是 Σ1n。由于可以迭代地构建类似于 θPow(U,E)的幂集，我们可以看出二阶逻辑中的有效性对于任何 m 和 n 都不是 Σmn。我们在下面的定理 6 中进一步扩展了这个结果。

5.3 “羊皮狼心的集合论”

二阶逻辑在其语义中隐藏了一些集合论中最困难的问题。用 Resnik（1988: 75）的话来说：

在《逻辑哲学》[Quine 1970] 中，W. V. Quine 通过将二阶逻辑称为“羊皮中的集合论”来总结了数学逻辑学家中的一种流行观点。

让我们看看这种观点可能来自哪里。首先，我们观察到一个非常简单，确实是非常基本的二阶公式可以表达两个集合具有相同的基数：假设 P 和 R 是一元关系变量。让 θ≤(P,R)表示该公式。

∃F(∀x∀y((F(x)=F(y)→x=y)∧(P(x)→R(F(x)))).

现在，如果且仅当|s(P)|≤|s(R)|，则 M⊨sθ≤(P,R)。让 θEQ(P,R)为公式 θ≤(P,R)∧θ≤(R,P)。现在，如果且仅当|s(P)|=|s(R)|，则 M⊨sϕ(P,R)。让 θ′EC(Y)为

∃F(∀x∀y((F(x)=F(y)→x=y)∧R(F(x)))∧∀x∃y(R(x)→x=F(y))).

现在，当且仅当集合 M 和 s(R)具有相同的基数时，M⊨sϕ(P,R)。我们将使用这些公式对连续统假设进行攻击，这是集合论中的一个臭名昭著的问题，由科恩在 1963 年（科恩 1966 年）证明与 ZFC 独立。

让 θCH 成为句子

(9)∃E∃U∃G∃z(θPow(E,U)∧θPA(U,G,z)∧∀Y(θ′EC(Y)∨θ≤(Y,U)))。

现在，θCH 是一个空词汇的句子，只有当连续统假设 CH 成立时，它才有一个模型。同样，存在一个句子 θ¬CH，只有当连续统假设 CH 不成立时，它才有一个模型。这表明，二阶逻辑的语义依赖于元理论集合论的深度，以至于甚至 ZFC 无法解决的问题也可以确定模型中句子的真假。

二阶逻辑的奇特之处在于，一个足够大的空词汇模型中句子 θCH 的真实性等价于集合论宇宙中连续统假设的真实性。通过同样的技术，几乎任何集合论陈述都可以转化为二阶逻辑的句子，在足够大的空词汇模型中的真实性等价于在集合论宇宙中的真实性。不知何故，二阶逻辑能够正确解读背景集合论。这是否意味着二阶逻辑是“羊皮中的集合论”？

5.4 二阶逻辑是否依赖于选择公理？

选择公理（AC）是数学基础中的一个哲学难题。粗略地说，这个最初在集合论中出现的公理表明，如果我们有一个非空不相交集合 A，那么我们可以构造一个新的集合 B，其中包含 A 中每个集合的一个元素。问题在于，当 A 是无限集时，构造集合 B 似乎需要做出无限次选择。详细的定义和讨论请参见选择公理词条。一方面，选择公理似乎是神奇的，例如它暗示了最疯狂的集合具有良序性。另一方面，它似乎是无害的，例如它暗示了一族非空集合的笛卡尔积是非空的。选择公理通常用于构造奇怪的“悖论”集合，例如一个非勒贝格可测的实数集，实数的良序性，球体的悖论分解（请参见集合论词条），等等。这些集合通常在某种意义上是不可定义的。例如，如果存在足够大的基数（请参见大基数和确定性词条），那么一个非勒贝格可测的实数集在（N,+,⋅）上必须是二阶逻辑中不可定义的。

选择公理的困惑也出现在二阶逻辑的中间：设 θ 为以下命题

∀X(∀x∃yX(x,y)→∃F∀xX(x,F(x)))。

然后，R⊨θ 本质上是说，如果一个二元关系 X 与 R 中的每个 x∈R 相关联一个非空集合{y∈R:X(x,y}，那么存在一个函数 F，它为每个 x∈R 选择一些 y=F(x)，使得 X(x,y)成立。在集合论中，这是说选择公理对于（连续大小）R 的子集族成立的许多等价方式之一。二阶逻辑的基本原则是“所有”固定域的元素的属性都存在，我们可以对它们进行量化。用集合论的术语来说，这意味着任意基数的集合的所有可定义或不可定义的子集都存在，我们可以对它们进行量化。在这个意义上，选择公理似乎是无害的，并且通常在二阶逻辑的文献中被接受。

根据科恩的结果（1966），存在 N 和 N'满足 ZF 公理（不包括选择公理），使得“N⊨θ”在 N 中成立但在 N'中不成立。这进一步证明了二阶逻辑语义对元理论的依赖性。

6. 二阶逻辑中真理的非绝对性

绝对性是逻辑学中最重要的概念之一。哥德尔在他对可构造集合层次结构的分析中（1939 [1990: 46]）已经使用了这个概念，以证明连续统假设的一致性。哥德尔在三年前与可计算性概念相关时简要提到了这个概念（1936 [1986: 397]）。

直观地说，如果一个概念的意义与所使用的形式主义无关，或者换句话说，如果其在形式意义上的意义与其在“真实世界”中的意义相同，那么它就是绝对的。这听起来可能非常模糊和不精确。然而，在集合论中，绝对性有一个完全精确的技术定义。

回想一下，如果集合 a 的每个元素的元素都是 a 的元素，那么集合 a 被称为传递的。传递模型是一个模型（M,∈），其中 M 是传递的。根据莫斯托夫斯基折叠引理（Mostowski 1949），每个良基模型（M,E）都与一个传递模型同构，满足外延公理。传递模型（M,∈）的一个基本性质是，如果 a，b∈M，则 M⊨a⊆b 当且仅当 a⊆b。（如果 a 中的所有元素都在 M 中且在 b 中，则 a 中的所有元素都在 b 中，因为根据 M 的传递性，a 的元素必然是 M 的元素。）我们可以说，公式 x⊆y 在传递模型中是绝对的。更一般地说，如果对于所有传递模型（M,∈）和所有 a1，…，an∈M，存在一个有限集 T⊆ZFC，使得 ϕ(x1,…,xn)是相对于 ZFC 绝对的。

ϕ(a1,…,an)当且仅当(M,∈)⊨ϕ(a1,…,an)。

这个绝对性的定义等价于以下更语法的条件（Feferman & Kreisel 1966）：存在一个 Σ1-公式 ∃yψ(y,x1,…,xn)和一个 Π1-公式 ∀yθ(y,x1,…,xn)，使得

ZFC⊢∀x1…∀xn(ϕ(x1,…,xn)↔∃yψ(y,x1,…,xn))

和

ZFC⊢∀x1…∀xn(ϕ(x1,…,xn)↔∀yθ(y,x1,…,xn)).

在这种情况下，我们说 ϕ(x1,…,xn) 是 ΔZFC1.

对于一阶逻辑，可以证明“M⊨sϕ”是相对于 ZFC 的 M、s 和 ϕ 的绝对属性。事实上，即使将 ZFC 替换为较弱的 Kripke-Platek 集合论 KP（参见 Barwise 1972a），这个结论仍然成立。一阶逻辑的通常 Tarski 真理定义可以用 ΔZFC1 形式来表示。对于二阶逻辑，命题“ϕ 是一个二阶公式”、“M 是一个 L-结构”和“s 是一个赋值”相对于 ZFC 也都是绝对的，但是“M⊨sϕ”不是，我们将在下面看到。这是二阶逻辑的一个关键特性。如果将绝对性视为一个可取的特性，那么可以认为这是一个弱点；如果将非绝对性视为表达能力的标志，那么可以认为这是一个优势。无论是弱点还是优势，这都是二阶逻辑的一个重要特征，也是关于二阶逻辑的讨论中的一个主要话题。然而，二阶逻辑并不是唯一的非绝对逻辑。例如，L(Q1)（参见广义量词条目）和 Lω1ω1（参见无穷语言条目）是非绝对的，而 L(Q0)和 Lω1ω 是绝对的。L(Q0)是绝对的主要原因在于在 ZFC 的传递模型中，集合无限的性质是绝对的。虽然 Lω1ω 的句子集合可能因为 ZFC 的不同传递模型而有所变化，但是在传递模型中，Lω1ω 的句子的真值是绝对的，主要是因为真值具有一个简单的归纳定义，只涉及句子的子公式和模型的元素。

回顾第 5.3 节中句子 θEC(P,R)的定义，该定义表明谓词 P 和 R 的解释具有相同的基数。基数不是绝对的属性。在 ZFC 的一个传递模型中，两个集合（甚至两个序数）的基数可以不同，在一个传递扩展中的基数可以相同。很容易看出，“M⊨sθEC(P,R)”相对于 ZFC 来说并不是绝对的。本质上，原因是如果两个集合之间存在双射，则它们具有相同的基数。在一个小的传递集合中，可能存在这些集合，但表现它们等基数的双射却不存在。这个双射可能是通过强制方法获得的。或者缺乏这个双射可能是应用了下降的 Löwenheim-Skolem 定理的结果 [6]。

更严重的非绝对性情况是第 5.3 节中的句子 θCH。空词汇的句子 θCH 只有在连续统假设为真时才有模型。如果 T⊆ZFC 是有限的，则存在可数的传递模型 M⊆M'，其中一个模型 M 满足 CH，而另一个模型 M'不满足（由 Cohen 1966 得出）。在 M 中，句子 θCH 有一个模型 A，即 M⊨“A⊨θCH”。在 M'中，同样的句子没有模型，特别是 M'⊭“A⊨θCH”。因此，满足二阶句子的模型的性质相对于 ZFC 来说并不是绝对的。甚至具有模型的二阶句子的性质相对于 ZFC 来说也不是绝对的，因为在 M 中，句子 θCH 有一个模型，但在 M'中没有。对于一阶逻辑，具有模型的句子的性质是可判定的，因此是算术的。算术性质相对于 ZFC 来说总是绝对的。如果连续统假设被替换为选择公理（见第 5.4 节），情况是类似的。

CH 和 AC 是集合论的核心问题，也是持续争论的主题。虽然 AC 大多被接受为公理，并且是 ZFC 公理系统的一部分，但 CH 被广泛认为是一个未解问题。甚至有人提出（例如，Feferman 1999）它不能通过任何具有与 ZFC 一样普遍接受的公理系统来解决。数学基础的形式主义立场更进一步，主张 CH 的真值是无意义的。在 ZFC 的前提下，CH 及其否定与 ZFC 一致。根据形式主义立场，CH 的地位已经得到解决。基于这些关于集合论的难题的二阶逻辑的语义将二阶逻辑与集合论放在同一个“篮子”中。对集合论的批评成为对二阶逻辑的批评，反之亦然。

另一个表明二阶逻辑依赖于集合论作为元理论的迹象是 Barwise 的结果，即在不使用高度复杂的替换公理的情况下，无法在集合论中证明二阶逻辑的 Hanf 数的存在（详见 Barwise 1972b）。

7. 二阶逻辑的模型论

让我们首先注意到，二阶逻辑能够量化关系的一些微不足道的结果。例如，对于微不足道的原因，克雷格插值定理适用于二阶逻辑：如果 ϕ 的有限关系词汇是 L，ϕ′的有限关系词汇是 L′，且 ⊨ϕ→ϕ′，那么存在 θ 使得 ⊨ϕ→θ 且 ⊨θ→ϕ′，且 θ 的词汇是 L∩L′，因为我们可以让 θ 成为句子 ∃X1…∃Xnϕ，其中 L∖L′={X1,…,Xn}。我们还可以要求 θ 中的每个正出现的谓词符号在 ϕ 和 ψ 中也正出现，并且 θ 中的每个负出现的谓词符号在 ϕ 和 ψ 中也负出现（琳登插值定理 [琳登 1959]）。同样，由于微不足道的原因，贝丝可定义性定理也成立，还有一些保持结果 [7] 有一个微不足道的证明。有关负面结果，请参见克雷格 1965 年的论文。

然而，二阶逻辑没有像一阶逻辑那样的模型论。没有紧致性定理来产生非标准模型。一阶逻辑之所以有如此丰富的模型论，是因为一阶逻辑相对较弱。可数的一阶理论具有无穷模型的情况下，具有所有无穷基数的模型。这是一阶逻辑的一个弱点的结果：除非模型的大小是有限的，否则它的句子不能限制模型的大小。在模型论中，这种弱点被转化为一种优势：一阶理论的模型结构可以以有趣的方式进行分析。有关此的示例，请参见模型论条目。

二阶理论通常只能有一个模型，直到同构。因此，如果我们研究一个二阶句子的模型类，这个类很可能只包含一个模型，直到同构。只有一个模型，我们无法真正发展模型论。我们最终只能研究这一个唯一的模型，没有令人信服的理由使用逻辑来研究它。如果这个唯一的模型是一个代数结构，我们应该使用代数来研究它。如果它是一个有序结构，我们应该使用有序结构的一般理论来研究它，依此类推。很难说二阶可表征性（见 §7.1）对结构本身有多大的意义。它更多地揭示了关于二阶逻辑的一般性质。例如，能够表征自然数结构意味着紧致性定理和完备性定理失败。能够表征实数有序域意味着向下和向上的 Löwenheim-Skolem 定理都失败了。从这个角度来看，了解哪些结构可以二阶可表征性同构是有趣的。

最后，让我们比较两个层次结构，即模型论层次结构 Σ1n∪Π1n 在二阶逻辑中和 Levy 层次结构 Σn∪Πn 在集合论中。

定理 4

  1. 有效的二阶句子的哥德尔数集是自然数的完全 Π2 集。（Tharp 1973）

  2. 二阶逻辑的 Löwenheim-Skolem 数是所有 Π2 可定义的序数的上确界。（Krawczyk＆Marek 1977）

  3. 二阶逻辑的 Hanf 数是所有 Σ2 可定义的序数的上确界。（Krawczyk＆Marek 1977）

  4. 在二阶逻辑中可定义的每个模型类都可以在集合论中 Δ2-定义。（Väänänen 1979）

根据上述定理，二阶逻辑坐落在集合论可定义性的 Σ2∪Π2 级别上。这是认为二阶逻辑比一阶集合论更弱的一个原因。这听起来有些矛盾。当一阶逻辑甚至无法表达有限性、可数性、不可数性等时，二阶逻辑如何比基于一阶逻辑的集合论更弱，尽管它具有所有的能力和非一阶特性？然而，定理 4 的信息是不可否认的。也许如果我们将集合论视为对空集的单例的非常高阶逻辑，这就不会那么令人困惑了。毕竟，集合论允许无限次的幂集操作迭代，而二阶逻辑只允许一次迭代。

我们从下面的一个小节开始，讨论可以通过一句话来表征的二阶逻辑模型的同构性。二阶逻辑模型理论的另一种方法是关注具有大基数（不可达基数、可测基数、超紧基数）属性的模型。这是第 7.2 节的主题。最后，在第 7.3 节中，我们考虑允许所谓的在第 9.1 节中引入的一般模型的可能性。在这种情况下，二阶逻辑非常类似于一阶逻辑。然而，一般模型在它们被称为 Henkin 模型时才是最有趣的，即它们满足所谓的包含公理。在 Henkin 模型中，二阶逻辑满足紧致性定理和其他来自一阶模型论的原理，但尚不存在一般的结构或分类理论，也许是因为包含公理为模型引入了许多复杂的结构。

7.1 二阶可表征结构

如果存在一个二阶句子 θA，使得对于与 A 具有相同词汇的所有结构 B，B⊨θA⟺B≅A，则结构 A 是二阶可表征的。

例子 5：以下结构是二阶可表征的：

  1. 自然数：(N,+,⋅)。

  2. 实数：(R,+,⋅,0,1)。

  3. 复数：(C,+,⋅,0,1)。

  4. 第一个不可数序数 (ω1,<).

  5. 累积层次的层级 (Vκ,∈)，其中 κ 是第一个强不可及基数 >ω.

  6. 第一个弱紧基数 >ω 的良序 (κ,<).

所有结构都是二阶可表征的吗？只有可数多个二阶句子，因此只有可数多个（在同构下）二阶可表征的结构。因此，每个无限基数都有很多不是二阶可表征的结构。然而，给出例子并不容易。一个例子是（κ，<），其中κ是第一个可测基数（> ω）。详见第 7.2 节的解释。另一个例子是（N，<，A），其中 A 是一个二元关系词汇中有效的二阶句子的哥德尔数集合。详见第 7.2 节的解释。人们可能会问是否存在一个来自数学实践而不是数理逻辑的例子。那么（R，+，×，<，A）怎么样？其中 A 是一个哈梅尔基（向量空间的基，实数是向量，有理数是标量，向量加法是实数的常规加法）。相对于 ZF 的一致性，没有这样的结构（R，+，×，<，A）是二阶可表征的（Hyttinen，Kangas 和 Väänänen 2013）。

二阶可表征结构的一个特殊属性是它们的约简也是二阶可表征的，因为我们可以使用存在性二阶量词来“猜测”缺失的关系和函数。因此，寻找具有尽可能多（但仅有有限多个）关系和函数的可表征结构是有趣的。我们可以赋予 N 任意有限数量的递归函数 f1，…，fn 和关系 R1，…，Rm，从而得到结构（N，f1，…，fn，R1，…，Rm），这是二阶可表征的。我们可以赋予 R 任何熟悉的解析函数，如三角函数或由收敛幂级数给出的任何其他函数，其系数由递归函数给出，结果是二阶可表征的。

显然，二阶可表征结构 A 的二阶理论可以简化为任何更大的二阶可表征结构 B 的二阶理论，对于所有的二阶 ϕ：

A⊨ϕ⟺B⊨∃P(θPA∧ϕP)。

可表征结构越大，二阶理论越复杂。可以从以下方面看出，不存在最大的可表征结构：如果 A 是二阶可表征的，那么将 A 还原为空词汇的约简 [8] 也是二阶可表征的，即 A 的基数|A|是可表征的。这样的基数被 Garland（1974）研究过。例如，如果 κ 是可表征的，那么 κ+和 2κ 也是可表征的。

如果 ϕ 是一个二阶句子，我们定义

Mod(ϕ)={M:M⊨ϕ}。

如果 ϕ 表征一个模型 A，那么 Mod(ϕ)就是与 A 同构的模型类。如果我们从集合论的角度看 Mod(ϕ)，我们知道它是 Δ2 的（定理 4）。另一方面，有效的二阶句子的哥德尔数集是 Π2-完备的（定理 4），因此不是 Σ2，特别地也不是 Δ2。这种思考引导我们到上述定理 3 的扩展：

定理 6（Väänänen 2012）二阶有效性在任何二阶可表征结构上都不是二阶可定义的。

这引发了一个问题，我们如何从二阶的角度理解二阶有效性？根据上述定理，我们无法将二阶有效性理解为可以在某个可以用二阶逻辑表达的结构上表达的东西，而这个结构本身可以用二阶逻辑来表征。在理解二阶有效性时，对集合论的参考似乎是不可避免的。让我们从结构主义的角度讨论这可能意味着什么。Parsons 将结构主义定义如下：

通过“数学对象的结构主义观点”，我指的是引用数学对象总是在某个背景结构的上下文中进行，并且所涉及的对象没有超出结构的基本关系所能表达的内容。（Parsons 1990: 303）

从这个意义上讲（对于其他类型的结构主义，请参见 Hellman 2001），结构主义似乎很适合二阶逻辑学的框架。与集合论相反，二阶逻辑学总是假设一个基础（有限）结构，该结构被认为反映了数学的一个特定方面，例如自然数的半环，实数的有序域，复数域，良序结构（ω1，<），等等。理想情况下，这些基础结构是二阶可表征的。这导致了一个关于普遍真理的问题，例如有效性，以及关于较不复杂的真理，例如每个线性序有一个完备性，或者每个域都有一个代数闭包。这些普遍真理不涉及任何特定的结构。

7.2 二阶逻辑学和大基数

我们参考 SEP 中关于独立性和大基数以及大基数和确定性的定义来定义与大基数相关的概念。

关于二阶逻辑模型论和大基数之间的联系的以下早期结果是其他更微妙结果的模型。这是二阶逻辑的一种向下 Löwenheim-Skolem 定理。它说，如果一个二阶句子有一个可测基数的基数模型，那么它有一个更小的子模型：

定理 7（Scott 1961）假设 κ 是一个可测基数。如果 ϕ 是一个二阶句子，ϕ 有一个基数为 κ 的模型 M，那么对于每个基数<κ 的 X⊆M，存在 N⊆M，使得 X⊆N，|N|κ，并且 N⊨ϕ。[9]

一个特殊的结果是第一个可测基数不能作为一个空词汇的二阶可刻画模型（这个事实在 7.1 节上面提到过）。定理 7 与一阶逻辑的向下 Löwenheim-Skolem 定理非常相似。唯一的区别是必须从一个大模型开始，一个基数大小的模型。较小的基数可能不起作用。例如，如果 λ 是最小的弱紧基数>ω，则存在一个句子 ϕ，它以 λ（使用空词汇）作为模型，但没有更小的模型。句子 [10] ϕ 表示 λ 是不可达的（>ω），并且每个 λ 树（高度为 λ，所有级别大小<λ）都有一个长度为 λ 的分支。

如果我们想要获得一个适用于任何结构的下降型 Löwenheim-Skolem 定理，而不仅仅适用于可测基数的结构，我们必须考虑更大的基数：二阶逻辑的 LST 数被定义为最小的（如果存在的话）κ，使得对于任何结构 A 和在 A 中为真的二阶句子 ϕ，存在一个基数为 κ 的 A 的子结构 B，也满足 ϕ。

定理 8（Magidor 1971）：如果存在超紧基数>ω，那么二阶逻辑的 LST 数存在，并且它是其中最小的。

二阶逻辑被认为满足强 κ-紧致性，如果每个二阶理论，其大小小于 κ 的每个子集都有一个模型，那么该理论本身也有一个模型。

定理 9（Magidor 1971）二阶逻辑满足强 κ-紧致性的最小 κ 是最小的可扩展基数。

7.3 一般模型和 Henkin 模型的模型论

如果我们采用所谓的一般模型（§9.1），情况将完全改变。对于一般模型，二阶逻辑具有与一阶逻辑类似的模型论性质，因为它可以简单地被视为多排序的一阶逻辑（参见 §9.1 和 Manzano 1996）。总的来说，多排序一阶逻辑的结果可以立即转化为二阶逻辑。

8. 可决定性结果

二阶逻辑即使在空词汇的情况下也是不可决定的，正如我们在 §5.1 中所指出的。相比之下，一阶单调逻辑产生了许多重要的可决定性结果。首先让我们观察到（不仅在空词汇中，而且）在一阶词汇中，即仅由一阶谓词组成的词汇中，一阶单调逻辑肯定是可决定的，正如 Löwenheim（1915）在关于形式逻辑数学方面的最早的论文之一中已经证明的那样。Löwenheim 的结果可以通过量词消除轻松证明，或者通过更近期的 Ehrenfeucht-Fraïssé 游戏方法证明（见 §3）。然而，一阶词汇中的一阶三阶（及更高阶）逻辑，其量词不仅涉及域的子集，还涉及域的子集的集合，是不可决定的（Tharp 1973）。我们现在将重点放在不仅仅是一阶的词汇上。

与一阶词汇相比，另一个极端可以描述如下：设 P 是一个三元谓词（“配对函数”），作用于非空集合 S 上。假设对于每个 x，y∈S，存在 z∈S 使得（x，y，z）∈P，并且对于每个 z∈S，最多只有一对（x，y）使得（x，y，z）∈P。那么 S 的真（完全）二阶理论可以在（S，P）的一阶理论中解释（Gurevich 1985）。换句话说，在存在配对函数的情况下，例如集合论和数论中，将二阶逻辑限制为其一阶片段并没有特殊的优势。

从仅包含一元谓词的词汇开始，下一步是具有恰好一个一元函数的词汇。为了描述在这种情况下的一些非常非平凡的结果，我们引入了以下概念，它具有独立的兴趣：一阶或二阶句子的谱是其有限模型的基数集合。谱由 Scholz 引入，参见 Durand、Jones、Makowsky 和 More（2012）的历史。谱当然总是递归的。实际上，自然数集合是一阶句子的谱，当且仅当它在 NEXPTIME 中，即可以由指数时间的非确定性图灵机识别（Jones＆Selman 1974）。对于仅具有一个一元函数符号的句子，存在一个令人惊讶的特征。让我们称一个自然数集合 S 为最终周期性的，如果存在自然数 N 和 p（p>0），使得对于每个 n（n>N），我们有 n∈S 当且仅当 n+p∈S。

定理 10（Durand，Fagin 和 Loescher 1998；Shelah 2004）假设词汇只有一个一元函数。那么，如果一个自然数集合是单调二阶句子的谱，那么它也是一阶句子的谱，当且仅当它是最终周期性的。

在图中，单调二阶逻辑仍然可以表达最有趣的属性。例如，图的连通性（这里 E 是边关系）可以通过以下句子来表达

∀X((∃xX(x)∧∀x∀y((X(x)∧xEy)→X(y)))→∀xX(x))

和图的 3-可着色性通过以下句子

∃X∃Y∃Z(∀x(X(x)∨Y(x)∨Z(x))∧∀x∀y(((X(x)∧X(y))∨(Y(x)∧Y(y))∨(Z(x)∧Z(y)))→¬xEy))

在线性序、树和图上，一阶逻辑的可决定性结果非常丰富。

定理 11（Büchi 1962; Elgot 1961; Rabin 1968）：自然数 N 上的一阶逻辑理论（N，s），即 N 上的后继函数，以及全体无限二叉树上的一阶逻辑理论，即两个后继函数的理论，都是可决定的。

证明通过将问题归约到自动机上。自动机是图灵机的一种受限形式。在自动机中，机器不会在纸带上写入任何内容，因此纸带上只包含输入（Rabin & Scott 1959）。然而，计算可能是无限的。如果无限计算达到接受状态无数次，那么输入被认为是被接受的（还有更复杂的接受标准）。使用一阶逻辑，我们可以猜测自动机的一个接受计算。但是，证明自动机可以检查一阶逻辑句子的真假则更加困难。从可决定性的角度来看，序数（α，<）的一阶逻辑理论已经得到了广泛研究。例如，所有可数序数的一阶逻辑理论、ω1 的理论以及所有小于 ω2 的序数的理论都是可决定的（Büchi 1973），但是 ZFC 无法确定 ω2 的一阶逻辑理论是否可决定（Gurevich，Magidor，& Shelah 1983）。

9. 二阶逻辑公理

回顾我们的约定：每当我们使用大写的 Fraktur 字母，比如 A、B、M、N 等，来命名一个结构时，我们使用相应的大写 Italic 字母，比如 A、B、M、N 等，来命名该结构的域。

二阶逻辑的演绎系统，最早在希尔伯特-阿克曼（Hilbert & Ackermann 1938）中明确提出，它基于一阶逻辑的公理和规则的明显扩展，以及所谓的包容公理模式，定义如下：假设 ϕ(x1,…,xn)是一个二阶公式，其中 x1,…,xn 是其自由个体变量，且二阶变量 R 在 ϕ 中不是自由的。那么以下公式是包容公理模式的一个实例：

(10)∃R∀x1…xn(ϕ(x1,…,xn)↔R(x1,…,xn)).

二阶公式定义函数的类似模式也存在，但我们在此省略。

数论中一个非常简单的二阶推理的例子是

2+5<9∃R R(2+5,9)∃F∃R R(F(2,5),9)

A priori ( 10)可能看起来非常强大，因为它规定了一个关系的存在。然而，接受这样一个 R 似乎是合理的，因为它是可定义的：

R={(a1…an)∈Mn:M⊨ϕ(a1,…,an)}.

我们的理解公理模式在某种意义上是内涵的，因为可能出现在公式 ϕ(a1,…,an)中的有界 n 元关系变量在其范围内具有 R。从这个意义上说，二阶逻辑是完全内涵的。理解公理模式有较弱的形式，它们不那么内涵。在算术理解模式中，我们假设 ϕ(a1,…,an)是一阶的。在 Π11-理解模式中，我们假设 ϕ(a1,…,an)是 Π11 的。在数学实践中，这两个较弱的原则通常足够，参见 Simpson（1999 [2009]）和第 14 节。

Hilbert-Ackermann（1938）在二阶逻辑的证明系统中还添加了两个不同的模式，他们称之为选择公理。我们习惯于将选择公理视为集合论原理。但是二阶逻辑与集合论一样具有选择原理的情况。在二阶逻辑中，询问域是否存在良序是完全有意义的。一般情况下，这样的良序不是由内涵模式推出的，因为良序可能是---并且很可能是---不可定义的。因此，在二阶逻辑中获得实数的良序，比如说，唯一的方法是假设某种形式的二阶选择公理。第一个选择原则是

(AC)∀x1…xm∃xm+1R(x1,…,xm+1)→∃F∀x1…∀xmR(x1,…,xm,F(x1…xm))

而第二个是

(AC')∀x1…xm∃Fφ→∃F′∀x1…xmφ′,

其中公式 φ′ 是通过在公式 φ 的每个地方替换 F(t1,…,tk) 为 F′(t1…tk,x1,…,xm) 而得到的。

选择公理（AC）的第一条直观地说，如果一个集合

{an+1∈M:M⊨R(a1,…,an,an+1)}

是非空的，那么存在一个函数，使用参数 a1,…,an 作为参数，从集合中选择一个元素 an+1。选择公理的第二条（AC'）是一种二阶选择：对于所有的 a1,…,an，存在一个具有性质 ϕ 的函数 F，实际上 F 取决于 a1,…,an，并且应该表示为 Fa1…an。现在（AC'）所说的是，我们可以将函数 Fa1…an 收集在一起，形成一个更高阶的函数 F'，使得它的元数更高，这样

F′(a1,…,an+1)=Fa1…an(an+1).

虽然 F'似乎是可定义的，但事实并非如此，因为映射

(a1,…,an)↦Fa1…an

可能是高度不可定义的。

自然地，我们可能还希望假设良序原理，即存在一个二元关系，它是个体上的全序，并满足每个非空个体集合在该序关系下都有一个最小元素的条件。很容易看出，这个原理蕴含了（AC'）。在 ZFC 中，存在着数百个等价的选择公理的表述或其较弱版本。在 ZFC 中等价的大多数表述在二阶逻辑中是不等价的。这是因为集合论允许在集合和它们的幂集之间自由移动，但是二阶逻辑不允许 [11]。要获得与集合论中类似的等价证明，就必须在二阶逻辑和三阶逻辑之间进行移动，参见 Gaßner（1994）。

9.1 一般模型和 Henkin 模型

“一般模型”的概念是由 Henkin（1950）引入的，目的是为了获得二阶逻辑的完备性定理。一般模型并不是公理的预期模型，因为绑定的关系和函数变量在这些模型中并不涵盖所有的关系和函数，而只涵盖其中的一部分。对于一般模型，普遍接受的态度是它们并不是人们所期望的，但是它们对于获得一个连续的理论是必要的。它们就像微积分中的无理数：如果在微积分（或几何学）中遇到的所有长度都是可比较的，那将是理想的，但事实并非如此。有些长度是不可比较的，我们最终接受无理数，以便拥有一个平滑的长度和比例的一般理论。一般模型也可以与集合论的传递模型进行比较。一个传递模型可能说某个命题为真，另一个传递模型可能说相反为真。但是，传递模型共同帮助我们理解集合论的公理。目前在集合论公理的元数学研究中使用的方法，即内部模型和强制扩张，都以集合论的传递模型为基础。类似地，二阶逻辑的一般模型帮助我们研究二阶逻辑及其公理的元数学性质。

定义 12 一般模型是一个二元组（M，G），其中 M 是一个通常的 L-结构，G 是 M 上的一组子集、关系（任意元数）和函数（任意元数）。在单调二阶逻辑中，假设 G 只包含一元谓词。

我们可以定义概念

(M,G)⊨sϕ

对于二阶的 ϕ，通过规定的归纳法

(M,G)⊨s∃Xϕ⟺(M,G)⊨s(P/X)ϕ，其中 P∈G.(M,G)⊨s∃Fϕ⟺(M,G)⊨s(f/X)ϕ，其中 f∈G.

二阶逻辑的原始真理定义与二阶变量的解释不完全任意，它们必须在 G 中找到。G 越小，逻辑越弱。另一方面，如果 G⋆ 是 M 上的所有关系和函数的集合，则对于一般模型（M，G⋆）的真理定义与原始真理定义相同。我们称这样的一般模型为全面模型，并将（M，G⋆）与 M 等同起来。另一个极端情况是 G=∅。那么我们回到了一阶逻辑。为了区分具有一般模型的二阶逻辑和原始二阶逻辑，我们称后者为全面的。

定义 13：满足二阶逻辑所有公理，包括包含公理模式和选择公理的一般模型称为亨金模型。

注意，没有二阶逻辑的句子说模型是全面的。也就是说，不存在二阶 ϕ，使得对于所有一般模型（M，G），它成立。

(M,G)⊨ϕ⟺(M,G) 是满的.

如果我们尝试将 ∀X∃Y∀x(X(x)↔Y(x)) 作为这样的 ϕ，我们只会得到 ϕ 总是为真，并且说一般模型 (M,G) 在其自身的“满”的意义上是“满”的结果，而不是在元理论的意义上。

获得一个 Henkin 模型 (M,G) 的自然尝试是让 G 由 M 上的一阶可定义的关系和函数组成。然而，通过这种方式，我们只能得到算术理解，而不是完整的理解公理。

获得一个 Henkin 模型(M,G)的简单方法是取一个 ZFC 的传递模型 N，使得 M∈N，并且让 G 包含所有在 M 上的关系和函数，这些关系和函数是 N 的元素。由 N⊨ZFC 可知，(M,G)是一个 Henkin 模型。

在一个一般模型中，即命题“(M,G)⊨sϕ”的真值相对于 ZFC 是绝对的，与(完全)二阶逻辑的真值定义相反。在这方面，具有一般模型的二阶逻辑类似于一阶逻辑。正如我们将看到的，它在许多其他方面也类似于一阶逻辑。

具有一般模型的二阶逻辑可以用多排序逻辑来思考。多排序逻辑是一阶逻辑，其中有几种不同类型的变量。相应地，关系和函数可以是不同类型的元素之间的关系和函数。这里的“类型”只是指通过给它们不同的名称来区分不同“类型”的变量。否则，变量只是普通的一阶变量。多排序逻辑的结构 M 对于每个类型 s 都有一个单独的域 Ms。我们可以将二阶逻辑看作是多排序逻辑，其中个体变量是类型 sin 的，每个 n 元关系变量是类型 sren 的，n 元函数变量是类型 sfun 的。此外，还有一个 n+1 元关系符号 Aren，它在个体 n 元组和 n 元关系变量之间指示哪些 n 元组在关系中，哪些不在关系中。最后，还有一个 n+1 元函数符号 Afun，它在个体 n 元组、个体和 n 元函数变量之间指示函数变量对每个 n 元组给出的值。有明显的一阶公理保证了刚刚描述的多排序逻辑忠实地反映了具有一般模型的二阶逻辑。[12]

关于将二阶逻辑归约为多分类逻辑的更多信息，请参阅 Manzano（1996）。例如，可以通过将二阶逻辑翻译为多分类逻辑来理解二阶逻辑的证明理论。关于二阶逻辑的证明理论，请参阅 Buss（1998）。多分类逻辑进一步通过 Herbrand（1930）的单分类一阶逻辑翻译，参见 Wang（1952）和 Schmidt（1951）。这可以用来获得多分类逻辑和二阶逻辑的一般模型的基本属性。

一般模型最重要的应用是完备性定理：

定理 14（Henkin 1950）：如果一个二阶句子从公理中推导出来，那么它在所有 Henkin 模型中都为真。[13]

分别地，我们得到了紧致性定理 [14] 以及 Löwenheim-Skolem 定理的向下和向上版本 [15]。

一种思考亨金模型的方式是它们填补了完全模型留下的空白，就像无理数填补了有理数留下的空白一样。为了得到一个平滑的二阶逻辑理论，它们是必需的。它们展现了我们在完全模型中看不到的“悖论”现象。例如，我们得到了非标准的数论模型，可数的实数公理模型等。现在，用于描述数学结构的范畴句子突然也有了其他“模型”，即亨金模型，并且它们具有各种无限基数。

如果 ϕ 是一个二阶句子，我们定义

(11)ModH(ϕ)={(M,G):(M,G)⊨ϕ}

显然，Mod(ϕ)⊆ModH(ϕ)。如果 ϕ 能够表征 M 的同构特性，则 M∈Mod(ϕ)。在所有非平凡的情况下 [16]，ModH(ϕ)≠{M}。我们可以将 ModH(ϕ)看作 M 的一类“近似”。其中一个近似是“真实”的 M，但通过二阶逻辑的推导，我们无法确定哪一个是真实的。由于形式系统的固有弱点，回溯到 Skolem 和 Gödel，无限结构被 Henkin 模型所掩盖，无法通过演绎手段完美地聚焦。

Fraenkel-Mostowski 方法是一种构建 Henkin 模型的方法，最初在集合论中用于获得选择公理失败的模型，后来在二阶逻辑中用于获得类似的模型，直到强制方法出现。该方法如下：假设 A 是一个结构，H 是 A 上的一组置换。如果存在一个有限集 E⊆A（称为 B 的支持集），使得对于所有点对点固定 E 的 π∈H，B 的 An 子集称为对称子集 [17]，

∀x1…∀xn((x1,…,xn)∈B→(π(x1),…,π(xn))∈B).

函数 f:An→A 的相应条件是

∀x1…∀xn((x1,…,xn)∈B→f(π(x1),…,π(xn))∈B∧f(π(x1),…,π(xn))=π(f(x1,…,xn)))

令 G 为 A 上的对称关系和函数的集合。对于任意的(A,G)都是一个 Henkin 模型。

Fraenkel-Mostowski 方法的早期应用之一是 Mostowski (1938)的结果，即仅凭借包含公理模式无法证明两个不同定义的有限性等价，以及 Lindenbaum 和 Mostowski (1938)的结果，即 Zermelo 的集合论公理不足以证明选择公理，甚至仅仅是每个无限集都是两个无限集的不相交并集。

如果 H 是无限集 A 上的所有置换的群，则产生了 Fraenkel 模型。在 Fraenkel 模型中，集合 A 是无限的但是 Dedekind 有限的（即 A 没有一对一函数映射到一个真子集），不能被良序，甚至不能被线性排序。此外，集合 A 不是两个无限集的不相交并集。对于 A 的两个元素子集，不存在选择函数。

如果 A=Q 且 H 是(Q,<)的自同构群，则出现了 Mostowski 模型。在 Mostowski 模型中，集合 A 可以被线性排序但不能被良序。选择公理对于（非空有限集的）集合成立。

关于 Fraenkel-Mostowski 模型作为二阶逻辑的 Henkin 模型的更多信息，请参见 Gaßner（1994）。

9.2 无穷公理

回想一下我们的约定：每当我们使用大写的 Fraktur 字母，比如 A、B、M、N 等，来命名一个结构时，我们使用相应的大写 Italic 字母，比如 A、B、M、N 等，来命名该结构的域。

二阶逻辑的公理在只有一个元素的（完全）模型中是显然成立的。这引发了一个问题，即如何保证域中有多于一个元素。当然，我们可以为每个 n 添加一个公理，该公理表明域中有多于 n 个元素。在二阶逻辑中，有多种方式可以用一个公理来表达存在无限多个个体。这些方式在完全模型中是等价的，但在 Henkin 模型中可能是非等价的。如果假设了选择公理，其中一些方式是等价的。让我们称一个空词汇的二阶句子 ϕ 为无穷公理，如果

当且仅当 A 是无穷的时，A⊨ϕ。

无穷公理可以在二阶逻辑中表达为：域的一个真子集与整个域具有相同的基数（即，域不是戴德金有限的），或者存在一个没有最大元素的偏序集，或者存在一个具有一元函数和常数的集合，构成一个与（N，s，0）同构的结构，或者域是两个不相交集合的并集，这两个集合与域具有相同的基数，等等。与没有选择公理的集合论一样，无穷性的不同表述不一定是等价的。在二阶逻辑中，情况更加复杂，因为选择公理有多种不同的表述。我们参考 Asser（1981）对不同变体的讨论，以及 Hasenjaeger（1961）对无穷公理的各种非等价形式形成一种稠密集的证明。有关有限性不同概念的调查，请参见 de la Cruz（2002）。

10. 一致性

二阶（或一阶）逻辑中的一个理论被称为是一致的，如果它的任意两个模型是同构的。一个单一的句子（具有一个模型）是一致的，当且仅当它以同构的方式表征某个模型（见 §7.1）。一种一致理论 Γ 的一个好的性质是（语义）完备性：在理论所写的语言中，Γ 决定了任何句子 ϕ 的意义。要么 Γ 的每个模型都满足 ϕ，要么 Γ 的每个模型都满足 ¬ϕ。换句话说，ϕ 或 ¬ϕ 是 Γ 的（语义）逻辑推理的结果。原因非常简单：Γ 只有一个模型 M，与同构保持二阶逻辑中的真值。根据 ϕ 在 M 中的真值或 M 中的假值，ϕ 或 ¬ϕ 是 Γ 的（语义）逻辑推理的结果。

如果 ϕ 是我们上面定义的二阶句子，我们将 Mod(ϕ)定义为类{M:M⊨ϕ}。如果 ϕ 能够表征 M 的同构性，那么在同构性上，

Mod(ϕ)={M}。

在 20 世纪的第一个季度，用二阶句子公理化数学结构的项目非常成功，以至于卡尔纳普甚至提出每个数学结构都可以通过其二阶理论来确定其同构性。对于大小为 2ω 及以上的所有模型，由于基数的原因，这显然是不可能的。与非同构模型的数量相比，二阶理论的数量太少了。然而，对于有限模型，卡尔纳普的假设是显然成立的，并且对于可数模型来说也不完全没有道理。事实上，Ajtai（1979）证明了，如果 ZFC 本身是一致的，那么任何两个满足相同二阶句子的可数词汇结构是同构的。Ajtai 还证明了，如果 ZFC 本身是一致的，那么存在两个满足相同二阶句子的可数词汇结构，但它们不是同构的。因此，卡尔纳普的猜想（对于可数模型）与 ZFC 无关。

Solovay 在 FOM（2006 年其他互联网资源）中发表了一篇文章，其中他展示了相关陈述，即每个完全的二阶句子 θ 是范畴的，与 ZFC 是独立的。

在重要情况下，Henkin 结构存在一种强形式的范畴性，并且与完全 Henkin 模型的常规概念一致。它建立在二阶逻辑表达其自身范畴性的显著能力之上。两个结构（M，R）和（M'，R'）的同构（M，R）≅（M'，R'），其中谓词 R 和 R'是二元的，可以用二阶逻辑表示如下，令 A =（A，M，M'，R，R'），其中 A 是包含 M∪M'的任意集合，M = UA，M' = U'A，R = PA 和 R' = P'A。现在

（M，R）≅（M'，R'）⟺A⊨ISOM（U，P，U'，P'），

其中 ISOM(U,P,U′,P′)是句子

∃F [∀x(U(x)→U′(F(x)))∧∀x∃y(U′(x)→(U(y)∧x=F(y)))∧∀x∀y((U(x)∧U(y))→[(F(x)=F(y)→x=y)∧(P(x,y)↔P′(F(x),F(y)))])].

这表明具有二元谓词符号 P 的句子 θ(P)的范畴性可以等价地重新定义为 [18]，让 CATEG(θ(P))成为句子

∀P∀P′∀U∀U′((θ(P)U∧θ(P′)U′)→ISOM(U,P,U′,P′)),

as

(12)⊨CATEG(θ(P)).

实际上，这是 Tarski 在 1956 年（第 387 页）中定义的范畴性。这使我们得出以下定义：

定义 15 如果 θ(P)在内部是范畴性的，则我们称其为内部范畴性。

(13)⊢CATEG(θ(P))。

内部范畴性也可以称为可证明的范畴性。短语“内部范畴性”是在 Walmsley（2002）的算术背景下引入的。它在 Väänänen（2012）中更普遍地被提倡，并在 Väänänen 和 Wang（2015）中有更多细节。关于这个概念的最近讨论，请参考 Button 和 Walsh（2016）。

注意，（13）比（12）更强，因为可证明的句子肯定是有效的。由于完备性定理，我们可以将（13）重写为

对于所有 Henkin 模型（A，G），（14）（A，G）⊨CATEG（θ（P））。

因此，内部范畴性意味着不仅对于普通模型，即完全 Henkin 模型，而且对于任意 Henkin 模型都是范畴性的。请注意，范畴性是一个元理论概念，因为它涉及到二阶逻辑的语义。在 CATEG(θ(P))中，θ(P)的范畴性是用二阶逻辑的语言书写的。也就是说，尽管范畴性是一个元理论概念，但它是用目标语言书写的。可以问，这是否导致了一个不同的概念？无论如何，当通过在元理论中考虑其语义来揭示 CATEG(θ(P))的含义时，其含义与我们赋予 θ(P)的范畴性的含义相同。在内部范畴性的概念中，我们利用了这种情况，通过从语义含义转换为证明论含义。我们坚持认为 CATEG(θ(P))是（不仅有效而且）可证明的。证明论比语义学需要更少的元理论。我们可以通过使用数字对句子和证明进行编码，如哥德尔在他的不完全性定理的证明中所做的那样，甚至在数论中研究二阶句子的可证明性。当然，完备性定理将我们带回到语义学。

要验证二阶句子的范畴性，必须以一种基本上需要集合论的方式遍历无限结构。内部范畴性的情况不同。要验证二阶句子的内部范畴性，只需产生一个证明。因此，存在明显的差异。而且，内部范畴性比范畴性更强。因此，如果能够建立内部范畴性，建立范畴性将是愚蠢的。幸运的是，经典的范畴句子的例子都是内部范畴的：

定理 16（Väänänen & Wang 2015）：表征结构（N，<）和（R，<，+，⋅，0，1）的接收的二阶句子是内部范畴的。

内部分类概念提供了完全语义学和亨金语义学之间的桥梁。它在两种情况下都以相同的方式工作，并且表明完全语义学是亨金语义学的极限情况，但在分类性方面并不垄断。

11. 第一阶和第二阶之间的逻辑

第一阶逻辑和第二阶逻辑在某种意义上是两个相反的极端。它们之间有许多逻辑，即在适当地扩展第一阶逻辑的同时，又适当地包含在第二阶逻辑中的逻辑。一个例子是通过被称为亨金量词的广义量词扩展第一阶逻辑：

(∀x∃y∀u∃v)ϕ(x,y,u,v,z1,…,zn)

其含义为

∃f∃g∀x∀uϕ(x,f(x),u,g(u),z1,…,zn).

通过 Henkin 量词扩展的一阶逻辑的扩展 L(H)与二阶逻辑几乎相同：它们具有相同的 Δ-扩展（Krynicki＆Lachlan 1979）[19]。

等势性或 Härtig 量词

Ixyϕ(x,z1,…,zn)ψ(x,z1,…,zn)

具有“存在与 ϕ(x,z1,…,zn)满足的元素 x 的数量相同，与 ψ(y,z1,…,zn)满足的元素 y 的数量相同”的含义，即，

∃f∀x [(ϕ(x,z1,…,zn)↔ψ(f(x),z1,…,zn))∧∀x∀y(f(x)=f(y)→x=y)∧∀y∃x(ψ(y,z1,…,zn)→f(x)=y)]

通过 Härtig 量词扩展的一阶逻辑的扩展 L(I)比二阶逻辑要弱 [20]，因为它的 Löwenheim 数可以小于 2ω，但如果 V=L，则与二阶逻辑是 Δ 等价的（Väänänen 1980）。

这里有一些明显是二阶可定义的其他广义量词：

Q0xϕ(x,z1,…,zn)⟺∃X(|X|≥ℵ0∧∀x∈Xϕ(x,z1,…,zn))Q1xϕ(x,z1,…,zn)⟺∃X(|X|≥ℵ1∧∀x∈Xϕ(x,z1,…,zn))QMM1xyϕ(x,y,z1,…,zn)⟺∃X(|X|≥ℵ1∧∀x,y∈Xϕ(x,y,z1,…,zn))Qcofωxyϕ(x,y,z1,…,zn)⟺{(x,y):ϕ(x,y,z1,…,zn)}

是一个具有共极性 ω 的线性序

在弱二阶逻辑中，我们没有函数变量，关系变量仅范围在有限关系上。由此产生的逻辑在许多方面类似于通过广义量词 Q0 扩展一阶逻辑。限制二阶逻辑能力的另一种方法是：假设 ψ 是一个带有 n 元关系变量 X 和无非逻辑符号的一阶公式。对于无穷集合 A，我们定义 A⊨sQψXϕ 当且仅当存在一个关系 P⊆Mn，使得 A⊨s(P/X)ϕ∧ψ。量词 Qψ 允许对满足 ψ 的关系进行二阶量化。如果 ψ 是 ∀x(x=x)，我们得到通常的二阶量词，记作 QII。如果此外 n=1，我们得到单调二阶量词，记作 Qmon。如果 n=1 且 ψ 表示 X 是一个单例集，我们得到通常的一阶量词，现在记作 QI。最后，如果 ψ 表示 X 是模型的排列图，我们将此量词记作 Q1−1。令人惊讶的是，通过适当的可解释性概念，量词 QI、Qmon、Q1−1 和 QII 是形式为 Qψ 的二阶量词中，唯一的、在双解释下等价的量词（Shelah 1973）。

12. 高阶逻辑与类型理论相对比

有许多方法可以进一步扩展二阶逻辑。最明显的是三阶、四阶等高阶逻辑。这个一般原则，已经被塔斯基（1933 [1956]）所认可，即在高阶逻辑中可以形式化低阶逻辑的语义——定义真理。因此，使用高阶逻辑肯定会获得更强的表达能力。让我们以数论为例。使用一阶逻辑，我们可以表达“n 是一个质数”的属性和命题，如“存在无限多个质数”，费马大定理和哥德巴赫猜想。自然数的一阶属性属于一个称为算术层次结构的自然层次，其级别表示为 Σ0n 和 Π0n。使用二阶逻辑，我们可以讨论自然数集合的属性，或者换句话说，实数的属性。特别地，我们可以定义有理数。实数上的连续函数由其在有理数上的取值决定。此外，开集由其包含的有理点决定。利用这些观察，我们可以讨论实数的连续函数和开集。微积分中的基本事实，如波尔查诺定理，即“如果一个连续函数在一个区间内有相反符号的值，那么它在该区间内有一个根”，可以用自然数的结构（N,+,⋅）上的二阶逻辑来表达。自然数的二阶属性属于一个称为分析层次结构的自然层次，其级别表示为 Σ1n 和 Π1n。使用三阶逻辑，我们可以讨论实数集合。我们可以用三阶逻辑写出连续统假设，并提出一个困难的问题，即模型（N,+,⋅）是否满足这个句子。自然数的三阶属性再次具有一个自然层次结构，其级别表示为 Σ2n 和 Π2n。

很明显，如果我们保持一个基本模型，比如(N,+,⋅)不变，并且转向更高阶的逻辑，我们可以表达更复杂的概念和命题。然而，对于 N1=(N,+,⋅)来说，三阶逻辑只不过是二阶逻辑的一种解释。

N1=(N,+,⋅)

只不过是二阶逻辑的一种解释。

N2=(P(N),E,N,+,⋅),

其中 E⊆N×P(N)是关系 nEr⟺n∈r，这只不过是对一阶逻辑的再次解释，

N3=(P(P(N))),E′,P(N),E,N,+,⋅),

其中 E'⊆P(N)×P(P(N)是关系 rE'X⟺r∈X。此外，N1 上的二阶逻辑不过是 N2 上的一阶逻辑。当这种思路被推到极限时，我们可以看到集合的累积层次上的一阶逻辑涵盖了层次结构中任何个别层次 Vα 上的高阶逻辑。从某种意义上说，集合的累积层次上的一阶逻辑是对 N1 的非常非常高阶逻辑。

N2 从 N1 产生的方式与 N3 从 N2 产生的方式有明显的相似之处。在这两种情况下，我们只是在模型已有的基础上添加了一个幂集构造。仅仅二阶逻辑对幂集非常好，正如我们在 §5.3 中所看到的。这导致了所有高阶逻辑（任何有限阶数和一定程度上的无限阶数）从二阶逻辑开始具有图灵等价的决策问题和相同的 Hanf 和 Löwenheim 数（见 §4）。因此，尽管高于二阶逻辑严格来说比二阶逻辑更强大，但在表达能力的常规标准下看不出任何差异。

类型理论是一种对高阶逻辑的系统化方法。变量被赋予类型，就像在二阶逻辑中我们有个体类型、关系类型和函数类型的变量一样。在高阶逻辑中，对于任何较低类型的对象之间的关系以及将较低类型的对象映射到较低类型的对象的函数，有变量是有意义的。在集合论中，对象具有一个等级。集合的元素比集合本身的等级低。然而，集合论中的等级与类型理论中的类型之间的区别在于，在集合论中，当集合已知时可以计算等级，而在类型理论中，可以从对象是值的变量的类型中看出对象的类型。从某种意义上说，类型理论从语法上为每个考虑的对象强加了一个类型，而在集合论中，集合的等级由语义给出。可以说，在 20 世纪 30 年代之后，集合论因其更简单的语法和语义而在类型理论之上占据主导地位。另一方面，类型理论在计算机科学中得到了应用，特别是在编程语言理论中（参见 SEP 关于类型理论的条目）。

13. 数学基础

数学可以基于集合论。这意味着数学对象被构造为集合，并且它们的属性是从集合论公理中推导出来的。集合论背后的直观非正式图像是，存在一组集合的累积层次 Vα（α 是一个序数），而公理旨在描述这些集合的基本属性。这种基于集合论的数学基础在工作数学家中得到了广泛接受。有关更多详细信息，请参阅 SEP 关于集合论的条目。集合论的替代方案至少包括范畴论、构造性数学和二阶逻辑。

如果一个人试图以逻辑学家的方式来追随数学家在他们的研究中使用的语言，那么他不禁会看到他们非常自由地使用二阶概念。例如，归纳公理无疑是数学家以(1)所描述的二阶形式使用的。在他们的自然语言中，数学家毫不犹豫地使用高阶概念，甚至不一定（需要）知道其中的区别。

作为数学基础的二阶逻辑关注的是数学结构而不是数学“对象”，就像集合论一样。原则上，每个结构都有基于结构的特殊特征的“基础”。二阶逻辑的作用是为此提供一个共同的框架。在结构上，二阶逻辑的直观非正式图像是存在一个个体的域 A，然后与 A 相关联的所有 n 元关系的单独域，其中 n∈N，并且与 A 相关联的所有 n 元函数的单独域，其中 n∈N。与集合论的非正式图像相比，我们只有子集、关系和函数的域，而没有集合的迭代，如集合的集合、集合的集合的集合等等。因此，二阶逻辑背后的直观图像比集合论背后的图像更简单。特别是，没有关于所有序数的超限迭代。在数学中使用的大多数结构 A 都有一个二阶特征 θA，参见第 10 节。证明这些结构的（二阶）性质 ϕ 意味着从 θA 推导出 ϕ。关于这种推导是否应该是使用某个（不完全的）二阶逻辑公理系统的句法（形式）推导，还是应该是语义推导（形式为“假设的每个模型都是结论的模型”），人们的意见不一。对于一个工作中的数学家来说，这没有太大的区别，可能更倾向于语义推导。

假设一个数学家想要说服某人关于 Bolzano 定理的真实性：“如果实数上的连续函数在一个区间内既有负值又有正值，那么它在该区间内有一个根”。他们会从实数的二阶有序域开始。这是因为该领域的二阶公理化是范畴论的，所以（被认为）清楚地知道这意味着什么。然后，他们会取一个在该域上的任意连续函数 f，使得它在一个固定区间（a，b）内具有相反符号的值。这是因为二阶逻辑具有函数变量，所以这也是清楚的。设 c，d∈（a，b），使得 f（c）<0 且 f（d）> 0。不失一般性，假设 c<d。设 X={e∈（a，b）：f（e）<0}。由于我们对域的子集有关系变量，我们可以将 X 简单地看作这样一个关系变量的值。很明显，X 存在，但是我们事先可能对 X 施加了矛盾的条件（例如，X={e:e∉X}），然后我们就不能声称它存在。然而，在这种情况下，包容公理模式意味着 X 存在。显然，X≠∅ 且 X 由 d 上界。实数域的二阶公理之一是，每个非空的上界有界集合都有一个上确界。因此，我们可以让 z 成为 X 的上确界。现在，根据连续函数的基本性质，得出 f（z）=0。

在上述证明中，很难判断它是从公理中的句法推导还是语义论证。表面上看起来像是一个语义论证。但是，每一步都可以从公理中推导出来，所以它可以被认为是一个句法推导的简写版本。

基于包含公理模式和选择公理的二阶逻辑中的句法推导与集合论中的句法推导非常相似。在这两种情况下，工作中的数学家不会写出所有论证的细节，而是会使用速记符号。在二阶逻辑和集合论中，我们都可以将证明解释为句法形式证明的速记版本或语义证明。一阶逻辑通过完备性定理得到满足，借助该定理，语义证明可以转化为句法形式证明。由于完备性定理使用了一阶结构的概念，从公理中证明的句子在所有模型中都是真的，包括可数模型和非标准模型。它们在集合的直观模型中是真的吗？根据反射定理，这样的句子在所有集合的类中都是真的，但由于直观模型是非正式的，我们无法证明所有集合的类与直观模型相同。

另一方面，为了使完备性定理适用，语义论证必须适用于我们使用的集合论模型。这意味着集合论中的语义论证不应使用集合论模型的个别属性，除非它们是 ZFC 所有模型的普遍一阶属性。实际上，这意味着如果使用了 CH、◊、2ℵ0=ℵ2 等属性，则需要单独提及作为假设。模型的非一阶属性不能被使用，否则无法使用完备性定理。然而，有时会使用非一阶属性。例如，我们可能有一个论证，即 ZFC 的每个可数模型都满足 ϕ。但是，根据下降型 Löwenheim-Skolem 定理，ZFC 的每个模型都满足 ϕ。因此，我们已经成功消除了模型可数性的非一阶假设。

二阶逻辑如果使用亨金模型，则满足完备性定理。因此，二阶逻辑中的语义论证可以转化为句法形式的证明，但与集合论一样，语义论证必须在所有亨金模型中有效，而不仅仅在所有完全亨金模型中有效。因此，与集合论类似，语义论证不能使用所有亨金模型共享的亨金模型的特性。特别是，不能假设完全性（见 §9.1），因为在一般模型中它不是二阶属性。当放弃完全性时，分类性会发生什么变化？我们仍然有内部分类性，因此只要确保我们在一个模型内工作，就可以在证明中使用分类性。确保这一点的一种确定的方法是将一切都基于公理，包括包含公理模式和选择公理。

当二阶逻辑被用作数学的基础时，可能会出现需要第三阶逻辑的情况。例如，拓扑通常被定义为一组集合，因此是一个第三阶对象。在二阶逻辑的精神中，当需要时，可以简单地包括第三（或更高）阶逻辑。自然地，必须假设包含公理模式和选择公理以支持第三阶量词。

我们在本条目中花了相当多的篇幅来讨论二阶逻辑描述结构的能力（见 §7.1）。简而言之，如果一个结构具有数学上的兴趣，那么它就是二阶可描述的。通过选择公理构造的结构可能逃脱二阶可描述性。但是，二阶逻辑证明结构的存在的能力是什么？包括包含公理和选择公理在内的公理可以在一个元素的域中满足。因此，我们无法从公理中证明存在任何大小大于 1 的结构。这削弱了奎因对二阶逻辑的描述为“羊皮中的集合论”（1970 年，第 5 章的章节标题），这可能意味着二阶逻辑的本体论承诺与集合论的本体论承诺处于同一水平。

或许二阶逻辑的哲学是，如果一个结构可以被描述，那么它存在，回应了希尔伯特的形式主义哲学。然而，即使在这个意义上，我们仍然需要知道描述性句子 θA 是一致的。一个微不足道的方法是观察到 A 本身肯定满足 θA，但这显然是在回避问题。然而，这就是希尔伯特为实数的公理的一致性辩护的方式（1900 年）。如果 A=(N,+,⋅)，那么需要一个无穷公理，它说一个域的真子集与整个域具有相同的基数。结合包含公理模式，A 的存在就可以得到。对于(R,+,⋅,0,1)来说，这还不够，我们需要一个更强的无穷公理，例如存在一个满足完备性公理的稠密序：每个有界的非空集合都有一个上确界。当我们从一个结构转移到一个更大的结构时，似乎不可避免地需要做一个大的假设。这样的假设在 Väänänen（2012）中被称为大域假设。在集合论中，这个方面在一开始就通过假设幂集公理和替换公理来处理，这两者一起确保了有足够大的集合。在二阶逻辑中，我们必须假设新的大域假设，随着我们的推进而不断增加。这可以看作是一个缺点，需要一直做出新的假设。另一方面，这可以看作是一个优点，在真正需要之前不必做出过于雄心勃勃的假设。

14. 二阶算术

由于实数在数学中的核心地位，自然数的二阶理论，即二阶算术（Simpson 1999 [2009]），记作 Z2，是一个重要的基础理论。它比（一阶）皮亚诺算术更强，但比集合论更弱。它有个体变量，被认为是自然数，也有被认为是实数的自然数集合的变量。此外，还有用于个体上的算术运算的+和 ×。作为公理，Z2 有一些关于+和 × 的相当明显的公理，归纳公理（1），以及二阶逻辑的公理，包括包含原则（10）。在 Z2 中可以推导出相当多的数学。有关详细信息，请参阅 Simpson（1999 [2009]）。从某种意义上说，Z2 是二阶逻辑的一个巨大成功案例。

反向数学使用 Z2 来确定数学中著名定理所依赖的确切公理。在教科书中，这些定理可能是在非正式的集合论中证明的，但在每种情况下实际上需要多少集合论呢？例如，我们可以问从哪个最弱的公理集合中可以证明波尔查诺-魏尔斯特拉斯定理 [21]？需要多少集合论、包含原则、选择、归纳等？由于 Z2 是许多数学定理的自然且足够的环境，它是回答反向数学计划提出的问题的适当框架。反向数学中主要（但不是唯一）的区别在于在证明这个或那个数学结果时需要多少包含原则。特别是，算术和 Π11-包含原则的作用得到了澄清。基本的实数理论可以仅基于算术包含原则来发展，但依赖于可数序数概念的证明需要 Π11-包含原则。再次，请参阅 Simpson（1999 [2009]）以获取详细信息。

15. 二阶集合论

到目前为止，我们将集合论（ZFC）视为一阶理论。然而，当策梅洛（1930 年）引入构成现代 ZFC 公理系统的公理时，他使用了二阶逻辑来表述这些公理。特别地，他的分离公理是

∀x∀X∃y∀z(z∈Y↔(z∈x∧X(z)))

而替换公理是

∀x∀F∃y∀z(z∈y↔∃u(u∈x∧z=F(u))).

二阶 ZFC，ZFC2，简单地是将接受的一阶 ZFC 中的分离模式替换为上述单一的分离公理，并将替换模式替换为上述单一的替换公理。因此，ZFC2 是一个有限的公理系统。泽尔梅洛证明了 ZFC2 的模型在同构意义下具有形式(Vκ,∈)，其中 κ 是（强）不可及的>ω。

Kreisel（1967）指出，二阶集合论在某种意义上决定了连续统假设（CH），即使我们不知道决策的方向。更确切地说，ZFC2⊨CH 或 ZFC2⊨¬CH，因为当且仅当对于不可达的 κ，Vκ⊨CH 成立，即当且仅当 ZFC2⊨CH 成立。当然，我们也可以在一阶集合论中表达 CH，所以情况与一阶集合论并没有真正的不同。许多集合论学家认为集合的概念足够明确，即使 ZFC 不能决定 CH，最终也能决定 CH。同样，我们可以主张，二阶语义的概念足够明确，即使当前的二阶逻辑公理不能决定 CH。

问题是，为什么我们不使用二阶集合论 ZFC2 作为二阶逻辑的元理论，就像 Shapiro（1991）建议的那样。实际上，我们可以使用它。然而，问题可能会出现，我们的元理论的语义是什么？原则上，这类问题可能会导致无限回归。通过使用一阶集合论作为元理论，关于元理论语义的问题简单地成为关于一阶逻辑语义的问题。我们在第 6 节中指出，一阶逻辑的语义相对于 ZFC 是绝对的。这给了我们一些保证，我们不需要继续问元理论是什么。

16. 有限模型论

二十世纪上半叶数理逻辑的兴起与对自然数和实数的无限结构的不同理解方法交织在一起。随着二十世纪下半叶计算机科学的出现，逻辑学经历了一次重生的过程。计算和数据库的概念都强调了理解有限/无限区别的需要，而不是新的有限度度量。例如，问题是否可以在多项式时间内决定，挑战了已经发展完善的有限时间内可以决定什么的理论。有限关系结构和数据库之间的类比导致了有限模型理论的出现。关于这方面的良好综述，请参考 Fagin（1993）。

在有限模型的背景下，二阶逻辑不像在无限模型的背景下那样遭受哲学问题的困扰。它只是众多语言中的一种。早期的成功之一是 Fagin（1974）的结果，即在存在性二阶逻辑中可定义的模型类，即 Σ11-片段，正是 NP 类，即可以由在多项式时间内运行的非确定性图灵机识别的模型，其时间与模型的编码大小成多项式关系。NP 类是否封闭于补集的问题是众所周知的未解问题。从二阶逻辑的角度来看，这是令人惊讶的，因为在所有模型中，无论是有限的还是无限的，Σ11 当然不封闭于补集。例如，无限模型的类（在空词汇中）是 Σ11 但不是 Π11。此外，良序类是 Π11 但不是 Σ11。因此，关于有限模型上的二阶逻辑的以下早期结果是非凡的。这里的 MON-Σ11 指的是单调二阶逻辑中的 Σ11，类似地，MON-Π11。

定理 17（Fagin 1975）：图的连通性在 MON-Σ11 中不可定义。因此，MON-Σ11≠MON-Π11。

这随后被扩展到具有特定其他结构的图形上，参见 Fagin，Stockmeyer 和 Vardi（1995）。证明使用 Ehrenfeucht-Fraïssé 游戏（见 §3.1）及其扩展。

让 Σ11,m 表示 Σ11 公式 ∃X1…∃Xkϕ 的类别，其中绑定的二阶变量 Xi 最多为 m 元，并且 ϕ 是一阶的。类似地，Π11,m 和 Δ11,m。

定理 18（Ajtai 1983）有限结构（A，R）的性质，其中 R 是 n+1 元的，|R|为偶数，是 Δ11,n+1 但不是 Σ11,n 或 Π11,n。

这个高度非平凡的定理是对有限结构上二阶逻辑研究的基石之一。我们不知道在有限结构上 Δ11 是否与 Σ11 不同，但上述定理给出了一个基于元数的 Δ11 内部的层次结果。

Bibliography

  • Ajtai, M., 1979, “Isomorphism and Higher Order Equivalence”, Annals of Mathematical Logic, 16(3): 181–203. doi:10.1016/0003-4843(79)90001-9

  • –––, 1983, “Σ11-Formulae on Finite Structures”, Annals of Pure and Applied Logic, 24(1): 1–48. doi:10.1016/0168-0072(83)90038-6

  • Asser, Günter, 1981, Einführung in Die Mathematische Logik: Teil Ill: Prädikatenlogik Höherer Stufe, Thun: Verlag Harri Deutsch.

  • Barwise, K. Jon, 1972a, “Absolute Logics and L∞ω”, Annals of Mathematical Logic, 4(3): 309–340. doi:10.1016/0003-4843(72)90002-2

  • –––, 1972b, “The Hanf Number of Second Order Logic”, Journal of Symbolic Logic, 37(3): 588–594. doi:10.2307/2272748

  • Büchi, J. Richard, 1962, “On a Decision Method in Restricted Second Order Arithmetic”, in Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress, Ernest Nagel, Patrick Suppes, and Alfred Tarski (eds.), Stanford, CA: Stanford University Press, 1–11.

  • –––, 1973, “The Monadic Second Order Theory of ωi”, in Decidable Theories II: The Monadic Second Order Theory of All Countable Ordinals, by J. Richard Büchi and Dirk Siefkes, edited by G. H. Müller and D. Siefkes, (Lecture Notes in Mathematics 328), Berlin, Heidelberg: Springer Berlin Heidelberg, 1–127. doi:10.1007/BFb0082721

  • Buss, Samuel R. (ed.), 1998, Handbook of Proof Theory, (Studies in Logic and the Foundations of Mathematics 137), New York: Elsevier.

  • Button, Tim and Sean Walsh, 2016, “Structure and Categoricity: Determinacy of Reference and Truth Value in the Philosophy of Mathematics”, Philosophia Mathematica, 24(3): 283–307. doi:10.1093/philmat/nkw007

  • Church, Alonzo, 1956, Introduction to Mathematical Logic, volume 1, Revised and enlarged edition, (Princeton Mathematical Series 17), Princeton, NJ: Princeton University Press.

  • Cohen, Paul J., 1966, Set Theory and the Continuum Hypothesis, New York-Amsterdam: W. A. Benjamin.

  • Craig, William, 1965, “Satisfaction for n-th order languages defined in n-th order languages”, Journal of Symbolic Logic, 30: 13–25.

  • de la Cruz, Omar, 2002, “Finiteness and Choice”, Fundamenta Mathematicae, 173(1): 57–76. doi:10.4064/fm173-1-4

  • Durand, Arnaud, Ronald Fagin, and Bernd Loescher, 1998, “Spectra with Only Unary Function Symbols”, in Computer Science Logic, Mogens Nielsen and Wolfgang Thomas (eds.), (Lecture Notes in Computer Science 1414), Berlin, Heidelberg: Springer Berlin Heidelberg, 189–202. doi:10.1007/BFb0028015

  • Durand, Arnaud, Neil D. Jones, Johann A. Makowsky, and Malika More, 2012, “Fifty Years of the Spectrum Problem: Survey and New Results”, The Bulletin of Symbolic Logic, 18(4): 505–553. doi:10.2178/bsl.1804020

  • Elgot, Calvin C., 1961, “Decision Problems of Finite Automata Design and Related Arithmetics”, Transactions of the American Mathematical Society, 98(1): 21–21. doi:10.1090/S0002-9947-1961-0139530-9

  • Fagin, Ronald, 1974, “Generalized First-Order Spectra and Polynomial-Time Recognizable Sets”, in Complexity of Computation, Richard M. Karp (ed.), (SIAM-AMS Proceedings 7), Providence, RI: American Mathematical Society, 43–73.

  • –––, 1975, “Monadic Generalized Spectra”, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 21(1): 89–96. doi:10.1002/malq.19750210112

  • –––, 1993, “Finite-Model Theory—a Personal Perspective”, Theoretical Computer Science, 116(1): 3–31. doi:10.1016/0304-3975(93)90218-I

  • Fagin, Ronald, Larry J. Stockmeyer, and Moshe Y. Vardi, 1995, “On Monadic NP vs Monadic Co-NP”, Information and Computation, 120(1): 78–92. doi:10.1006/inco.1995.1100

  • Feferman, Solomon, 1999, “Does Mathematics Need New Axioms?”, The American Mathematical Monthly, 106(2): 99–111. doi:10.1080/00029890.1999.12005017

  • Feferman, Solomon and Georg Kreisel, 1966, “Persistent and Invariant Formulas Relative to Theories of Higher Order”, Bulletin of the American Mathematical Society, 72(3): 480–486. doi:10.1090/S0002-9904-1966-11507-0

  • Frege, Gottlob, 1879, Begriffsschrift: Eine Der Arithmetischen Nachgebildete Formelsprache Des Reinen Denkens, Halle.

  • –––, 1884, Die Grundlagen Der Arithmetik, Breslau: Verlage Wilhelm Koebner.

  • Garland, Stephen J., 1974, “Second-Order Cardinal Characterizability”, in Axiomatic Set Theory, Part 2, T. J. Jech (ed.), (Proceedings of Symposia in Pure Mathematics, 13.2), Providence, RI: American Math Society, 127–146. [Garland 1974 available online]

  • Gaßner, Christine, 1994, “The Axiom of Choice in Second-Order Predicate Logic”, Mathematical Logic Quarterly, 40(4): 533–546. doi:10.1002/malq.19940400410

  • Gödel, Kurt, 1931 [1986], “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für Mathematik und Physik, 38(1): 173–198. Reprinted and translated as “On Formally Undecidable Propositions of Principia Mathematica and Related Systems” in Gödel 1986: 144–195. doi:10.1007/BF01700692

  • –––, 1936 [1986], “Über Die Länge von Beweisen”, Ergebnisse Eirtes Mathematischen Kolloquiums, 7: 23–24. Reprinted and translated as “On the Length of Proofs” in Gödel 1986: 396–399.

  • –––, 1939 [1990], “Consistency-Proof for the Generalized Continuum-Hypothesis”, Proceedings of the National Academy of Sciences, 25(4): 220–224. Reprinted in Gödel 1990: 28–32. doi:10.1073/pnas.25.4.220

  • –––, 1986, Collected Works, Volume 1: Publications 1929-1936, Solomon Feferman (ed.), New York: Oxford University Press.

  • –––, 1990, Collected Works, Volume 2: Publications 1938-1974, Solomon Feferman (ed.), New York: Oxford University Press.

  • Gurevich, Yuri, 1985, “Monadic Second-Order Theories”, in Model-Theoretic Logics, Jon Barwise and Sol Feferman (eds.) (Perspectives in Logic), New York: Springer-Verlag, 479–506. doi:10.1017/9781316717158.019

  • Gurevich, Yuri, Menachem Magidor, and Saharon Shelah, 1983, “The Monadic Theory of ω2”, Journal of Symbolic Logic, 48(2): 387–398. doi:10.2307/2273556

  • Hasenjaeger, Gisbert, 1961, “Unabhängigkeitsbeweise in Mengenlehre Und Stufenlogik Der Modelle.”, Jahresbericht Der Deutschen Mathematiker-Vereinigung, 63: 141–162.

  • Hellman, Geoffrey, 2001, “Three Varieties of Mathematical Structuralism†”, Philosophia Mathematica, 9(2): 184–211. doi:10.1093/philmat/9.2.184

  • Henkin, Leon, 1950, “Completeness in the Theory of Types”, Journal of Symbolic Logic, 15(2): 81–91. doi:10.2307/2266967

  • Herbrand, Jacques, 1930, Recherches sur la théorie de la démonstration, (Thèses de l’entre-deux-guerres 110), L’Université de Paris. [Herbrand 1930 available online]

  • Hilbert, David, 1900, “Über Den Zahlbegriff.”, Jahresbericht Der Deutschen Mathematiker-Vereinigung, 8: 180–183.

  • Hilbert, David and William Ackermann, 1928, Grundzüge Der Theoretischen Logik, (Grundlehren Der Mathematischen Wissenschaften in Einzeldarstellungen Mit Besonderer Berücksichtigung Der Anwendungsgebiete 27), Berlin: J. Springer.

  • –––, 1938, Grundzüge Der Theoretischen Logik, second edition, Berlin: Springer. doi:10.1007/978-3-662-41928-1

  • Hintikka, K. Jaakko J., 1955, “Reductions in the Theory of Types”, Acta Philosophica Fennica, 8: 57–115.

  • Hyttinen, Tapani, Kaisa Kangas, and Jouko Vaananen, 2013, “On Second-Order Characterizability”, Logic Journal of IGPL, 21(5): 767–787. doi:10.1093/jigpal/jzs047

  • Jones, Neil D. and Alan L. Selman, 1974, “Turing Machines and the Spectra of First-Order Formulas”, Journal of Symbolic Logic, 39(1): 139–150. doi:10.2307/2272354

  • Krawczyk, A. and W. Marek, 1977, “On the Rules of Proof Generated by Hierarchies”, in Set Theory and Hierarchy Theory V, Alistair Lachlan, Marian Srebrny, and Andrzej Zarach (eds.) (Lecture Notes in Mathematics 619), Berlin: Springer Berlin Heidelberg, 227–239. doi:10.1007/BFb0067654

  • Kreisel, Georg, 1967, “Informal Rigour and Completeness Proofs”, in Problems in the Philosophy of Mathematics, Imre Lakatos (ed.), (Studies in Logic and the Foundations of Mathematics 47), Amsterdam: North-Holland, 138–186. doi:10.1016/S0049-237X(08)71525-8

  • Krynicki, Michał and Alistair H. Lachlan, 1979, “On the Semantics of the Henkin Quantifier”, Journal of Symbolic Logic, 44(2): 184–200. doi:10.2307/2273726

  • Kunen, Kenneth (ed.), 1980, Set Theory: An Introduction to Independence Proofs, (Studies in Logic and the Foundations of Mathematics 102), Amsterdam: North-Holland.

  • Lévy, Azriel, 1965, A Hierarchy of Formulas in Set Theory, (Memoirs of the American Mathematical Society 57), Providence, RI: American Mathematical Society.

  • Lindenbaum, Adolf and Andrzej Mostowski, 1938, “Über Die Unabhängigkeit Des Auswahlaxioms Und Einiger Seiner Folgerungen”, Sprawozdania z Posiedzeń Towarzystwa Naukowego Warszawskiego, Wydział III Nauk Matematyczno-Fizycznych (Comptes-Rendus Des Séances de La Société Des Sciences et Des Lettres de Varsovie,Classe III), 31: 27–32.

  • Löwenheim, Leopold, 1915, “Über Möglichkeiten im Relativkalkül”, Mathematische Annalen, 76(4): 447–470. doi:10.1007/BF01458217

  • Lyndon, Roger C., 1959, “An Interpolation Theorem in the Predicate Calculus.”, Pacific Journal of Mathematics, 9(1): 129–142.

  • Magidor, M., 1971, “On the Role of Supercompact and Extendible Cardinals in Logic”, Israel Journal of Mathematics, 10(2): 147–157. doi:10.1007/BF02771565

  • Makowsky, J.A., Saharon Shelah, and Jonathan Stavi, 1976, “δ-Logics and Generalized Quantifiers”, Annals of Mathematical Logic, 10(2): 155–192. doi:10.1016/0003-4843(76)90021-8

  • Manzano, María, 1996, Extensions of First Order Logic, (Cambridge Tracts in Theoretical Computer Science 19), Cambridge: Cambridge University Press.

  • Montague, Richard, 1963, “Reductions of Higher-Order Logic”, in The Theory of Models: Proceedings of the 1963 International Symposium at Berkeley, J.W. Addison, Leon Henkin, and Alfred Tarski (eds.), Amsterdam: North-Holland, 251–264. doi:10.1016/B978-0-7204-2233-7.50030-7

  • Moore, Gregory H., 1988, “The Emergence of First-Order Logic”, in History and Philosophy of Modern Mathematics, (Minnesota Studies in the Philosophy of Science 11), Minneapolis, MN: University of Minnesota Press, 95–135.

  • Mostowski, Andrzej, 1938, “O niezależności definicji skończoności w systemie logiki” (“On the independence of definitions of finiteness in a system of logic”), Dodatek do Rocznika Towarzystwa. Matematycznego, XI: 1–54; English translation in Mostowski 1979.

  • Mostowski, Andrzej, 1949, “An Undecidable Arithmetical Statement”, Fundamenta Mathematicae, 36(1): 143–164.

  • Mostowski, Andrzej, 1979, Foundational Studies. Selected works (Volume II), Studies in Logic and the Foundations of Mathematics: Volume 93, Amsterdam-New York: North-Holland Publishing Co.; PWN-Polish Scientific Publishers, Warsaw, 1979, edited by Kazimierz Kuratowski, Wiktor Marek, Leszek Pacholski, Helena Rasiowa, Czesław Ryll-Nardzewski and Paweł Zbierski.

  • Parsons, Charles, 1990, “The Structuralist View of Mathematical Objects”, Synthese, 84(3): 303–346. doi:10.1007/BF00485186

  • Quine, W. V. O., 1970, Philosophy of Logic, Cambridge, MA: Harvard University Press.

  • Rabin, Michael O., 1968, “Decidability of Second-Order Theories and Automata on Infinite Trees”, Bulletin of the American Mathematical Society, 74(5): 1025–1030. doi:10.1090/S0002-9904-1968-12122-6

  • Rabin, Michael O. and Dana Scott, 1959, “Finite Automata and Their Decision Problems”, IBM Journal of Research and Development, 3(2): 114–125. doi:10.1147/rd.32.0114

  • Resnik, Michael D., 1988, “Second-Order Logic Still Wild”, The Journal of Philosophy, 85(2): 75–87. doi:10.2307/2026993

  • Schmidt, Arnold, 1951, “Die Zulässigkeit der Behandlung mehrsortiger Theorien mittels der üblichen einsortigen Prädikatenlogik”, Mathematische Annalen, 123(1): 187–200. doi:10.1007/BF02054948

  • Scott, Dana, 1961, “Measurable Cardinals and Constructible Sets”, Bulletin de l' Académie Polonaise des Sciences, Série des sciences mathématiques, astronomiques et physiques, 9: 521–524.

  • Shapiro, Stewart, 1991, Foundations without Foundationalism: A Case for Second-Order Logic, New York: Oxford University Press. doi:10.1093/0198250290.001.0001

  • Shelah, Saharon, 1973, “There Are Just Four Second-Order Quantifiers”, Israel Journal of Mathematics, 15(3): 282–300. doi:10.1007/BF02787572

  • –––, 2004, “Spectra of Monadic Second Order Sentences”, Scientiae Mathematicae Japonicae, (Special issue on set theory and algebraic model theory), 59(2): 351–355. [Shelah 2004 available online]

  • Simpson, Stephen G., 1999 [2009], Subsystems of Second Order Arithmetic, second edition, (Perspectives in Logic), Cambridge: Cambridge University Press. first edition in 1999, New York: Springer. doi:10.1017/CBO9780511581007

  • Tarski, Alfred, 1933 [1956], Pojęcie Prawdy w Językach Nauk Dedukcyjnych (Le concept de vérité dans les langages formalisés), (Prace Towarzystwa Naukowego Warszawskiego, Wydział III Nauk Matematyczno-fizycznych/Travaux de la Société des Sciences et des Lettres de Varsovie, Classe III Sciences Mathématiques et Physiques, 34), Warsaw. German translation see Tarski 1936. English translation as “The Concept of Truth in Formalized Languages” in Tarski 1956: chapter 8: 152–278.

  • –––, 1936 [1956], “Der Wahrheitsbegriff in Den Formalisierten Sprachen”, Studia Philosophica, 1: 261–405. Translated as “The Concept of Truth in Formalized Languages” in Tarski 1956: chapter 8.

  • –––, 1956, Logic, Semantics, Metamathematics; Papers from 1923 to 1938, J. H. Woodger (trans.), Oxford: Clarendon Press.

  • Tharp, Leslie H., 1973, “The Characterization of Monadic Logic”, Journal of Symbolic Logic, 38(3): 481–488. doi:10.2307/2273046

  • Väänänen, Jouko, 1979, “Abstract Logic and Set Theory. I. Definability”, in Logic Colloquium ’78: Proceedings of the Colloquium Held in Mons, Maurice Boffa, Dirk van Dalen, and Kenneth Mcaloon (eds.), (Studies in Logic and the Foundations of Mathematics 97), Amsterdam: Elsevier, 391–421. doi:10.1016/S0049-237X(08)71637-9

  • –––, 1980, “Boolean Valued Models and Generalized Quantifiers”, Annals of Mathematical Logic, 18(3): 193–225. doi:10.1016/0003-4843(80)90005-4

  • –––, 2012, “Second Order Logic or Set Theory?”, The Bulletin of Symbolic Logic, 18(1): 91–121. doi:10.2178/bsl/1327328440

  • Väänänen, Jouko and Tong Wang, 2015, “Internal Categoricity in Arithmetic and Set Theory”, Notre Dame Journal of Formal Logic, 56(1): 121–134. doi:10.1215/00294527-2835038

  • Walmsley, James, 2002, “Categoricity and Indefinite Extensibility”, Proceedings of the Aristotelian Society, 102(1): 239–257. doi:10.1111/j.0066-7372.2003.00052.x

  • Wang, Hao, 1952, “Logic of Many-Sorted Theories”, Journal of Symbolic Logic, 17(2): 105–116. doi:10.2307/2266241

  • Zermelo, Ernst, 1930, “Über Grenzzahlen und Mengenbereiche: Neue Untersuchungen über die Grundlagen der Mengenlehre”, Fundamenta Mathematicæ, 16: 29–47.

Academic Tools

Other Internet Resources

Related Entries

category theory | computability and complexity | mathematics: constructive | plural quantification | set theory | set theory: independence and large cardinals | set theory: large cardinals and determinacy | type theory

Copyright © 2019 by Jouko Väänänen <jouko.vaananen@helsinki.fi>

上一页相干逻辑 relevance (Edwin Mares)下一页*句子连接词——见连接词：形式逻辑中的句子连接词 sentence connectives in — see connectives: sentence connectives in formal logic

最后更新于

Logo

道长哲学研讨会 2024