资源介绍
这是一本篇幅精炼却内容扎实的数学逻辑著作，来自印度理工学院马德拉斯分校电气工程系的Krishna Suryanarayan，将其收录在Springer的计算智能简册系列中，于2026年正式出版。整本书虽然只有两个章节，但信息密度相当高，目标也非常明确，就是教会读者怎样一步一步地写出可以被机械验证的形式化证明。所谓形式化证明，是指那些每一步推导都可以被计算机程序严格检查的证明过程，它不同于我们在普通数学课上写的那种依赖直觉和自然语言的论证，而是要求每一条规则、每一步推理都有明确的逻辑依据。全书选择策梅洛公理系统作为集合论的基础框架，作者在序言中坦率地指出，这套公理对于本书涉及的内容而言已经足够了，并不需要用到更强的选择公理或替换公理等，这在一定程度上降低了读者的学习门槛。第一章是逻辑基础部分，作者系统地整理了书写形式化证明所需要的全部逻辑符号，包括非、或、且、蕴含、当且仅当、对所有、对至少一个、对恰好一个以及等号等基本符号，并在此基础上给出了项、公式、公理等核心概念的精确定义。作者特别强调了一个"适当公理"的概念，这一概念贯穿全书，是判断一个陈述能否被作为公理使用的关键标准。第二章是集合论的主体部分，内容涵盖了集合论中最基本也是最重要的概念和定理，包括集合的相等与配对、并集、子集、空集、交集、罗素悖论与全集的不存在性、差集、幂集、有序对、笛卡尔积、关系与函数、归纳集、传递集，最终还给出了Peano系统存在性的形式化证明。值得注意的是，这个Peano系统的构造是从集合论公理出发完成的，也就是说，作者用形式化的方式证明了自然数系统可以在集合论的框架内被建立起来，这为数论乃至整个数学的公理化基础提供了一个完整的形式化链条。对于初学者来说，这本书的阅读路径是比较清晰的，但作者也提醒读者，假定读者已经具备基本的逻辑知识，并对"公理化集合论"这个概念有所了解，否则直接阅读可能会感到吃力。书中给出了大量完整的推理步骤和形式化写法，对于想学习如何写证明、尤其是想在计算机辅助证明系统上动手实践的读者来说，是一份非常实用的参考资料。作者也在序言中明确提到，这本书可以帮助读者开发用于验证形式化证明的软件，因此它不仅适合作为形式化证明课程的教材或参考书，对于从事自动定理证明、形式化验证、编程语言理论等方向研究的工程技术人员也有参考价值。如果你正在寻找一本不过分冗长、又能直接带你进入形式化证明世界的入门读物，这本SpringerBriefs值得认真翻一翻。