数理逻辑的起点

虽然是科普书，但没有纯谈数理逻辑的演化史，从概念出发，到推理结束，一环裹一环，像不断裹挟上升的浪花，看得非常过瘾。里面主体讲的是数理逻辑，还讲了一小些极限、连续、正余弦函数（并不知道为什么插入这些内容）。

可以瞥见，数理逻辑是计算机软件的雏形和基础，尤其是从罗素到哥德尔的一路论证与反论证，都是一步步地扩大形式系统，为了计算机的不可判定问题进行充分的理论准备。皮亚诺公理用来定义自然数集，将集合与逻辑结合在一起，建立了数学的基础。但集合如果只研究有限的话，其实很 trivial，集合被提出来的核心问题是研究无限。逻辑学的两大研究方法——语义学（Sematics）和句法学（Syntax），都是编译器乃至自然语言处理的基石。尤其是句法学研究，在不了解语义的情况下，使用与外延相对的内涵方式，使用一系列的集合来定义形式系统，更贴近计算机程序的日常思维。形式系统的组成包括公理、逻辑公式和推理规则，将三者结合在一起就能从形式上表示“证明”，得到的就是“定理”。而形式系统本身可以被定义为“相容”和“完备”的，这两者都是使用形式系统本身得到的定义，也就是形式系统的形式系统，希尔伯特计划就是想要证明数学可以被形式系统完全表示，并且具有相容性。哥德尔的两种不完备定理就是对这种形式系统能否用来描述形式系统进行了一番推理，他将形式系统的符号序列中的每个符号用质数来唯一描述，得到乘积，这一乘积被称为哥德尔数——因为是质因数，可以一一对应，所以哥德尔数可以用来唯一表达与确定形式系统。

形式系统里的逻辑公式可能会有自由变量，在自由变量还存在时逻辑公式就能被称为谓词，即 Predicate，消除掉自由变量后就是语句，语句才在语义上存在现实逻辑中的对错，而谓词不会。将自由变量用哥德尔数的数项替换后，就是对角化。对角论证法，就是将逻辑公式的现实含义代入形式系统，康托尔用它论证了实数是不可数集合。

在书里还提到了形式系统里的不同类（第 1 类、第 2 类……），类似于泛函里高阶函数的概念，很有趣。另一个有趣的形式系统表示是，将公理、定理都定义成形式系统里的数组项，前些项是公理，最后一项是定理，大概是酱紫研究形式系统本身。

分析、拆分和综合，形式化后又返回有含义的问题，酱紫形式和本质统一起来研究，会促进理解，也就是数学建模的核心所在。在数学中，形式相似时本质便也相似。数学归纳法，之所以有“数学”的前缀，是因为把它应用在其他学科时，很容易得出一些玄学结论。书里也批评了“滥用不完备定理，把它当成证明理性界限的定理”这样的玄学应用法。

另，书里几乎给出了哥德尔不完备定理的完整证明（说几乎是我根本没有跟着推……），如果有兴趣的话也可以就着哥德尔的原始论文单看这个。