构造性数学（一）

一、简介

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 成立，则为 0

1 如果 Ø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 并导出矛盾是不够的。

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