← #805

《数学原理》读起来一点也不古老，反而现代得惊人

查看原文 HN 讨论

文章摘要

这是 Oleg Kiselyov（函数式编程与元编程领域的知名研究者，okmij.org 站长）在读怀特海与罗素 1910 年出版的《数学原理》（Principia Mathematica，简称 PM）第一章时做的一组笔记。他的核心感受是：这本 116 年前的书读起来不像数学史文献，而像一本现代的程序设计语言教材。文章一开头就点明了这个反差——PM 以极大的洞察力讨论了外延性/内涵性、引用透明性、类型这些今天仍然是编程语言研究前沿的话题，可能是历史上第一次在现代意义上使用「定义域（domain）」「α 重命名」和「类型（type）」这些词；它的「不完整符号」（只有放在上下文中才有意义的符号）预示了 continuation 和控制算子；它还敏锐地指出自由变量与约束变量、代换、抽象与应用这一整套概念其实都来自语言学。作者说，他忍不住觉得 PM 里其实已经包含了 lambda 演算。

作者也先给读者打了预防针：PM 全书极其庞大，以「花一千页证明 1+1=2」闻名。但按前言的说法，证明之所以写得如此不厌其烦，正是为了杜绝任何未言明的前提偷偷溜进推理。PM 的目标是给出一组极其基本的概念，并证明仅凭这些概念就足以支撑整个数学。作者认为，如果 PM 是今天出版的，所有证明都会被扔进附录（或者交给定理证明器），真正重要的是那套基本概念和整体设定，而这些几乎都写在前言和第一章里。

具体的发现包括：

• 引用透明性（第 8 页）：PM 可能是数学文献中最早提出内涵与外延之分、以及今天所谓「引用透明」的地方——「若 p ≡ q，则 f(p) ≡ f(q)」。用现代话说，f 是一个上下文 C[]，若 p ≡ q 则 C[p] ≡ C[q]。紧接着书里就给出了一个非引用透明的反例：「A 相信 p」。这个例子暴露了概念的语言学出身（脚注里提到了弗雷格）。书中还明确写道「数学永远关心外延而非内涵」。
• 定义（第 12 页）：PM 说定义严格来讲只是排版上的便利、理论上是多余的；但同一段又强调定义往往比使用它们的命题携带更重要的信息，因为定义体现了我们对主题的选择和对重要性的判断，而且一个定义常常包含对某个common idea 的分析，本身就可能是一次显著的推进。
• 命题函数即 lambda 项（第 15 页）：以「x 受伤了」为例，在 x 未确定前它其实什么都没断言。PM 引入了 x 戴帽的记号来表示这个「命题函数」，并明确指出「x̂ 受伤了」和「ŷ 受伤了」在意义上毫无区别——这正是自由变量、约束变量、代换与 α 等价。第 17 页讨论量化公式时又用定积分 ∫ 作类比说明约束变量（PM 沿用皮亚诺的术语称之为「表观变量」，自由变量则称「实变量」），并引入了变量作用域的概念。作者感叹这说明 lambda 演算血统悠久。
• 「任一」与「所有」（第 18–19 页）：PM 坚持区分模式断言 ⊢ f x 与全称量化 ⊢ (x).φx，尽管在它自己的逻辑里两者等价。书中用 sin²x + cos²x = 1 举例：这个公式既不断言某个特定情形，也不字面断言「对所有 x」，它只是让 x 完全未定地成立。这与后来的直觉主义倾向遥相呼应。
• 存在即构造（第 20 页）：PM 在讲 ∃ 引入规则时写道，证明存在性定理「实践中唯一的办法」就是找到某个具体的 y 使 φy 成立；并指出若假定乘法公理（选择公理）就会在一大类情形中给出找不到任何具体实例的存在性定理。作者认为罗素与怀特海也许是无意识地采取了直觉主义甚至构造主义立场，而这发生在 1910 年。Jacques Carette 补充说布劳威尔当时也在发表，且部分构造主义可上溯到 30 年前的克罗内克。
• 类型（第 21 页）：书中要求 φ 与 ψ 必须是「接受同一类型参数」的函数，作者说这大概是「type」一词第一次以今天编程中如此常见的含义被使用。
• 属于符号 ∈ 的来源（第 26 页）：作者注意到书里指出集合成员符号其实是希腊字母 epsilon，取自 ἐστί（「是」）的首字母，所以 x ∈ man 字面意思就是「x 是一个 man」。
• 描述性函数（第 33 页）：这可能是把函数定义为一种特殊二元关系的最早现代定义——任何二元关系 R 诱导出一个函数 R’y，取使 xRy 成立的那个唯一的 x。PM 称之为「描述性函数」（今天常叫「限定摹状词」），名称与论述都承袭罗素五年前那篇著名的《论指称》。Carette 补充说 PM 在 1910 年就预见了「限定摹状词」和「显式函数」的区别，因为数学中早有这类例子——解析延拓就是一种「有函数性但不是函数」的过程，因为其中涉及一定的选择。

文章当前版本为 1.3（2026 年 8 月），并给出了密歇根大学历史数学收藏的 PM 全书扫描件链接，以及斯坦福哲学百科关于 PM 记号法的条目。

HN 评论精华

276 分、155 条评论。讨论主要围绕「这书到底怎么读」「PM 在数学史上的地位」和「与现代类型论的关系」三条线展开，气氛相当友善，几乎没有争吵。

• glimshe：能把这本书从头读到尾的人绝对是英雄。他甚至怀疑作者是不是在中间故意插了个大逻辑错误来钓鱼，赌没人会真的读完。
  • gumby 顺着这个玩笑回：「你难道墙上没挂一张怀特海亲笔签名的 bug bounty 支票？」然后正色补充：整个工程的核心处确实有一个巨大的逻辑漏洞，只不过要等到很久以后才被哥德尔发现。
  • kjellsbells 想的是另一个方向：排版工人当年出错的概率有多大？谁能连打一千页 APL 式的符号而不引入 bug？
  • sergevar 指出去年 HN 上有过一个把 PM 形式化到 Lean 里的 Show HN，另有 Principia Rewrite 项目已在 Coq 中依照原书证明草稿验证了命题逻辑部分（第 1–5 节）的全部 189 条定理。
• WillAdams 推荐入门顺序：先读罗素的《数理哲学导论》（Introduction to Mathematical Philosophy），并给出了 UMass 上 Klement 整理的多个 PDF 版本；zote 补充 PM 原书本身也在同一站点有电子版。
• hasley 推荐用更轻松的方式入门：图像小说《Logicomix》，讲罗素的求索之旅，虽然为了叙事牺牲了一些史实准确性。nitsuaeekcm 独立地也推荐了这本书，说自己十年没重读，却一直在反复琢磨这个故事。
• voidhorse 说自己更偏爱弗雷格的《概念文字》（Begriffsschrift），认为那套记号法非常有创意，可惜被罗素的「拆台」扫进了历史垃圾堆。
  • igravious 强烈反对这个判断：《概念文字》根本没有被扫进垃圾堆，它是奠基之作。集合论基础里的一个悖论并不能抹掉其哲学洞见、创新记号法，以及把数学函数与逻辑结合从而给出谓词逻辑的做法。他给了一个漂亮的对照：布尔是「逻辑 + 代数 = 代数逻辑」，弗雷格是「逻辑 + 函数 = 谓词逻辑」，既然布尔被神化，弗雷格也应当如此。
  • cubefox 指出原评论混淆了两本书：发明现代谓词逻辑的是《概念文字》，而试图（未能成功）从纯逻辑推出算术的是后来的《算术基本定律》。
• TimorousBestie 建议与其和罗素、怀特海较劲，不如去读同伦类型论（HoTT Book）：依值类型已经足够开阔眼界，高阶归纳类型更是「改变思维方式」；而且对函数式编程更有直接用处，甚至可能比常被推荐给数学倾向 Haskell 新手的 Mac Lane《Categories for the Working Mathematician》更合适。
  • fn-mote 强烈反对推荐 Mac Lane：那本书晦涩得毫无必要，虽然他也说不出更好的范畴论入门。
  • js8 说 HoTT 第一章讲类型论很好懂，第二章就彻底迷路了；但对单价公理很着迷，并谈到自己感兴趣的一种更「唯物」而非「结构主义」的 triage calculus 类型进路。
• tristramb 引用 Mark Dominus 的评论作为一种平衡：PM 是一本奇书，值得从历史和数学两个角度看，但它的记号法今天读起来相当晦涩，很多我们视为理所当然的技巧当时还不存在——「就像一个写得很差的计算机程序，PM 的篇幅有很大一部分是重复代码，是几个说着基本相同的事情的独立章节，因为作者还没学会能把这些章节合而为一的技巧」。bazoom42 顺势发问：有人把它重构成更简洁的现代版本了吗？
• pngwen 说自己在教计算理论时会讲 PM，但主要是为了讲清楚我们是如何发现计算的极限的；并建议大家读哥德尔那篇「加长版书评」——他在其中证明了 PM 做不到它想做的事，任何这类系统都做不到。lioeters 补上了论文名与链接：《论 PM 及有关系统中的形式不可判定命题》。
• d4rkp4ttern 提供了一个漂亮的历史闭环：PM 正是 Newell、Simon 和 Shaw 1956 年那个「逻辑理论家（Logic Theorist）」的素材——公认的第一个人工智能程序，它证明了 PM 第二章前 52 条定理中的 38 条，还为定理 2.85 找到了一个更短的新证明。放在今天 LLM 猛攻 Erdős 猜想的背景下看格外有意思。
• lordleft 感叹罗素竟然是（形式化）类型概念的发明者，这么基本又这么有用；layer8 提醒说罗素的类型跟编程语言里的类型并不真是同一个概念，并给了 PlanetMath 上罗素类型论的说明。
• radford-neal 回忆起 PM 里那套用点号代替括号的记号法，认为也许对编程语言有用：对非结合的运算符 $，不写 a$(b$c)，而写 a$.b$c——点号让它前面的 $ 在右侧具有更低的优先级，点越多优先级越低。他补充说自己读这书已经是五十多年前的事了，记忆未必准确。layer8 直接反问：这比括号好在哪？
• data_maan 泼了一盆冷水：「一个只读了 PM 前 40 页的人随手写的笔记居然能在 HN 引来几十条评论，这社区一定是数学极度饥渴、想学数学又始终没学成的一群人。」
  • laichzeit0 的回复反而成了整串里被赞最多的建议之一：其一，如果你已经会编程，最糟糕的做法就是把数学当成一门编程语言来学，你会被记号和「语法」折磨得毫无必要，数学是靠做才熟悉起来的，允许自己处于困惑状态；其二，做习题，别到处找答案手册，重点是逼你思考，挣扎的过程比对错重要，「我怎么知道对不对，又不能编译」是典型的程序员思维。他猜程序员之所以偏爱数学基础，是幻想只要挖到最底层的「汇编/机器码」，整件事就说得通了——但吊诡的是，历史上那些真正伟大的数学家，做数学时数学远未被形式化。
• jonjacky 分享了爱荷华大学的「PM 地图与表格站点（PM-MATS）」，用三种数字工具把 PM 各部分之间的结构关联可视化，还能查那条著名的 1+1=2 的证明（*110.643）。
• zual 提到有人在用 Lean 翻译 PM（大概借助了 LLM）的 GitHub 仓库；titanomachy 顺手纠正了他把西班牙语 traducir 直译成英文 traduce 的用词错误（英文里那是「诽谤」）。
• makerdiety 用调侃语气说「古人试图用数学证明数学的幼稚努力（被哥德尔的不完备性斩落）居然能帮我写更好的 TypeScript」，bulbar 认真反驳：为什么要用贬低的措辞？数学的一部分确实可以证明其完备性与一致性；公理虽古已有之，但「证明数学」这件事是希尔伯特开的头；不用数学还能怎么证明数学？当时发现的那些限制在那个年代是相当出人意料的。
• scoofy（前分析哲学专业学生）说，在 CS/技术论坛里看到这类内容既奇怪又令人鼓舞：既然我们已经在处理「智能」机器的种种含义，我们需要更多哲学。