二阶和高阶逻辑（四）

证明是通过减少到自动机进行的。自动机是图灵机的限制形式。在自动机中，机器从未在胶带上写入，因此胶带只包含输入（Rabin＆Scott 1959）。但是，计算可能是无限的。如果无限地达到接收状态多次，则在无限计算的情况下认为输入被认为是接受的。 （也有更复杂的接受标准）。使用Monadic二阶逻辑，我们可以猜测自动机的接受计算。可能会出现自动机可以检查Monadic二阶句子的真相。从可决定性的角度进行了广泛的研究，对序数（\ alpha，＜）的统一二阶理论进行了广泛研究。例如，所有可计数的句子，\ omega_1的理论和所有序列的理论＜\ omega_2的理论都是可决定的（Büchi1973），但是ZFC无法决定是否可以决定\ omega_2的\ omega_2二阶理论，是可决定的（Gurevich，Magidor和Shelah 1983）。

9。二阶逻辑的公理

回想我们的惯例：每当我们使用上案例fraktur字母，例如\ ma，\ mb，\ mm，\ mn等，以命名结构，我们都会使用这些字母的上情况斜体版本，例如a，b，m ，n等，以命名结构的域。

二阶逻辑的演绎系统首先在 Hilbert-Ackermann (Hilbert & Ackermann 1938) 中明确提出，它基于一阶逻辑公理和规则的明显扩展以及综合公理模式，定义如下：假设 \ phi(x_1,\ldots,x_n) 是一个二阶公式，其中 x_1,\ldots, x_n 为自由个体变量，二阶变量 R \phi 中不是免费的。那么下面的公式是理解公理模式的一个实例：

\tag{10}\label{CA} \存在 R\,\forall x_1\ldots x_n(\phi(x_1,\ldots, x_n)\leftrightarrow R(x_1,\ldots, x_n))。

定义函数的二阶公式有类似的模式，但我们在这里省略它。

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

\frac{\dfrac{2+5＜9}{\存在 R\ R(2+5,9)}}{\存在 F\,\存在 R\ R(F(2,5),9)}

先验（\ref{CA}）可能显得非常强大，因为它规定了关系的存在。然而，这样的 R 似乎可以合理接受，因为它是可定义的：

R=\{(a_1\ldots a_n) \in M^n: \mm\models \phi(a_1,\ldots, a_n)\}。

我们的理解公理模式是必然的，因为公式 \phi(a_1,\ldots, a_n) 中可能出现的绑定 n 元关系变量在其范围内具有 R。从这个意义上说，二阶逻辑是完全必然的。理解公理模式具有较弱的形式，不那么必然。在算术理解模式中，我们假设 \phi(a_1,\ldots, a_n) 是一阶。在 \Pi^1_1-推导式中，我们假设 \phi(a_1,\ldots, a_n) 是 \Pi^1_1。在数学实践中，这两个较弱的原则通常就足够了，请参见 Simpson (1999 [2009]) 和§14。

Hilbert-Ackermann (1938) 在二阶逻辑的证明系统中还添加了两个不同的模式，他们称之为选择公理。我们习惯于将选择公理视为集合论原理。但二阶逻辑的选择原理与集合论有相同的情况。在二阶逻辑中，询问域是否存在良序是完全有意义的。这种良序的存在通常不能从理解模式中得出，因为良序可能并且很可能是无法定义的。因此，在二阶逻辑中获得良序的实数的唯一方法是假设某种形式的二阶选择公理。首选原则是

\tag{AC}\forall x_1\ldots x_m\exists x_{m+1}\, R(x_1,\ldots, x_{m+1}) \rightarrow {}\\ \exists F\,\forall x_1\ ldots\forall x_m\, R(x_1,\ldots, x_m, F(x_1\ldots x_m))

第二个是

\tag{AC′} \forall x_1\ldots x_m\exists F\,\varphi\rightarrow\exists F'\,\forall x_1\ldots x_m\varphi',

其中公式 \varphi' 是通过将公式 \varphi 处处的 F(t_1,\ldots, t_k) 替换为 F'(t_1\ldots t_k,x_1,\ldots, x_m) 来获得的。

第一个选择公理 (AC) 直观地说，如果一个集合

\{a_{n+1}\in M : \mm\模型 R(a_1,\ldots,a_n, a_{n+1})\}

是非空的，那么有一个函数使用参数 a_1,\ldots,a_{n} 作为参数，从集合中选取一个元素 a_{n+1} 。第二个选择公理 (AC′) 是一种二阶选择：对于所有 a_1,\ldots,a_n，我们有一个具有属性 \phi 的函数 F，因此实际上 F 取决于 a_1,\ldots, a_n 和应表示为 F_{a_1\ldots a_n}。 (AC′) 现在所说的是，我们可以将函数 F_{a_1\ldots a_n} 收集在一起以形成一个更高数量的函数 F'，这样

F'(a_1,\ldots,a_{n+1})=F_{a_1\ldots a_n}(a_{n+1})。

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

(a_1,\ldots,a_n)\映射到 F_{a_1\ldots a_n}

可能是高度无法定义的。

当然，我们可能还想假设良序原理，它指出存在一种二元关系，它是个体上的全序，并且满足每个非空个体集合在顺序中具有最小元素的条件。容易看出该原理隐含着(AC′)。在 ZFC 中，有数百个选择公理的等效公式或其较弱的版本。大多数在 ZFC 中等效的公式在二阶逻辑中是非等效的。这是因为集合论允许集合及其幂集之间的自由移动，但二阶逻辑不允许[11]。为了获得与集合论中类似的等价证明，人们必须在二阶逻辑和三阶逻辑之间转换，参见 Gaßner (1994) 和 Siskind, Mancosu & Shapiro (2023)。

9.1 通用模型和Henkin模型

Henkin（1950）为了获得二阶逻辑的完备性定理而引入了“一般模型”的概念。一般模型不是公理的预期模型，因为绑定关系和函数变量不在这些模型中的所有关系和函数上，而仅在它们的集合上。人们普遍接受的态度是，它们不是人们想要的，但它们是获得顺利理论所必需的。它们就像微积分中的无理数：如果我们在微积分（或几何）中遇到的所有长度都是可通约的，那将是理想的，但事实并非如此。有些长度是不可通约的，我们最终接受无理数，以便有一个关于长度及其比例的平滑的一般理论。一般模型也可以与集合论的传递模型进行比较。一种传递模型可能会说一件事是正确的，而另一种模型可能会说相反的事情是正确的。但传递模型一起帮助我们理解集合论的公理。目前对集合论公理进行元数学研究的方法，即内模型和强制外延，都在本质上使用了集合论的传递模型。类似地，二阶逻辑的一般模型帮助我们研究二阶逻辑及其公理的元数学性质。

定义 12 一般模型是一对 (\mm,\G)，其中 \mm 是通常的 L 结构，\G 是 M 上的子集、关系（任意数量）和函数（任意数量）的集合。在一元二阶逻辑中，假定 \G 仅包含一元谓词。

我们可以定义这个概念

(\mm,\G)\models_s\phi

对于二阶 \phi，通过规定 \phi 进行归纳

\begin{align} (\mm,\G)\models_s\exists X\,\phi & \iff (\mm,\G)\models_{s(P/X)} \phi\text{ 对于某些 $P \in \G$}.\\ (\mm,\G)\models_s\存在 F\,\phi &\iff (\mm,\G)\models_{s(f/X)} \phi\text{对于某些人来说$f\in\G$}。 \结束{夕阳}

因此，与二阶逻辑的原始真值定义的区别在于，二阶变量的解释不能非常任意，它们必须在\G中找到。 \G 越小，逻辑越弱。另一方面，如果 \G^\star 是 M 上所有关系和函数的集合，则通用模型 (\mm,\G^\star) 的真值定义与原始真值定义相同。我们称这种通用模型为完整模型，并且确实将 (\mm,\G^\star) 与 \mm 等同起来。另一个极端是\G=\emptyset。然后我们回到一阶逻辑。为了区分具有一般模型的二阶逻辑和原始二阶逻辑，我们将后者称为完整的。

定义13 满足二阶逻辑所有公理（包括理解公理模式和选择公理）的通用模型称为亨金模型。

请注意，没有二阶逻辑语句表明模型是完整的。也就是说，不存在二阶 \phi 使得对于所有一般模型 (\mm,\G) 都成立

(\mm,\G)\models\phi\iff (\mm,\G) \text{已满。}

如果我们尝试使用 \forall X\,\exists Y\,\forall x(X(x)\leftrightarrow Y(x)) 作为这样的 \phi，我们只会得到 \phi 总是 true 的结果，并表示一般模型（\mm，\G）是其本身意义上的“满”，而不是元理论意义上的“满”。

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

获得 Henkin 模型 (\mm,\G) 的一个简单方法是采用 ZFC 的传递模型 N，使得 \mm\in N 并让 \G 由 M 上作为 N 元素的所有关系和函数组成。从 N\models ZFC 可以得出 (\mm,\G) 是 Henkin 模型。

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

具有一般模型的二阶逻辑可以被认为是许多排序逻辑。许多排序逻辑是具有几种不同类型变量的一阶逻辑。关系和功能分别可以存在于不同类型的元素之间。这里的“排序”只是意味着通过给不同“类别”的变量赋予不同的名称来将它们分开。否则变量只是普通的一阶变量。多排序逻辑的结构 \mm 对于每个排序 s 有一个单独的域 M_s。我们可以将二阶逻辑视为许多排序逻辑，其中各个变量的排序为 \si，对于每个 n，n 元关系变量的排序为 \sr，n 元函数变量的排序为 \sr s_n^{\rm fu}。此外，在 n 元组个体和 n 元关系变量之间有一个 n+1 元关系符号 \sA ，指示哪些 n 元组处于关系中，哪些不处于关系中。最后，在个体、个体和n元函数变量的n元组之间有一个n+1元函数符号\sF，指示函数变量赋予每个n元组什么值。有明显的一阶公理保证刚刚描述的许多排序逻辑忠实地反映了具有通用模型的二阶逻辑。 [12]

有关将二阶逻辑简化为多排序逻辑的更多信息，请参阅 Manzano (1996)。例如，二阶逻辑的证明论可以通过转换为多排序逻辑来理解。有关二阶逻辑证明论的更多信息，请参见 Buss (1998)。主要归因于 Herbrand (1930)，将许多排序逻辑进一步转换为单个排序一阶逻辑，另请参阅 Wang (1952) 和 Schmidt (1951)。这可用于首先获得许多排序逻辑的一阶逻辑的许多基本属性，然后进一步获得具有通用模型的二阶逻辑的许多基本属性。

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

定理 14 (Henkin 1950) 当且仅当它在所有 Henkin 模型中都为真时，二阶句子才能从公理得出。 [13]

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

思考亨金模型的一种方法是，它们填补了完整模型留下的空白，就像无理数填补了有理数留下的空白一样。为了获得平滑的二阶逻辑理论，需要它们。它们表现出我们在完整模型中看不到的“矛盾”现象。例如，我们获得了数论的非标准模型、实数公理的可数模型等。完整模型中表征数学结构的分类句子现在突然也有了其他“模型”，即亨金模型，它们全部出现了。无限基数。

如果 \phi 是我们定义的二阶句子

\tag{11}\label{henkin} \textit{Mod}_H(\phi)=\{(\mm,\G) : (\mm,\G)\models\phi\}

显然，\Mod(\phi)\subseteq \textit{Mod}_H(\phi)。如果 \phi 将 \mm 表征为同构，则 \mm\in \Mod(\phi) 。在所有重要情况下[16] \textit{Mod}_H(\phi)\ne \{\mm\}。对于 \mm\in\Mod(\phi)，我们可以将 (\mm,\G)\in\textit{Mod}_H(\phi) 视为 \mm 的“近似值”。其中一个近似值是“真实的”\mm，即 (\mm,\G^*)，但通过二阶逻辑的推导，我们无法判断是哪个。由于形式系统固有的弱点，追溯到斯科伦和哥德尔，无限结构被亨金模型所笼罩，无法通过演绎手段完美地聚焦。

Fraenkel-Mostowski 方法是 Henkin 模型的一种构造，它首先用于集合论中以获得选择公理失败的模型，后来用于二阶逻辑以获得类似的模型，然后强制方法出现。方法如下：假设\ma是一个结构，H是\ma的一组自同构。如果存在有限集 E\subseteq A（称为 B 的支持），则 A^n 的子集 B 称为对称子集，使得对于所有固定 E 的 \pi\in H 逐点[17]，

\forall x_1\ldots\forall x_n((x_1,\ldots, x_n)\in B\to (\pi(x_1),\ldots, \pi(x_n))\in B)。

函数 f:A^n\to A 的相应条件是

\forall x_1\ldots\forall x_n ((x_1,\ldots ,x_n) \in B \to f(\pi(x_1), \ldots ,\pi(x_n)) \in B \land {}\\ f( \pi(x_1),\ldots ,\pi(x_n)) = \pi (f (x_1,\ldots ,x_n )))

令 \G 为 A 上的对称关系和函数的集合。 (\ma,\G) 对始终是 Henkin 模型。

在 Fraenkel-Mostowski 方法的早期应用中，Mostowski (1938) 的结果表明，仅从理解公理模式无法证明某些两个不同的有限性定义的等价性；Lindenbaum 和 Mostowski (1938) 的结果表明，Zermelo 的集合公理理论不足以证明选择公理，甚至不足以证明每个无限集都是两个无限集的不相交并。

如果 H 是无限集合 A 的所有排列的群，则出现 Fraenkel 模型。在 Fraenkel 模型中，集合 A 是无限的，但 Dedekind 有限（即，A 没有进入真子集的一一函数）并且不能很好地表示-有序的，甚至不是线性有序的。此外，集合 A 不是两个无限集合的不相交并。 A 的两个元素子集没有选择函数。

如果 A=\oQ 且 H 是 (\oQ,＜) 的自同构群，则 Mostowski 模型出现。在 Mostowski 模型中，集合 A 可以是线性有序的，但不是良序的。选择公理适用于非空有限集（组）。

有关二阶逻辑的 Fraenkel-Mostowski 模型作为 Henkin 模型的更多信息，请参阅 Gaßner (1994)。

9.2 无穷公理

回想一下我们的约定：每当我们使用大写 Fraktur 字母（例如 \ma、\mb、\mm、\mn 等）来命名结构时，我们都会使用这些字母的大写斜体版本，例如 A、B、M ,N 等，命名结构的域。

二阶逻辑的公理在只有一个元素的（完整）模型中是微不足道的。这就提出了如何保证域中存在多个元素的问题。当然，我们可以为每个 n 添加一个公理，表示有超过 n 个元素。在二阶逻辑中，有多种方法可以用一个公理来表达存在无限多个个体。这些在完整模型中是等效的，但在 Henkin 模型中可能不等效。如果假设选择公理，有些是等效的。让我们将空词汇表的二阶句子 \phi 称为无穷大公理如果

\ma\models\phi\text{当且仅当$A$ 是无穷大}。

无穷大公理可以在二阶逻辑中表示域的真子集与整个域具有相同的基数（即域不是戴德金有限），或者存在没有最大元素的偏序，或者存在一个具有一元函数和一个常量的集合，构成与 (\oN,s,0) 同构的结构，或者域是具有相同基数的两个不相交集合的并集如域等。正如没有选择公理的集合论中的情况一样，无限性的不同表述不必是等价的。在二阶逻辑中，由于选择公理有多种不同的表述，情况更加分散。我们参考 Asser (1981) 来讨论不同的变体，参考 Hasenjaeger (1961) 来证明无限公理的各种非等价形式在某种意义上形成了一个稠密集。有关有限性的不同概念的调查，请参见 de la Cruz (2002)。

10. 类别性

如果二阶（或一阶）逻辑中的任何两个模型是同构的，则称该理论是范畴的。单个句子（具有模型）当且仅当它表征某个模型达到同构时才是分类的（参见第 7.1 节）。分类理论 \Gamma 的一个很好的属性是（语义）完整性：在编写该理论的语言中的任何句子 \phi 由 \Gamma 在以下意义上决定。要么 \Gamma 的每个模型都满足 \phi，要么 \Gamma 的每个模型都满足 \neg\phi。换句话说，\phi 或\neg\phi 是\Gamma 的（语义）逻辑结果。原因很简单： \Gamma 在同构之前只有一个模型 M。由于同构在二阶逻辑中保留了真值，\phi 或 \neg\phi 是 \Gamma 的（语义）逻辑结果，取决于 \ phi 在 M 中为真或在 M 中为假。