逆向数学（一）

1. 逆向数学的历史介绍

1.1 数学必然性和公理化方法

1.2 分析的算术化

1.3 从递归反例到逆向数学

1.4 逆向数学的早期发展

2. 二阶算法及其子系统

2.1 二阶算术语言

2.2 二阶算术的语义

2.3 二阶算术公理

3. 基础理论

3.1 递归理解

3.2 配对、序列和编码基础知识

3.3 整数、有理数和实数

3.4 ω-模型和可计算性

4.五巨头

4.1 弱König引理

4.2 算术理解

4.3 算术超限递归

4.4 Π11 理解

5. 基础程序和逆向数学

5.1 可计算数学、构造性数学和 RCA0

5.2 有限论和RCA0

5.3 有限还原论和WKL0

5.4 算术可定义性和可预测性

5.5 算术超限递归和预测性的局限性

6. 进一步阅读

参考书目

学术工具

其他互联网资源

相关条目

1. 逆向数学的历史介绍

1.1 数学必然性和公理化方法

逆向数学是数理逻辑的一个相对年轻的子领域，作为可计算性理论的产物始于 20 世纪 70 年代中期。在该领域的创始论文（Friedman 1975）中，哈维·弗里德曼首先问

在数学中证明特定定理或定理体时，可以使用哪些正确的公理？那些隔离了证明它们所需的基本原理的正式系统是什么？ （1975：235）

弗里德曼关于证明给定定理的适当公理的概念是一种不仅可以从公理证明定理，而且可以从定理证明公理的概念。换句话说，为了证明该定理，正确的公理是必要的，而不仅仅是充分的。

从这个意义上说，寻找正确的公理来证明给定的定理是数学领域的长期努力。欧几里得的第五条公设，即平行公设，是一个老生常谈的例子。为了证明欧几里得几何中的许多重要结果（例如毕达哥拉斯定理），这是必要的，但历史上的数学家都发现这个假设令人不安。 Lewis (1920) 认为，欧几里得试图找到正确的原理来证明 29 以后的命题，而平行公设最终被作为公设给出，仅仅是因为没有找到其他方法来证明这些命题。整个古代，尤其是普罗克卢斯，以及中世纪伊斯兰世界和现代时期，人们都在尝试证明平行假设（Bonola 1912；Rosenfeld 1976 [1988]）。我们现在知道这些尝试存在难以克服的障碍。正如十九世纪所发现的那样，存在满足其他公设但不满足平行公设的非欧几里得几何模型。因此，平行公设并不遵循其他公设。

为了证明平行公设对于证明毕达哥拉斯定理是必要的，我们需要从定理到公理的逆转。我们通过证明毕达哥拉斯定理的平行假设来做到这一点，从而建立蕴涵

勾股定理⇒平行公设，

同时小心地只使用其他几何公设，而不是使用平行公设本身进行循环推理。由于毕达哥拉斯定理是从平行假设得出的，因此这两个陈述是等价的，以其他几何假设为模。此外，由于平行公设独立于其他公设，因此从这种等价性出发，毕达哥拉斯定理也是如此：它在所有且仅那些欧几里得几何中为真，即平行公设成立的几何。

希尔伯特在他的《Grundlagen der Geometrie》（1899）中对欧几里得几何和非欧几里得几何的公理化提供了一个可以给出原理之间等价性证明的环境。特别是，希尔伯特公理提供了类似形式基础理论的东西，可以从平行假设证明毕达哥拉斯定理，反之亦然。此类证明现在已成为本科几何教科书中的标准练习（例如 Hartshorne 2000）。至关重要的是，希尔伯特的基础理论并没有证明平行公设：正如希尔伯特所表明的，基础理论有分析模型（由实数构建的模型），其中平行公设为真，但也有平行公设为假的模型。在纯粹的逻辑层面上，如果 T 是一个形式理论，并且 ψ 和 ψ 在 T 中都是可证明的，那么 T 证明它们是等价的。类似地，如果 Øφ 和 Øψ 都可证明，则 T 也证明 Ø 和 ψ 是等价的。因此，平行公设与希尔伯特基本理论的独立性表明，平行公设和毕达哥拉斯定理之间的等价性是非平凡的，因为它不能建立在两者都是可证明的平凡基础上，也不能建立在两者都可证明的平凡基础上。是可以反驳的。

尽管这篇文章不会进一步涉及几何等价性的研究，但应该指出的是，这个领域仍然充满活力。例如，Pambuccian (1996, 2001, 2006, 2009) 的工作在其动机上是明确的哲学性的，并且激发了从事数学方法论和逻辑纯粹性问题的哲学家的兴趣。一些代表性作品有Arana (2008年；Arana & Mancosu 2012年；Baldwin 2013年；Pambuccian 2019年)、Pambuccian & Schacht (2021年)。 Dean（2021）从不同的方向研究逆向数学和几何原理，即它们对弗雷格-希尔伯特争议的影响。

第二个历史先例是集合论中的选择公理（AC）。 Zermelo (1904) 在证明良序定理时引用了选择公理，引起了人们对选择公理的广泛关注。在此过程中，他引发了对该原理的争议，并招致了亨利·庞加莱和埃米尔·博雷尔（Moore 1982）等数学名人的广泛批评。在对这些批评的回应中，Zermelo（1908）认为AC是“科学所必需的”，特别是有

在我看来，如果没有选择原则，根本无法解决基本的定理和问题。 （策梅洛 1967：187–188）

策梅洛所指的“基本定理和问题”包括诸如两个集合的基数是否总是可比较的基本问题。与毕达哥拉斯定理的情况一样，历史已经证实了策梅洛的论点，即选择公理对于证明此类陈述是必要的，因为它们意味着选择公理对策梅洛-弗兰克尔集合论 (ZF) 的其他公理取模（Jech 1973；Rubin & Rubin 1963、1985；Howard & Rubin 1998）。保罗·科恩 (Paul Cohen) 的强迫发现进一步证明了与平行假设的情况相似，因为选择公理被证明在形式上独立于基础理论 ZF。因此，AC 与良序定理等陈述的等价性被证明是不平凡的，就像平行公设与毕达哥拉斯定理等陈述的等价一样。

然而，逆向数学与选择公理等价性的研究以及更普遍的 ZF 上可证明的等价性研究之间存在实质性差异。逆向数学涉及可以用自然数集表示的结构，而不是任意基数集。正如我们将在本文中看到的那样，这些结构和与之相关的定理比人们最初想象的要广泛得多，其中包括通常被称为“普通数学”的很大一部分。虽然选择公理相当于拓扑学、泛函分析和组合学中的许多重要的一般定理，但在日常数学应用中很少需要这些结果的完全通用性。关于“具体”结构（例如实数）的基本特征定理仅需要二阶算术弱子系统的公理。最后，选择公理还以其纯粹的存在性本质而著称：它没有给出从无限集合族中选择元素的方法或过程，而只是断言存在某种这样的选择。另一方面，逆向数学中研究的集合存在原理都具有可计算性理论方面，因此与可定义性密切相关，这构成了本文的主题。对于像算术理解（第 4.2 节）这样的原理，这种联系位于表面上，而对于弱 König 引理（第 4.1 节）等其他原理，这种联系不太明显，但同样真实（Eastaugh 2019）。

1.2 分析的算术化

尽管逆向数学的许多方面都植根于几何学，但数学的另一个部分提供了许多其他内容：分析。这是数学的一部分，涉及实数的连续统以及基于它的许多结构。分析提供了大部分主题，因为许多分析定理被证明等同于逆向数学中研究的集合存在原理。它也是逆向数学家的大部分工具包，即在二阶算术中表示复杂对象和结构所需的各种编码方案。

逆向数学和分析之间联系的两个方面都可以追溯到十九世纪，当时数学，特别是分析，经历了翻天覆地的变化。推动力之一是希望提高数学分析的严谨性，用基于原始集合论原理和构造的“算术”论证取代几何直觉和无穷小量。

在分析的算术化过程中取得的许多重要进展中，我们可以选出三个特别重要的进展：收敛数列和极限的新定义；连续函数；以及实数系统本身。假设 x=⟨xn：n∈N⟩ 是无限实数序列。那么实数 y 是序列 x 的极限，用符号 y=limn→∞xn 表示，如果对于每个实数 ε＞0 都存在一个自然数 N，使得对于所有自然数 n＞N，|xn−y |＜ε。极限概念的定义仅取决于实数和自然数的概念，以及算术运算、绝对值、阶数和无限序列的概念：不需要求助于几何概念。这一发展为更彻底的算术化奠定了基础，其中实数的概念也被类似地减少了。

与连续性和收敛性的概念一样，实数的定义在这一时期也经历了重大的演变。历史上，无理数一直被视为几何学，例如 2 的平方根是单位正方形对角线的长度，或者 π 是圆的周长与其直径的比值。虽然在 19 世纪发展实数算术定义的分析家并不旨在消除这种几何方面，但他们倾向于以怀疑的态度看待证明中对几何直觉的诉求，并希望给出一种不依赖于几何直觉的实数理论。基于这种直观的考虑。

乔治·康托尔（Georg Cantor）就是这样的理论之一，他根据有理数的收敛序列给出了实数的构造（Cantor 1872，1883）。有一些不合时宜的地方，让 x：N→Q 是从自然数到有理数的全函数。我们可以将 x 视为无限有理数序列⟨xn：n∈N⟩。 x 是一个基本序列，如果存在 k∈N，使得对于每个正有理数 ε，|xn+m−xn|＜ε 对于每个 m，n∈N，其中 n＞k。然后，我们可以按照惯例将基本序列 x 与实数 y=limx 联系起来，即序列 x 在极限情况下达到的值。此外，康托还展示了如何将加法、减法、乘法和除法的运算扩展到被视为基本序列极限的实数。

理查德·戴德金 (Richard Dedekind) 在其 1872 年的专着《Stetigkeit und irrationale Zahlen》中提出了一种截然不同的处理实数的方法，即将有理数“切割”或分为上下两部分。戴德金的方法最初是为 1858 年在苏黎世理工学院教授的入门课程制定的，他认为实数不符合有理数收敛序列的极限，而是符合有理数中的任意“切割”。割是一对不相交的非空有理数集 (A1，A2)，使得 A1∪A2=Q 并且 A1 向下闭，而 A2 向上闭：如果 p 和 q 是有理数，且 p＜q，如果q ε A 1 则 p ε A 1 ，如果 p ε A 2 则 q ε A 2 。实数 x∈R 对应于割 (A1，A2)，或者由割 (A1，A2) “创建”，以防万一对于每个 p∈A1，p≤x，以及对于每个 q∈A2，x＜q。

尽管戴德金德和康托尔的概念存在差异，但他们的构造有很多共同点。它们都将有理数以及一些集合论机制作为实数的基础。在戴德金的例子中，这涉及有理数的任意子集的概念，而在康托的例子中，它涉及有理数的无限序列的概念。正如康托尔和戴德金所知，有理数的讨论原则上可以简化为自然数的讨论，他们的定义可以被视为将实数简化为“算术”：自然数，以及自然数理论的某些部分。套。这部分实际上很小，只需要一组自然数的概念，康托尔和戴德金对实数的定义都可以（经过一些修改）用二阶算术形式化（参见§3.3了解前者和Simpson (1984) 对于后者）。

戴德金 (Dedekind, 1872) 除了将实数开创性地定义为有理数的切口，并将连续性原理表述为算术连续统的基本公理之外，还包含了对反转方法的惊人预见，作为第一个Sieg 指出（1988：344，fn.16）。 《Stetigkeit und irrationale Zahlen》的最后一部分致力于分析的基本定理，即单调收敛定理和柯西收敛定理。戴德金表明，连续性原理不仅可以用来推导这些定理，而且这些定理反过来也可以用来推导连续性原理。

从这时起，算术的故事就与逻辑的故事联系在一起了。弗雷格和皮尔斯对量化逻辑的发展、皮亚诺的象征主义以及罗素对类型论的发展都在希尔伯特学派工作中适合算术和分析形式化的现代框架的出现中发挥了重要作用。 ，最著名的是希尔伯特与威廉·阿克曼和保罗·伯奈斯的合作。这些成果在希尔伯特和伯奈斯的巨著《数学原理》中达到了顶峰，该书分两卷出版（1934 年、1939 年）。有兴趣的读者可能会更容易获得第二版（1968 年、1970 年）。

在希尔伯特和伯奈斯的《Grundlagen》对数学基础的众多贡献中，与逆向数学和二阶算术子系统研究最明显的直接联系出现在第 2 卷的补遗 IV（1939/1970）中。本补充介绍了几种算术形式主义，它们可以被视为逆向数学中使用的二阶算术公理系统 Z2 的祖先，在本条目的第 2.3 节中定义。补充 IV 的大部分内容使用系统 H，其中包括自由和绑定的一阶和二阶变量。一阶变量的预期范围是自然数。二阶项是一元函数项，而不是集合或谓词项，二阶变量的预期解释是函数 f：N→N (Hilbert & Bernays 1970: 467)。形式主义的这些方面与二阶算术的语言 L2 非常相似，但在其他方面，系统 H 与当代实践有相当明显的分歧。一方面是包含自由公式变量，桑德斯（Sanders，2022：2）等一些作者将其解释为将三阶参数和运算符引入系统。另一个是该系统使用希尔伯特 epsilon 演算的一种形式，尽管补充 IV 的 F 节中引入的修订形式 K 展示了如何修改系统 H 以消除这种依赖性。函数项而不是集合项的使用一直延续到后来的工作中，例如 Grzegorczyk、Mostowski 和 Ryll-Nardzewski (1958) 的工作，但事实上 Hilbert 和 Bernays 在补充 IV 的 G 节中也定义了一个系统 L，该系统交换自由和绑定公式变量的自由和绑定函数变量。

在建立了高阶算术的形式系统 H 后，希尔伯特和伯内斯继续将其中的实分析的实质性片段形式化，包括表明最小上界原理的一个版本成立。他们明确评论（Hilbert & Bernays 1970：482），通过单独的数论函数表示实数序列的可能性，就像现在通过单独的自然数集在逆向数学中所做的那样（详细信息请参见§3.3），取决于能够定义从（可数）数论函数序列到单个数论函数的可逆映射，该映射本身源于从自然数对到单个数字的可逆映射。这种表示形式的存在和使用可以被理解为十九世纪发展起来的算术化传统的延续，尽管现在是在精确界定的形式系统中而不是在非正式数学中。

因此，算术化可以被理解为逆向数学发展的重要组成部分，因为它展示了如何将复杂的数学概念（例如实数、连续函数、度量等）简化为更基本的概念，即自然数的概念和集合或集合的概念。这种还原精神在逆向数学的整个历史中始终保持着其重要性，尽管它以多种不同的方式表现出来。一种是通过希尔伯特的将无限数学还原为有限数学的方案，以及通过证明论中的还原方案来延续它。另一个是无处不在地使用编码来表示看似严峻的二阶算术本体中的各种数学对象（特别参见§3.2–§3.3，了解逆向数学中编码的基本原理）。

对于有兴趣更详细地追踪二阶算术发展的读者来说，从 Hilbert 和 Bernays 的工作开始，Dean & Walsh (2017) 的工作是一个重要的起点。 Sieg & Ravaglia (2005) 回顾了《数学原理》第一版两卷的内容，尽管没有对补充 IV 进行太多讨论。希尔伯特关于算术和逻辑基础的讲座（Ewald & Sieg 2013）还提供了有关最终出现在《Grundlagen》中的思想发展的更多细节。 Sieg (1984, 2020) 详细介绍了本节中相关的一些概念进展及其哲学影响。其他参考文献可以在希尔伯特程序条目的参考书目中找到。

1.3 从递归反例到逆向数学

尽管逆向数学深深植根于希尔伯特学派（第 1.2 节）的工作，但从方法论上（以及历史上）来看，逆向数学也许最好被理解为可计算性理论以及更广泛的可定义性理论的产物。特别是，反转方法可以被视为起源于经典定理的递归反例的传统。这些是可计算对象，当它们的量词仅限于可计算（递归）对象时，它们见证了经典数学定理的失败。递归反例的一个典型例子是 Specker 序列：一个可计算的、有界递增的实数序列，没有可计算的限制。斯佩克序列是单调收敛定理和 Bolzano-Weierstraß 定理等定理的递归反例。

Specker（1949）没有从他的结果中得出明确的哲学结论，但显然他理解这些结论不仅适用于可计算分析，而且适用于构造性数学。这是当时逻辑学家的普遍态度：因为递归函数的形式概念允许我们对算法和有效过程的非正式概念给出精确的数学表征，所以很自然地假设它也可以让我们理解数学构造的非正式概念。使用可计算性理论来研究构造性数学是由克莱恩（Kleene）及其对直觉逻辑的可实现性解释（Kleene 1945）开创的。 Kleene 在可实现性和 Brouwer 扇形定理（Kleene 1952）方面的工作导致他构建了 Kleene 树，这是一种没有可计算路径的可计算树，这对于发现弱 König 引理的可计算性理论属性非常重要。一个独立但同样重要的发展是俄罗斯马尔可夫学派的递归构造性数学，它也试图根据递归函数的概念来理解构造的概念（Nagorny 1994；Kushner 2006；Moschovakis 出现）。

许多建构主义者要么接受丘奇论文的某种形式——即每个建构过程就其输出而言，在外延上等价于一个可计算函数——要么接受与其一致的系统。像单调收敛定理这样的定理与这种方法不兼容，因为正如斯佩克发现的那样，存在可计算（因此是构造性的）有界数序列，没有可计算的极限。因此，对于建构主义者来说，斯佩克序列的极限并不存在，不仅因为它暗示了建构主义丘奇论点的虚假性，而且还因为它暗示了一种被称为全知有限原则（LPO）的原则，即削弱了建构主义者通常也否认排除中间法则（Mandelkern 1988，1989）。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。