1910 年的 Principia Mathematica 竟预言了 Lambda 演算
Principia Mathematica is modern and insightful
重读 1910 年出版的 Principia Mathematica，我惊讶地发现它读起来像是一本现代编程语言教材。Whitehead 和 Russell 在书中极具洞察力地探讨了 referential transparency、extensionality 以及 type 等现代概念，甚至早于 lambda-calculus 的正式提出就引入了 propositional functions。书中对 'any' 与 'all' 的区分暗示了 Intuitionism 的萌芽，而关于存在性证明必须提供具体 witness 的观点，更是与后来的构造主义不谋而合。尽管证明过程繁琐，但其核心思想——如 bound variables、alpha renaming 以及 descriptive functions 的定义——至今仍是计算机科学和逻辑学的基石。
定义在理论上虽然是多余的，但它们是纯粹的排版便利，却往往比命题本身传达出更重要的信息。
HN 评论区
155- tristramb
在开始阅读之前，如果想先找本通俗易懂的入门书，可以看看他的《数学哲学导论》：
https://en.wikipedia.org/wiki/Introduction_to_Mathematical_P...
为了方便阅读，这里还有各种 PDF 版本：
- WillAdams
如果你能从头到尾读完这本书，那你绝对是英雄。我有时候甚至怀疑，他们是不是故意在中间塞了个巨大的逻辑错误，就是为了恶搞那些假设没人会去读它的人。
- radford-neal
对于那些不熟悉《数学原理》这部伟大却悲剧的作品，以及罗素为寻找数学基础而进行的探索（剧透：根本不存在）的人来说，有一本非常棒的漫画叫 Logicomix：https://en.wikipedia.org/wiki/Logicomix
我大概有十年没读过了，但不知为何，它总是我花大量时间去思考的书和故事之一。
- pngwen
与其把时间花在对着罗素和怀特头撞南墙上，我建议大家去读读《同伦类型论》（也就是 HoTT 书）。依赖类型很酷，能开拓思维，但高阶归纳类型简直能让人精神错乱。
《小 Scheme 程序员/类型论者》可以作为预备读物，帮你为 HoTT 热身。
它的优势在于对函数式编程语言更实用，甚至比 Mac Lane 的《为工作数学家准备的范畴论》（我有时看到有人推荐给有数学倾向的 Haskell 新手）还要实用。
- glimshe
我有一本，很喜欢。不过我一直更偏爱 Frege 的《概念文字》。他的符号系统非常有创意。很遗憾，罗素对这个项目的消解让它被扔进了历史的垃圾堆。