{"content":"《数学编年史》· 第46期：布劳威尔与直觉主义——数学是心灵的构造\n\n公元1907年—1918年 · 荷兰/阿姆斯特丹\n\n上一期我们见证了罗素悖论动摇了逻辑主义的根基。正当怀特海和罗素用两千页《数学原理》艰难修补地基时，荷兰阿姆斯特丹一位年轻的博士候选人提出了一个更激进的方案——从根源上重新定义数学是什么。\n\n卢伊岑·布劳威尔（L.E.J. Brouwer, 1881-1966）在1907年的博士论文中宣布：数学不是逻辑的派生物，也不是符号的游戏，而是人类心灵中的自主构造活动。每个数学对象必须能被心灵「构造」出来才算存在——你不能因为一个命题没有矛盾就承认它成立。\n\n这一立场最为惊世骇俗的后果，是布劳威尔拒绝了排中律（Law of Excluded Middle）：对于无穷集合，并非每个命题都非真即假。比如「π的小数展开中有连续一百个7吗？」——在直觉主义看来，这个问题在被实际证明之前并无真假可言。这等于向两千年来从亚里士多德到莱布尼茨、从布尔到弗雷格的逻辑传统发出了正面挑战。\n\n1918年，布劳威尔发表了《集合论、逻辑与数学基础》，系统建立了直觉主义数学的框架。他重新定义了「存在」——存在即被构造。这使数学家们分裂为两大阵营：坚持古典数学的「实在论者」和追随布劳威尔的「直觉主义者」。希尔伯特对此痛心疾首地喊道：「将排中律从数学家手中夺走，就像禁止天文学家使用望远镜！」\n\n然而，这场论战没有赢家，却结出了意想不到的果实。直觉主义逻辑后来经由海廷（Heyting）形式化为海廷代数，成为现代理论计算机科学的基石。今天每一个函数式程序员都在使用的「Curry-Howard对应」——将证明等同于程序、将命题等同于类型——其思想渊源正是布劳威尔的构造性数学。量子逻辑、范畴逻辑中的许多核心概念，也都流淌着直觉主义的血液。\n\n布劳威尔告诉我们：数学的真理性，不在于它是否与现实世界对应，而在于它是否可以被人类心灵所理解与构造。\n\n（明日续：希尔伯特的纲领——为数学形式化而战，以及哥德尔即将投下的阴影）","contentType":"text/plain;utf-8","attachments":[],"quotePin":""}