从心理学的观点来看，学习构造性数学是痛苦的，因为它要求首先忘却从经典数学训练中取得的特定而深刻的直觉与习惯。在《论死亡和濒临死亡》中，心理学家伊丽莎白·库伯勒·罗斯确立了人们接纳生命创伤事件的五步：拒绝、愤怒、挣扎、沮丧以及接纳。我们仿此循途。

拒绝

我曾遇见过一些视构造主义数学如胡诌的数学家，因为他们误解了构造主义者的言论，或曰他们只是犯了简单的逻辑错误。让我们首先处理这类误解。

排中律.

构造主义数学是没有排中律的数学：

对于任意命题 $P$，$P$ 或非 $P$。

这并不是说我们否认这规律，而是我们只会在已被我们证明的情况下使用。第一个好练习是从 Peano 公理中证明任意两个自然数要么相等，要么不等。

排中律也被称为 “the law of excluded third"，或者拉丁文 “tertium non datur"。某人可能会错误地认为构造主义者承认一种 “第三” 可能性:

存在一个命题 $Q$ 既非真也非假。

此陈述以构造观点看为假，因为它声称 $\neg Q$ ($Q$ 非真) 以及它的否定 $\neg \neg Q$ ($Q$ 非假) 都成立，而这因如下无矛盾律 是不可能的：

不存在命题 $P$ 使得 $P$ 且 $\neg P$。

我们证此如下，注意在构造主义数学中 $\neg P$ 是 $P \Rightarrow \perp$ 的简写：

假定存在命题 $P$ 使得 $P$ 且 $\neg P$。因为 $\neg P$ 只是 $P \Rightarrow \perp$，我们用分离规则 (modus ponens) 得出 $\perp$。至此我们得出矛盾，因此不存在如是 $P$。

顺便一提，这不是反证法 (a proof by contradiction)，而是归谬法 (a proof of negation)，我们接下来将一一解释。

反证法与归谬法.

反证法，或者拉丁文 “reductio ad absurdum"，是如下推理原则：

如果一个命题 $P$ 非假，那么它真。

就符号形式而言，它声称 $\neg \neg P \Rightarrow P$ 对任意命题 $P$ 成立，而这等价于排中律。令人疑惑的是，数学家们把任何从一个确信为假的陈述出发，得出矛盾的论断称作 “反证法”，但是却有两种推理原则具备这种形式。其一确是通过矛盾而得出的证明，它形如

假定 $\neg P$，…… (导向矛盾的论述) ……，所以 $P$。

然而另一个却是否命题如何被证明的：

假定 $P$,…… (导向矛盾的论述) ……，所以 $\neg P$。

因为 $\neg P$ 是 $P \Rightarrow \perp$ 的缩写，证明否命题只是证明蕴含关系 $P \Rightarrow Q$ 的一个实例：假定 $P$ 并推出 $Q$。诚然，这两个论述看起来差不多，但是注意在其中一种情况中，结论消去了否定，而另一种却加上了否定。除非我们已然确信 $\neg \neg P \Leftrightarrow P$，否则我们不能通过交换 $P$ 与 $\neg P$ 以此推彼。这实在是不同的推理原则。

一些用到归谬法的著名证明有 $\sqrt{2}$ 的无理性、Cantor 对不存在某集到其幂集双射的对角线论证，以及 Russell 证明不存在全体集合构成的集合这一二律背反。因此这些都是完完全全构造地有效定理。为确信起见，让我们构造性地证明 Russell 定理。

这确实是一个归谬法证明：我们假定全体集合构成的集合存在，然后推出矛盾。我们可以把如上两个观察视为排中律 (要么 $R \in R$ 要么 $R \notin R$) 的应用，然而我们不必如此！

接下来的证明经常表现为排中律应用的典范。

正如此例，这例子选得并不好，因为分出两种情况并不本质。$\sqrt{2} ^ {\sqrt{2}}$ 是一个无理数，此事证明起来并不简单，因此我们应当立即采取第二种方案。这儿有一个构造性证明：

当然，$\log_2 9$ 的无理性也需证明，但是这个证明并不比证明 $\sqrt{2}$ 的无理性困难。

选择公理 (Axiom of choice)

在构造性数学中我们无法承认选择公理，因为它蕴含了排中律。为证之，我们需要一点点集合论。回忆无序对 $\{a, b\}$ 是元素等于 $a$ 或等于 $b$ 的集合： $$\{a, b\} = \{x \mid x = a \lor x = b\}.$$

因此为证 $P(x)$ 对全体 $x \in \{a, b\}$ 都成立，考察 $P(a)$ 和 $P(b)$ 足矣。

在构造主义数学中，我们需要谨慎对待选择公理的公式表达，因为非空集 (nonempty set)，即使得 $\neg (A = \emptyset)$ 的集合 $A$ 和有物集 (inhabited set)，即满足存在 $x \in A$ 的集合 $A$ 之间是有差别的。选择公理说的是任意一族有物集有一个选择函数。

构造主义数学有不同的品味，有些采纳可数选择：一族被自然数标号的有物集有一个选择函数。这种形式的选择对许多在分析学中遇到的问题足够用了，所以并不是一切都逝去了。我们稍后将讨论没有选择公理的数学。现在让我们来看看一个很容易避免，但典型的无意用到选择的应用。

你能指出用了选择公理的那个应用吗？它正好就在第一句里，如其言 “对所有 $x \in X$，取 $\varepsilon_x > 0$”。映射 $x \mapsto \varepsilon_x$ 是一个选择函数。这般隐现的选择常出现在我们引入新符号和用下标表示依赖关系的时候，在我们的例子中便是 $\varepsilon_x$。要是我们以 “对所有 $x \in X$，存在 $\varepsilon > 0$” 开始，我们就不会作任何选择了，但是我们已然会被卡住。这种情况的补救方法很简单：别选！

在进入下一幕之前，让我们先澄清最后一种误解。假设在某段数学文本中，我们假定存在 $x$ 使得 $\phi(x)$。我们习惯说 “选择一个满足 $\phi(x)$ 的 $x$” 来给自己这样一个满足 $\phi$ 的 $x$。这并不是选择公理的应用，而是存在量词的消去。类似地，如果我们知道一个集合 $A$ 有物并且说 “选取 $x\in A$”，这不是选择，而也是存在量词的消去。

看起来构造主义数学也并非完全不可理解：构造主义者不否认排中律，但对它持矛盾态度；他们同意不存在既真又假的命题，也不存在非真非假的命题；他们允许使用否定，并通过得出矛盾来证明否定；他们认为某些形式的选择是可以接受的。我们也不得不承认，只要稍加注意，某些排中律和选择的情况是可以消除的，或者只是由于逻辑训练不足而产生的错觉。

愤怒

构造主义者可能是自洽的，但我们仍然记得 David Hilbert 于 1927 年说过的话 [31]:

从数学家们那里拿走排中律就如同，例如，取缔天文学家的望远镜或是禁止拳击手用他的拳头。禁止存在性陈述以及排中律等同于一并放弃数学的科学。因为同现代数学的浩渺无垠相比，那些可怜的残余，那些直觉主义者不使用逻辑的 $\epsilon$-律而获得的不完整、无关的孤立结果，又算得了什么呢？¹

Hilbert 的回击是成功的，因为当时他是对的。直觉主义者事实上只做出了 “少许孤立的结果”，而且因讨论含糊不清的 “选择序列 (choice sequences)”、强调 “所有函数都连续” 把事情弄得更糟。以 A. A. Markov 为首的俄罗斯构造主义者证明了一些让数学分析闹笑话的定理，例如在构造主义者的频道里存在一个无界连续映射 $[0,1] \to \mathbb{R}$，使问题更加复杂。

在更广泛的数学界里鲜为人知的是，事情在 1967 年即 Brouwer 死后那年，起了变化，当时 Erret Bishop 出版了一本关于构造主义分析的书 [5]。这项重要的工作被 Michael Beeson 描绘得最好 [4]：

Bishop 工作的要旨是 Hilbert 和 Brouwer 在一个他们一致同意的关键点上都错了。即他们都认为如果一个人认真对待构造主义数学，那么便必要“放弃”现代数学最重要的部分 (例如测度论和复分析)。Bishop 指出这根本是错的，并且根本没必要引入一些在初学者看起来矛盾的不寻常假设。能量与安全性之间的冲突完全是虚幻的！我们只需优雅的步履，而非 Hilbert 的 “拳击手之拳”。

这怎么可能呢？基数的良序、极大理想的存在性、向量空间基的存在性、Hilbert 的零点定理、区间的紧性、中值定理、Tychonoff 定理以及其他种种基本定理都或多或少需要排中律和选择公理。Erret Bishop 是怎么实现不可能的？为什么构造主义者还存在？

历史性的讨论很有意思，但是一个良好推理出来的数学表达更具真正的力量。不存在拒绝有限集的子集也有限这一事实的理智数学家，对吧？

显然，构造主义者认为一个有限集的子集并不必是有限的。粗略的文献检索揭示了构造主义数学中另一些奇怪的论断：“$\mathbb R$ 测度为零” [28, §6.4.3]，“存在没有聚点的单调递增有界序列” [26]，“序数构成一个集合” [22]，“存在 $\mathbb{N} ^ \mathbb{N}$ 到 $\mathbb N$ 的单射” [3]，如此种种。

构造主义者可能指出，什么东西奇怪是很主观的，并提醒我们曾几何时非欧几何被束之高阁、Weierstrass 的处处连续无处可导函数曾是，且仍是一个奇观、而 Banach-Tarski 关于分球的定理甚至时至今日仍被叫作 “悖论”。不过，我们需要的是对构造主义的数学解释，而非历史教训和主观意见。

挣扎

经典数学的训练把排中律深深植入年轻学生的脑海中，以至于大部分数学家甚至不能感知到证明中排中律的存在。为了获得对构造主义立场的某种理解，我们应当提供一种手段来悬置对排中律的信任。

如果几何学家不信 Euclid 的第五公设 (Euclid’s fifth postulate)，那么他们可能会发现非欧几何的某种模型很有帮助 —— 一种人为更改过 “线” 与 “点” 的概念而使得平行公设失效的几何世界。我们的处境与之比较，只不过更加基础，因为我们需要转变对 “真理 (truth)” 本身的理解。我们无法对构造性世界进行完整的数学描述，但我们仍然可以提炼出其本质，只要我们记住重要的技术性问题被省略了就可以了。

经典数学.

值得指出，构造主义数学是对经典数学的一般化，正如被 Fred Richman [21] 所强调的那样，避免了排中律和选择的证明仍然是一个经典性证明。然而，试图在经典数学中学习构造主义思想，就像通过学习 Abel 群来学习非交换代数一样。

可实现性 (Realizability).

在我们第一个实在的构造主义世界里，只有可计算的才是真的。让我们像程序员一样想象一下，数学对象在计算机中被表示为数据，而函数便是对数据进行运算的程序。进一步，一个逻辑论断只有在被一个程序见证 (witnessing) 它的真时才是有效的。我们称这样的程序为实现子 (realizers)³，同时，我们称这样一个论断被它们实现。Brouwer-Heyting-Kolmogorov 律揭示了一个程序怎样实现一个论断：

1. 谬误 $\bot$ 不会被任何东西实现；

2. 真 $\top$ 被选取的常量实现，例如 $\star$；

3. $P \land Q$ 被一个序对 $(p,q)$ 实现，其中 $p$ 是 $P$ 的实现子，$q$ 是 $Q$ 的实现子；

4. $P \lor Q$ 被 $(0, p)$ 实现，其中 $p$ 是 $P$ 的实现子，或被 $(1, q)$ 实现，其中$q$ 是 $Q$ 的实现子；

5. $P\Rightarrow Q$ 被一个将 $P$ 的实现子映到 $Q$ 的实现子之程序实现。

6. $\forall x \in A. P(x)$ 被一个将任意 $a\in A$ 映到 $P(a)$ 的实现子之程序实现；

7. $\exists x \in A. P(x)$ 被一个序对 $(p, q)$ 实现，其中 $p$ 表示某些 $a \in A$ 且 $q$ 实现 $P(a)$；

8. $a=b$ 被同时表示 $a$ 和 $b$ 的 $p$ 实现。

此律适用于任何合理的 “程序” 概念。图灵机可以，而量子计算机和程序员实实在在写出来的程序也可以。为适应实现子，我们来解释一下如下命题的计算性意义：

对任何自然数都存在比它大的素数。

这是一个 “对任意” 式的论断，所以它的实现子是一个以自然数 $n$ 为输入，并输出 “存在比 $n$ 的素数” 的实现子之程序，也就是一个序对 $(m, p)$，其中 $m$ 是一个自然数，而 $q$ 实现 “$m$ 是素数且 $m > n$”。如果我们忘却 $q$，则把 $p$ 视为本质上计算任意大素数的程序。因为这样的程序存在，所以在可计算世界里存在任意大的素数。

一个更加有趣的例子是这个论断

$$\forall x \in \mathbb{R}. x = 0 \lor x \neq 0.$$

如果我们把实数定义为有理数的 Cauchy 完备，那么一个实数 $x \in \mathbb R$ 被一个输入 $k \in \mathbb N$，输出满足 $\mid x - r_k \mid \leq 2^{-k}$ 的有理数 $r_k$ 之程序表示。因此上式的实现子是如下程序 $q$：接受任意 $x\in\mathbb R$ 的表示 $p$，并输出或者满足 $s$ 实现 $x=0$ 的 $(0, s)$，或者满足 $t$ 实现 $x\neq0$ 的 $(1, t)$。