数学里的构造主义与直觉主义（一） (3-1)

¬(p∧¬p)

翻开数学史的书籍，构造主义仿佛是二十世纪初期的一股叛逆思潮。它曾经很酷，但是却缺乏主流数学家的关注，甚至遭到批判。本文试图梳理一下构造主义的脉络，始于构造主义，终于 univalence axiom (i.e. homotopy type theory).

§-1. 构造主义和直觉主义

用过分简单的话讲，构造主义的核心就是 “要证明一个东西存在，必须把它构造出来”。这直接否定了人们熟悉的反证法。把反证法拿走，后果有多严重呢？

从某些层面上讲，它并没有人们想象的那么严重——只要澄清了一些概念并且做一些仔细地重新叙述，有些用反证法证明的命题其实并不需要反证法：比如欧几里得仔细选取的对 “素数有无穷个” 这个命题的陈述，本质上说的是

任意一个有限集合到素数的集合都存在一个单射。

完全避开了 “无穷” 的概念这一蹚浑水。（从欧几里得对平面几何第五公理的谨慎态度也可以理解，他绝对不会用 “素数有无穷个” 这种描述。）

“√2是无理数” 这个命题，也可以转化为

对任意的自然数m，n，我们有m²＞2n²或者m²＜2n².

并且可以构造性地证明（证明比一般的用反证法证明稍微冗长些）。

在另一些层面上，构造主义带来的困难则大得多——构造主义的一支，布劳威尔（L. E. J. Brouwer）的直觉主义直接要求 "there exists" 被解读为 'there can be constructed', 也就是说 'we can compute'. 这直接导致了了以下的 “神逻辑”:

(★)对于数列(αₙ)，即使 “∀n，αₙ＝0（对任意的n，αₙ＝0）” 这一命题不成立，我们也不能得出∃n，αₙ ≠ 0（“存在” n使得αₙ ≠ 0）

因为——虽然在非直觉主义的意义下有这么一个n，但是这个n并不是被构造出来的。没有 “算法” 告诉你怎么计算出这个n.

§0. 如何解读神逻辑

要理解这个神逻辑，不能拘泥于 “存在” 这两个字在自然语言中的字面意思，而是把 “∃” 这个量词 (quantifier) 看做一个纯粹的符号，再接受布劳威尔对这个词的解读——换句话讲建构在直觉主义上的数学和逻辑，其实是我们熟悉的那套东西的一个兄弟，只是 “∃” 这个基因发生了一点变异。

由于 “∃” 的变异，直觉主义的数学发展相比迟缓。因为，(★)直接否定了数学中一个常用的逻辑命题——排中律！排中律的陈述很简单：

对于任意的命题P，P∨¬P成立。（也就是说，P或非P总有一个成立。）

加上量词的版本更能体现排中律和(★)的不可调和之处——加上量词的排中律是这样的：

¬(∀x. Px) ⇒ ∃x.(¬Px).

用直觉主义的方式来阐释 “∃”, 显然无法接受排中律——即使我们否定了 “对任意的x，都有Px” 这一命题，我们也不能算出一个使得Px不成立的x.

把排中律抽走，对直觉主义的数学影响有多大呢？很大：

（注意：这里原文有误，已修改）由 Diaconescu's theorem 排中律是选择公理的推论，抽走排中律，选择公理也不能成立，这就抽走了很多现代数学里最重要的引理，动摇了很多比较现代的理论的基石——

1. 分析上，没有排中律，不能得出∀x∈ℝ，(x＝0)∨(|x|＞0)（即使知道x＝0不成立也不能推出的x绝对值大于0.）类似地，也没有中值定理。

2. 代数上，没有选择公理，甚至不能证明任意一个环的存在极大理想！

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。