构造性数学（一）

一、简介

2.逻辑的建设性解释

3. 构造性数学的种类

3.1 直觉数学

3.2 递归构造数学

3.3 Bishop的构造数学

3.4 Martin-Löf的构造类型理论

4. 选择公理

5. 构造逆向数学

5.1 CRM 中的范定理

6.构造拓扑

7. 建构性数理经济与金融

八、结束语

参考书目

参考

相关文献

学术工具

其他互联网资源

相关条目

一、简介

在数学家断言某件事（除了公理之外）之前，他们应该已经证明它是正确的。那么，当数学家断定析取 P∨Q 时，其中 P 和 Q 是某种（正式或非正式）数学语言中语法上正确的陈述，他们的意思是什么？对这种析取的一种自然的解释（尽管我们将看到这不是唯一的）是，不仅（至少）陈述 P，Q 之一成立，而且我们可以决定哪一个成立。因此，正如数学家只有在通过证明 P 成立时才会断言 P 一样，只有当他们能够产生 P 的证明或产生 Q 之一时，他们才会断言 P∨Q。

然而，通过这种解释，我们在 Q 是 P 的否定 ØP 的特殊情况下遇到了一个严重的问题。断言 ØP 就是表明 P 意味着矛盾（例如 0=1）。但数学家常常既没有 P 的证明，也没有 ØP 的证明。要看到这一点，我们只需要反思以下哥德巴赫猜想（GC）：

每个大于 2 的偶数都可以写成两个素数之和，

自从 1742 年哥德巴赫写给欧拉的信中首次提出这个问题以来，尽管许多顶尖数学家尽了最大努力，但它仍然既没有被证明也没有被反驳。我们被迫得出结论，在 P ∨Q 的非常自然的可判定性解释下，只有顽固的乐观主义者可以保留对排中法则（LEM）的信念：

对于每个陈述 P，P 或 ØP 都成立。

经典逻辑通过扩大析取的解释来解决这个问题：它将 P∨Q 解释为 Ø(ØP∧ØQ)，或者换句话说，“P 和 Q 都是假的，这是矛盾的”。反过来，这导致了对存在的唯心主义解释，其中 ∃xP(x) 意味着 Ø∀xØP(x) （“对于每个 x，P(x) 都是假的，这是矛盾的”）。正是基于这些对析取和存在的解释，数学家们建立了宏伟的、显然坚不可摧的经典数学大厦，为物理、社会和（越来越多的）生物科学奠定了基础。然而，更广泛的解释是有代价的：例如，当我们从最初对 P∨Q 的自然解释过渡到不受限制地使用理想主义解释 Ø(ØP∧ØQ) 时，所得的数学通常不能是在计算模型（例如递归函数理论）中进行解释。

这一点可以用一个老生常谈的例子来说明，这个命题是：

存在无理数 a，b 使得 ab 是有理数。

一个巧妙的经典证明如下。任何一个

√2√2是有理数，在这种情况下我们取 a=b=√2；不然 √2√2是无理数，在这种情况下我们取 a=√2√2和 b=√2

（参见达米特 1977 [2000]，6）。但就目前情况而言，这个证明并不能让我们确定 (a,b) 两个选择中哪一个具有所需的性质。为了确定 (a,b) 的正确选择，我们需要决定是否

√

2

√

2

是有理还是无理，这正是运用我们对析取的最初解释与 P 的陈述“

√

2

√

2

是理性的”。

这是解释之间差异的另一个例子。考虑以下关于实数集合 R 的简单陈述：

∀x∈R(x=0∨x≠0),

其中，由于我们稍后会透露的原因，x≠0 意味着我们可以找到一个有理数 r，其中 0＜r＜|x|。 (*) 的自然计算解释是，我们有一个过程，应用于任何实数 x，要么告诉我们 x=0，要么告诉我们 x≠0。 （例如，如果 x=0，这样的过程可能会输出 0，如果 x≠0，则可能会输出 1。）但是，由于计算机只能通过有限有理近似来处理实数，因此我们会遇到下溢问题，其中足够小的正数可能会被计算机误读为 0；因此不可能有一个决策程序来证明该陈述 (*) 的合理性。换句话说，我们不能期望 (*) 在我们对量词 ∀ 和连接词 ∨ 的自然计算解释下成立。

让我们从另一个角度来审视一下这个问题。令 G(n) 充当“2n+2 是两个素数之和”的简写，其中 n 的范围为正整数，并定义一个无限二进制序列 a=(a1,a2,…) 如下：

一个={ 如果 G(k) 对于所有 k≤n 成立，则为 01 如果 ØG(k) 对于某些 k≤n 成立

毫无疑问，a 是一个计算上明确定义的序列，从某种意义上说，我们有一个为每个 n 计算 an 的算法：检查偶数 4,6,8,…,2n+2 以确定它们中的每一个是否是两个素数的和；在这种情况下，设置an=0，在相反情况下，设置an=1。现在考虑第 n 个二进制数字是 an 的实数：

x =(0⋅a1a2⋯)2

=2−1a1+2−2a2+⋯

=

无穷大

Σ

n=1

2−nan。

如果 (*) 在我们的计算解释下成立，那么我们可以在以下两种选择之间做出决定：

2−1a1+2−2a2+⋯=0，这意味着对于每个 n，an=0；

我们可以找到一个正整数 N，使得 2−1a1+2−2a2+⋯＞2−N。

在后一种情况下，通过测试 a1,…,aN，我们可以找到 n≤N 使得 an=1。因此，(*) 的计算解释使我们能够确定是否存在 n 使得 an=1；换句话说，它使我们能够确定哥德巴赫猜想的地位。这种类型的一个例子，表明某些经典结果 P 的建设性证明将使我们能够解决哥德巴赫猜想（并且通过类似的论证，许多其他迄今为止尚未解决的问题，例如黎曼假设），被称为布劳威尔例子，甚至是陈述 P 的布劳威尔式反例（尽管它不是该词正常意义上的反例）。

这里使用哥德巴赫猜想纯粹是戏剧性的。因为，上一段的论证可以修改为表明，根据我们的计算解释，(*) 暗示了全知的有限原则（LPO）：

对于每个二进制序列 (a1,a2,…)，对于所有 n，要么 an=0，要么存在 n 使得 an=1，

由于多种原因，这通常被认为是本质上非建设性的原则。首先，它的递归解释，

有一种递归算法，应用于任何递归定义的二进制序列（a1，a2，…），如果对于所有n，an = 0，则输出0，如果对于某些n，an = 1，则输出1，

在递归函数理论中，即使对于经典逻辑，也可证明是错误的（参见 Bridges & Richman [1987]，第 3 章）；因此，如果我们想允许对所有数学进行递归解释，那么我们就不能使用 LPO。其次，有一个模型理论（Kripke 模型），其中可以证明 LPO 不是构造性可导的（Bridges & Richman [1987]，第 7 章）。

2.逻辑的建设性解释

到目前为止，应该清楚的是，数学的全面计算发展不允许对大多数经典数学所依赖的析取和存在进行唯心主义解释。为了建设性地开展工作，我们需要从经典解释回归到自然的建设性解释：

∨（或）：为了证明 P∨Q，我们必须要么有 P 的证明，要么有 Q 的证明。

∧（和）：为了证明 P∧Q，我们必须同时拥有 P 的证明和 Q 的证明。

⇒（隐含）：P→Q 的证明是一种将 P 的任何证明转换为 Q 的证明的算法。

Ø（非）：为了证明ØP，我们必须证明P意味着0=1。

∃（存在）：为了证明 ∃xP(x)，我们必须构造一个对象 x 并证明 P(x) 成立。

∀（对于每个/全部）：∀x∈SP(x) 的证明是一种算法，应用于任何对象 x 和证明 x∈S 的数据，证明 P(x) 成立。

这些 BHK 解释（该名称反映了它们起源于 Brouwer、Heyting 和 Kolmogorov 的著作）可以使用 Kleene 的可实现性概念变得更加精确；参见（Dummett [1977/2000]，222-234；Beeson [1985]，第七章）。

有一个常见的误解，认为构造性数学只是没有矛盾证明的数学（反证法论证）。事实并非如此。考虑典型的证明

√

2

是非理性的：这些都是从假设 '

√

2

是理性的”，然后通过基本的、完全建设性的步骤来得出矛盾。这样的程序是一个完美的建设性证明

√

2

不理性；事实上，“Øp”的建设性解释恰恰是假设p会导致矛盾。本段开头提到的误解是由于将否定陈述的证明（如前述）与以下类型之一混淆而引起的：假设 Øp，导出矛盾，并得出 p 必须成立的结论。从建设性的角度来看，从后一类证明中最多可以获得的结论是 Øp；最后一步，声称 p 必须成立，是非建设性的。

为了强调这一点，请考虑以下形式的证明

假设不存在 boojum 这样的东西；然后进行建设性辩论以得出矛盾。

这样的证明通常不包含使我们能够建设性地证明存在 boojum 的算法信息。更正式地说， ØØ∃xP(x) 的构造性证明并不自动让我们得出 ∃xP(x) 的结论。

总结一下：为了证明 Øp，我们通常可以假设 p 并导出矛盾。为了证明 p，仅仅假设 Øp 并导出矛盾是不够的。

现在我们转向实践中的直觉逻辑。如果我们认真地以这样一种方式发展数学，即当一个定理断言具有属性 P(x) 的对象 x 存在时，那么该定理的证明就体现了构造 x 和通过任何必要的计算来证明 x 具有属性 P(x)。这里是一些定理的例子，每个定理后面都有对其构造性证明的要求的非正式描述。

对于每个实数 x，x=0 或 x≠0。

证明要求：一种应用于给定实数 x 的算法，可确定 x=0 或 x≠0。请注意，为了做出此决定，算法可能不仅使用描述 x 的数据，还可能使用显示 x 实际上是实数的数据。

上面有界的 R 的每个非空子集 S 都有一个最小上界。

证明要求：一种算法，应用于实数集合 S、S 的成员 s 以及 S 的上限，

计算对象 b 并显示 b 是实数；

表明对于每个 x∈S，x≤b；和

给定实数 b′＜b，计算 S 的元素 x，使得 x＞b′。

如果 f 是闭区间 [0,1] 上的连续实值映射，使得 f(0)⋅f(1)＜0，则存在 x 使得 0＜x＜1 且 f(x)=0 。

证明要求：一种算法，应用于函数 f、f 的连续模以及值 f(0) 和 f(1)，

计算对象 x 并显示 x 是 0 到 1 之间的实数；和

表明 f(x)=0。

如果 f 是闭区间 [0,1] 上的连续实值映射，使得 f(0)⋅f(1)＜0，则对于每个 ε＞0，存在 x 使得 0＜x＜1 且 | f(x)|＜ε。

证明要求：一种算法，应用于函数 f、f 的连续模、值 f(0) 和 f(1) 以及正数 ε，

计算对象 x 并显示 x 是 0 到 1 之间的实数；和表明|f(x)|＜ε。

我们已经有理由怀疑 (A) 是否有建设性的证明。如果可以满足 (B) 的证明要求，那么，给定任何数学陈述 P，我们可以应用 (B) 的证明来计算集合的上界 σ 的有理近似 z

S={0}∪{x∈R:P∧x=1}

误差＜1⁄4。然后我们可以确定是否 z＞1⁄4（在这种情况下 σ＞0）或 z＜3⁄4（在 σ＜1 时）。在第一种情况下，存在 x∈S 且 x＞0，因此我们必须有 x=1，因此 P。在 σ＜1 的情况下，我们有 ØP。因此(B)蕴含着排中律。

然而，在Bishop的实数构造性理论中，基于预先指定收敛速度的柯西序列，我们可以证明以下构造性最小上界原理：

令 S 为上面有界的 R 的非空子集。那么 S 具有最小上界当且仅当它是上序定位的，即对于所有实数 α，β 且 α＜β，要么 β 是 S 的上界，要么存在 x∈S 且x＞α（Bishop & Bridges [1985]，第 37 页，命题 (4.3)）。

顺便提及，我们提到基于区间算术的 R 构造性理论的另一种发展；参见 Bridges & Vîşă [2006] 第 2 章。

陈述（C）和（D）在经典上是等价的，都是中值定理的一个版本。在这些陈述中，f 的连续性模是正实数有序对 (ε,δ) 的集合 Ω，具有以下两个属性：

对于每个 ε＞0 都存在 δ＞0 使得 (ε,δ)εΩ

对于每个 (ε,δ)εΩ，以及对于所有 x，y∈[0，1] 且 |x−y|＜δ，我们有 |f(x)−f(y)|＜ε。

陈述 (C) 包含另一个本质上非建设性的原则，即全知次要有限原则 (LLPO)：

对于每个最多有一项等于 1 的二进制序列 (a1，a2，…)，对于所有偶数 n，an=0 或对于所有奇数 n，an=0。

陈述（D）是（C）的弱形式，可以使用标准类型的区间减半论证进行建设性证明。使用近似区间减半论证证明了以下更强的构造性中间值定理，该定理足以满足大多数实际目的：

令 f 为闭区间 [0,1] 上的连续实值映射，使得 f(0)⋅f(1)＜0。还假设 f 局部非零，即对于每个 x∈[0,1] 且每个 r＞0，存在 y 使得 |x−y|＜r 且 f(y)≠0。那么存在 x 使得 0＜x＜1 且 f(x)=0。

中间值定理的情况是许多构造性分析中的典型情况，其中我们发现一个经典定理具有多个构造性版本，其中一些或全部在经典逻辑下可能是等效的。

有一种全知原理，其建构地位不如 LPO 和 LLPO 明确，即马尔可夫原理（MP）：

对于每个二元序列（an），如果矛盾所有项a都等于0，则存在等于1的项。

这个原理等价于一些简单的经典命题，包括：

对于每个实数x，如果x等于0是矛盾的，则x≠0（在我们前面提到的意义上）。

对于每个实数x，如果x等于0矛盾，则存在y∈R使得xy=1。

对于每个一对一连续映射 f:[0,1]→R，如果 x≠y，则 f(x)≠f(y)。

马尔可夫原理代表了无界搜索：如果你有证据证明所有项 a 为 0 都会导致矛盾，那么，通过依次测试项 a1,a2,a3,…，你一定会遇到等于 1 的项;但这种保证并不保证你会在宇宙终结之前找到所需的期限。大多数构造性数学的实践者即使不是完全怀疑，至少也持怀疑态度。克里普克模型表明 MP 不可建设性地推导，这一观察结果强化了这种观点（Bridges & Richman [1987], 137–138。）

3. 构造性数学的种类

保留计算解释可能性的愿望是使用我们上面给出的逻辑连接词和量词的建设性重新解释的动机之一；但这并不完全是数学建构主义先驱的动机。在本节中，我们将探讨过去 130 年来数学建构主义的一些不同方法。

3.1 直觉数学

十九世纪末，某些人——尤其是克罗内克和庞加莱——对同时代的一些人所使用的唯心主义、非建设性方法表示怀疑，甚至不赞成。但这是在 L.E.J. 的争论性著作中。 Brouwer（1881-1966）从他的阿姆斯特丹博士论文 Brouwer [1907] 开始，并在接下来的四十七年中继续，为精确、系统的构造性数学方法奠定了基础。在布劳威尔的直觉主义哲学中，数学是人类思想的自由创造，当且仅当它可以被（精神上）构造时，一个对象才存在。如果一个人采取这种哲学立场，那么一个人就会不可避免地被上述逻辑联结词和量词的建设性解释所吸引：因为证明某个对象x不存在的不可能性怎么能描述x的心理构造呢？

布劳威尔并不是他的思想最清晰的阐释者，正如下面的引文所示：

当时间流逝所产生的二元性主题被从所有特殊事件中抽象出来时，数学就出现了。所有这些二元性的共同内容所剩下的空形式[n与n+1的关系]成为数学的原始直觉，并无限地重复创造新的数学学科。 （引自 Kline [1972], 1199–2000）

Errett Bishop 给出了 Brouwer 观点的现代版本（Bishop [1967]，第 2 页）：

数学最关心的是数字，这意味着正整数。我们对数字的感受就像康德对空间的感受一样。正整数及其算术是由我们智力的本质所预设的，而且我们很容易相信，也是由一般智力的本质所预设的。正整数从单位的原始概念、邻接单位的概念以及数学归纳过程的发展具有完全的说服力。用克罗内克的话说，正整数是上帝创造的。

无论布劳威尔的著作多么晦涩难懂，有一点总是很清楚的：对他来说，数学优先于逻辑。有人可能会说，正如赫尔曼·韦尔在下一段中所做的那样，布劳威尔认为经典数学的缺陷恰恰在于它对经典逻辑的使用，而没有参考基础数学：

根据布劳威尔的观点和对历史的解读，经典逻辑是从有限集及其子集的数学中抽象出来的。 ……忘记了这一有限的起源，后来人们误认为该逻辑高于并先于所有数学，并最终在没有理由的情况下将其应用于无限集的数学。这是集合论的堕落和原罪，它因此受到了二律背反的公正惩罚。令人惊讶的并不是这种矛盾的出现，而是它们在比赛的后期才出现。 （韦尔[1946]）

特别是，这种对逻辑的滥用导致了非建设性的存在证明，用韦尔的话说，“告诉世界宝藏存在而不透露其位置”。

为了描述直觉主义数学家使用的逻辑，必须首先分析心灵的数学过程，从中可以提取逻辑。 1930 年，布劳威尔最著名的学生阿伦德·海廷 (Arend Heyting) 发表了一套形式公理，这些公理如此清晰地描述了直觉主义者所使用的逻辑，以至于它们被普遍称为直觉主义逻辑公理 (Heyting [1930])。这些公理捕捉了我们之前给出的连接词和量词的非正式 BHK 解释。

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