希尔伯特 vs 布劳威尔：形式主义 vs 直觉主义

对话背景#

这场对话依据 1920 年代基础论争（Grundlagenstreit）中双方已发表的讲演、论文与公开冲突来编排，不是一次对坐的会谈。大卫·希尔伯特（David Hilbert, 1862–1943）要把古典分析保住：形式化，再用有限手段证明不矛盾。1925 年明斯特讲演《论无穷》里那句「没有人能把我们从康托尔创造的乐园里驱逐出去」，针对的就是当时的「革命」。

鲁伊兹·埃格伯特斯·扬·布劳威尔（L.E.J. Brouwer, 1881–1966）从 1907 年学位论文起就把数学写成心灵的构造：对象必须能被构造，排中律（$P \lor \neg P$）不能自动用于无穷，实无穷不是已完成的仓库。

导火索往往被记成外尔。希尔伯特的学生赫尔曼·外尔 1921 年发表《论数学的新基础危机》，倒向布劳威尔，称其为「革命」。希尔伯特 1921 年夏在汉堡三场讲演、1922 年《数学的新奠基》公开反击。

争论在 1928 年变成人事：希尔伯特出席博洛尼亚国际数学家大会，布劳威尔反对德国数学家在那种政治条件下出席；同年 10 月希尔伯特把布劳威尔从《数学年刊》编委会除名。爱因斯坦对玻恩说，这是「蛙鼠之战」（Frosch-Mäusekrieg），自己保持中立。哥德尔 1931 年的定理改写了棋盘，但论争的高峰在那之前。本篇轴线是直觉主义与形式主义，不是不完备。

第一幕：数学的本质#

希尔伯特：布劳威尔先生，从最基本的问题开始：数学是什么？我要把古典数学写成可以检查的形式系统：公理、推理规则、定理。理想元素不必先在本体论上「存在」，它们是符号。外尔把这说成「按固定规则进行的公式游戏」。游戏二字是他的贬义，不是我的投降。

布劳威尔：希尔伯特先生，数学是心灵里的构造。对象只有被一步步做出来才在。证明不是改写一串无意义的符号，是一种可以内省的活动。外尔 1921 年看清的正是这一点：一致性是必要的，远远不够。一堆不崩的公式，不必是数学。

希尔伯特：心灵活动是私人的。不同的人可以「看」出不同的东西。要客观，只能把步骤写成任何人都能核验的规则。您的「直觉」一旦拒绝排中律，分析学里现成的定理就会成批消失。那不是基础，是政变。

布劳威尔：形式系统提供的是变换许可，不是意义。一份语法正确的推导，可以不对应任何构造。意义来自对时间中展开的构造的直觉，不是来自印刷出来的公理表。

第二幕：排中律的争议#

希尔伯特：布劳威尔先生，你拒绝排中律——对任何命题 $P$，$P \lor \neg P$。这是经典数学的骨架。拒绝它，等于拒绝现成的分析与存在性证明。

布劳威尔：有限情形里它成立。命题若只关于一个可检查完的有限域，穷举会给出 $P$ 或 $\neg P$。无穷域里没有这份穷举。此时再断言 $P \lor \neg P$，是在尚未构造判决时，把判决说成已经到手。

希尔伯特：请举一个例子。

布劳威尔：取 $P$：「$\pi$ 的十进制展开里出现连续一百个 7。」没有人交出这段展开，也没有人证明它永不出现。断言 $P \lor \neg P$，并不多给我们一个构造，只是把「尚未知道」说成已经二值。

希尔伯特：但 $P$ 要么为真要么为假——即使我们不知道哪个。这是逻辑的最低要求，不是一种数学口味。

布劳威尔：在直觉主义里，「真」意味着我们有构造。没有构造，$P$ 不是真的，也还不是假的。假，要有把 $P$ 导向矛盾的构造。中间那一大片不是第三值的神秘主义，是尚未完成的工作。

第三幕：非构造性证明#

希尔伯特：布劳威尔先生，让我举一个非构造性证明的例子。定理：存在两个无理数 $a$ 和 $b$，使得 $a^b$ 是有理数。证明：考虑 $\sqrt{2}^{\sqrt{2}}$。如果它是有理数，取 $a = b = \sqrt{2}$。如果它是无理数，取 $a = \sqrt{2}^{\sqrt{2}}$，$b = \sqrt{2}$——那么 $a^b = (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^2 = 2$，是有理数。

布劳威尔：这个证明是无意义的！它没有告诉我们 $a$ 和 $b$ 是什么——它只是证明了"存在"。在直觉主义中，"存在"意味着"可以构造"——如果你不能构造 $a$ 和 $b$，你就没有证明存在。

希尔伯特：但这个证明是完全正确的！它使用了排中律——$\sqrt{2}^{\sqrt{2}}$ 要么是有理数要么是无理数——然后分别讨论两种情况。两种情况都把「存在」送到手。逻辑不要求我们先指出是哪一只手。

布劳威尔：这正是问题所在。你讨论两种情况，却不知道哪一种是实际的。对象没有被交出来，只被「存在」这个词盖住。这不是数学，是对尚未完成的构造提前开收据。

希尔伯特：这不是赌博——这是逻辑。如果两种情况都导致结论，那么结论必然成立——不管哪种情况是实际的。

布劳威尔：但你没有构造任何东西——你只是证明了一个"存在"命题。在直觉主义中，这不是有效的数学。

第四幕：无穷的性质#

希尔伯特：布劳威尔先生，让我谈谈无穷。我认为实无穷——已完成的无穷整体——是数学的基本对象。自然数集、实数集、函数空间——这些无穷集合是现代数学的基础。

布劳威尔：我拒绝实无穷。无穷是永远进行的过程，不是已经装进仓库的整体。我可以构造 1, 2, 3, ……，不能把「所有自然数」当成一个完成了的对象。连续统更是如此：它由选择序列展开，每一项可以依法给出，也可以自由选取。正在生成的连续统，不是康托尔那条已完成的实数直线。

希尔伯特：没有实无穷，分析学就站不住。完备性、连续函数、测度——都把无穷集合当对象。您 1911 年的不动点定理，自己也用了经典工具。现在却要数学家把这些工具交回去。

布劳威尔：定理可以有经典的外壳。基础不能靠外壳。直觉主义分析只用能被构造的对象：自然数、有理数、由定律或选择序列给出的实数。连续统是生成，不是库存。

希尔伯特：但这种分析学是贫乏的——它不能证明许多经典定理。

布劳威尔：它能证明所有有意义的定理。那些不能在直觉主义中被证明的定理——它们的意义是什么？如果一个定理不能被构造性地证明，它就是一个关于不可构造对象的断言——这种断言没有数学意义。

第五幕：希尔伯特纲领 vs 直觉主义#

希尔伯特：布劳威尔先生，让我谈谈我的纲领。我相信：全部数学可以被形式化——建立在有限的、一致的公理系统之上。更重要的是，我可以用元数学——关于数学的数学——来证明这个系统的一致性。

布劳威尔：你的纲领有两块：（1）数学可以被完全形式化；（2）有限的元数学能证明一致性。1920 年代我反对的是第一块里的「意义被抽空」，以及第二块里「有限」被说得太轻易。哥德尔后来才来——他改的是棋盘，不是我们这场争论的开场。

希尔伯特：为什么第一块错？形式化并不禁止人去理解。它只要求：理解若要被公共检查，必须落成符号变换。

布劳威尔：检查可以是形式的，数学本身不是。海廷日后会把直觉主义逻辑写成演算；那是学生的翻译，不是我把心灵活动交给印刷机。第二块同样可疑：你对任意长符号序列做推理，已经在用一种完成了的无穷。

希尔伯特：有限立场只承认纸上写得完的东西。任意长不是「无穷集合已经在手」，是「这一次写到哪里，就检查到哪里」。这与您的选择序列不是一回事。

第六幕：数学的可靠性#

希尔伯特：布劳威尔先生，你的直觉主义数学是可靠的——因为它只使用构造性的方法。但它是贫乏的——它拒绝了大部分现代数学。你是在为了可靠性而牺牲内容。

布劳威尔：而你的形式主义数学是丰富的——它包含了大量的非构造性定理。但它是不可靠的——它使用了排中律和实无穷，这些概念可能导致矛盾。

希尔伯特：我不相信会导致矛盾。我相信经典数学是一致的——我愿意用我的纲领来证明它。

布劳威尔：没有发现矛盾，不等于证明了没有矛盾。外尔已经说过：一致性必要，不够。一套永不崩的公式，仍可能不对应任何构造。

希尔伯特：经典数学用了一代人，没有崩。我愿意把「没有崩」变成定理。这才是纲领。

布劳威尔：把「尚未崩」说成已经担保，是另一种排中律：要么已有矛盾，要么永远没有。中间那一大片，仍是尚未完成的工作。

第七幕：被驱逐的威胁#

布劳威尔：希尔伯特先生，1928 年 10 月您让布卢门塔尔转告：我的名字将从《数学年刊》封面拿掉。理由写成「根本观点无法共事」。博洛尼亚大会上您出席、我反对德国数学家在那种条件下出席——这些和政治、和编辑部日常并不相同。把它们捆成一次除名，是人事，不是证明。

希尔伯特：我不能与您同在一个编委会。若数学家接受您对排中律的禁令，分析学将成批交回。《数学年刊》是当时主要的数学期刊，不能变成这场革命的机关报。

布劳威尔：这是用编辑权结束一场应当在论文里打完的仗。爱因斯坦不肯副署，还把这叫做蛙鼠之战。他可以中立。被除名的人不能把中立当成论证。

希尔伯特：中立解决不了基础。基础要么保住康托尔的乐园，要么按您的禁令拆迁。我选前者。直觉主义可以当哲学课，不能当数学的警察。

第八幕：两种数学#

布劳威尔：希尔伯特先生，让我尝试理解你的立场。你相信：数学是一种形式游戏——公理和推理规则定义了数学的内容。数学对象不需要"存在"——它们只是符号。

希尔伯特：正确。数学的可靠性来自形式系统——不是来自直觉。如果一个系统是一致的，它就是可靠的——不管它是否有"意义"。

布劳威尔：而我相信：数学是心灵的构造——数学对象只有在能被构造时才存在。一个定理是"真的"意味着我们有一个构造性的证明。没有构造性证明的定理不是"真的"——它只是"在某个形式系统中可证明的"。

希尔伯特：这是否意味着你拒绝反证法？

布劳威尔：我接受一种有限形式的反证法——如果假设 $P$ 导出矛盾，那么 $\neg P$ 成立。但我拒绝用反证法证明存在命题——如果假设"不存在 $x$"导致矛盾，这不能证明 $x$ 存在——它只能证明"不存在 $x$"是错误的，但不能构造 $x$。

希尔伯特：这种限制会使得数学变得极其困难。

布劳威尔：但也会使得数学变得更加可靠和有意义。

第九幕：遗产与影响#

希尔伯特：布劳威尔先生，你的学生海廷 1930 年把直觉主义逻辑写成形式规则。那已经是一种演算。你接受这种翻译吗？

布劳威尔：海廷是学生。演算可以让外人看见哪些推理被允许。它不是原作。原作是心灵里的构造，不能被封面和编委会保管。外尔 1921 年倒向我，伤的是您的师门，不是因为我抢了年刊。

希尔伯特：外尔是我的学生，他喊「革命」的时候，我必须回答。回答写成了证明论，也写成了除名。两者不该被说成同一件事，它们确实发生在同一十年。

布劳威尔：哥德尔的 Dialectica 解释、贝斯的实现性，后来都从构造这边借路。那是后人的翻译史。1928 年我们争的是：排中律能不能对无穷生效，康托尔的乐园要不要拆迁。

希尔伯特：乐园留下了。大多数数学家仍用排中律。您赢的是另一块地：谁若坚持「存在即构造」，就必须走您的路，不能再假装经典存在证明已经给出对象。

分析#

基础论争的高峰在 1921–1928 年：外尔倒戈、汉堡讲演、博洛尼亚、年刊除名。爱因斯坦的「蛙鼠之战」说的是人事，不是排中律被证伪。希尔伯特 1927 年汉堡讲演仍把有限立场说成足以保住古典分析；布劳威尔 1927 年的《对形式主义的直觉主义评论》则把形式主义写成没有内容的公式游戏。

两套讲法在 1928 年已经互相听不进去，除名只是把听不进去写成封面。哥德尔 1931 年来得更晚；冯·诺伊曼事后认为哥尼斯堡那种三派并陈已经过时。把不完备提前塞进 1920 年代的对骂，会把两场不同的危机叠成一场。

第三幕那个 $\sqrt{2}^{\sqrt{2}}$ 的例子，方法上仍是非构造的：它靠排中律分案，不指出哪一案为真。1934 年格尔丰德—施奈德定理后来证明 $\sqrt{2}^{\sqrt{2}}$ 是超越数，因而无理——后人知道该取第二案。知道答案，并不把当年的方法变成构造。希尔伯特要保住的是这种分案仍算证明；布劳威尔要否定的也正是这一点。

核心分歧#

合法的推理是什么？希尔伯特认为：一致的形式系统里可证的，就是合法的——排中律、反证法、非构造存在都是工具。布劳威尔认为：只有构造才给出对象与真；$\neg\neg P$ 推不出 $P$，对存在尤其如此。形式主义问系统崩不崩；直觉主义问每一步是否真的做出了那个对象。

当代启示#

海廷 1930 年把直觉主义逻辑写成形式规则，布劳威尔本人对此并不热心——形式化是翻译，不是原作。后来的 Curry–Howard 对应、马丁-洛夫类型论、Coq / Agda / Lean，走的是海廷这条翻译路线：构造性证明对应程序。

这不是 1928 年年刊人事的翻案，也不是「人工智能必须用直觉主义」。经典数学仍是主体；构造性数学是另一套可检查的标准。两套标准可以并存，正因为当年谁也没有把对方从数学里真正驱逐出去。

延伸思考#

• 如果布劳威尔赢了，数学会是什么样子？
• 排中律在有限情况下是显然的——在无穷情况下，它的合理性是否需要重新审视？
• 年刊除名结束的是一场哲学争论，还是只结束了一场人事？

延伸阅读：布劳威尔《直觉主义与形式主义》(Intuitionism and Formalism, 1912 就职演讲)；海廷《直觉主义逻辑的形式规则》(1930)；阿伦·海廷《Intuitionism: An Introduction》(North-Holland, 1956)；迈克尔·达米特《Elements of Intuitionism》(1977)；迪尔克·范·达伦《Mystic, Geometer, and Intuitionist: The Life of L. E. J. Brouwer》(牛津, 1999/2005)