学校放春假了，随便喵两句。
第一次见到 Godel 不完备性的人可能都会解读成『「数学」是不完备的』：在人类理性史上高歌猛进、战无不胜的数学在其核心处存在无法知晓的真相。一定程度上这要归咎于不负责任的科普家玩弄噱头，把形式化数学混淆等同于一切的数学。数学并不自动是形式化的：现代人倘若反思从小到大的数学实践经验也会疑心日常见到的样子很难称为形式化，我们描述命题用的是自然语言、写证明用的是散文。
鉴往知来、有益无害。我们回顾一下这一段数理逻辑、分析哲学和数学基础的共同历史。1847 年，De Morgan, A.* 引入了专门符号来表示逻辑规律。同年，Boole, G. 的书**则用代数来描写命题的逻辑演算。1879 年，Frege, G. 将 Aristotle 以降确定的主词谓词区分弃之不顾，用变量（变项）和函数（函项）来刻画命题内部的结构，完成了《概念文字***》，基于量词对无穷和复杂度的分析自此得以成为可能。
理性主义哲学家 Leibniz, G. 曾经设想过 characteristica universalis（「通用文字」）来处理数学、科学和哲学上的概念，以摆脱日常语言带来的误解。Frege 氏将自己的工作看成是这个纲领的部分实现，他说
算术、几何、化学中的符号可以看成 Leibniz 氏纲领在特定领域的实现，而这里所给出的概念文字又增加了一个领域，实际上是一个中心领域，与其他所有领域相连。
即便有明确的哲学旨趣，Frege 氏并没有计划让他的《概念文字》来彻底完成 Leibniz 氏的通用文字纲领，但他确实计划了最终将数学建立在逻辑这个基础之上。
* De Morgan, A. Formal Logic. 1847. 后世以「De Morgan 律」冠名纪念。
** Boole, G. The Mathematical Analysis of Logic. 1847. 后世以 「Boole 代数」冠名纪念。
*** Frege, G. Begriffsschrift. 1879.
在《算术基础》中，Frege 氏试图澄清「（自然）数」这个概念，并将数的概念建立在逻辑概念之上。这是其目录的一部分：
II. 一些作者关于数概念的观点
- 数是外部事物的属性吗？
- 数是某种主观的东西吗？
- 数的聚合论
III. 关于单位和一的看法
- 数量词「一」是不是表达了对象的一个属性？
- 单位是不是彼此相同？
- 克服这些困难的尝试
- 困难的解决
IV. 数这个概念
- 每个单独的数都是一个自存的对象
- 为了得到数这个概念，我们必须明确等数的意义
- 我们的定义是完整的且被证明是有意义的
从中也可以看出，为什么分析哲学会追认 Frege 氏为其真正的奠基人*。在他看来，所谓自然数就是所有概念按等数关系划分出来的等价类：如果一个概念或者说命题函数 $\Psi(x)$ 与 $\Phi(x)$ 的外延有相同数量的元素，也就是说有相同数量的输入使得 $\Psi(-)$ 和 $\Phi(-)$ 为真（但不必同时为真），那么这两个概念被称为「等数」。等数的等价类构成数的概念，可以用数字来命名，比如 $\Phi(x)\in 1$ 和 $\Psi(x)\in 1$，其中 $1$ 在定义上无非是如上所述的等数等价类的缩写记号。其含义是说只有唯一一个输入使得两个命题为真。据此我们只借助逻辑学自然提供的命题作为资源，定义了作为数学基础的数。这种定义或者说对概念的分析方式，也正是分析哲学所提倡的「语境原则(context principle)」。
* Dummett, M. Origins of Analytical Philosophy. 1996.
作为间奏我们稍稍离题。1905 年，Russell, B. 在《论指称》*中利用 Frege 氏发明的概念文字对指称短语（denoting phrase）这一长期被视为形而上学难题的困境做了极其成功的诠释。该文中 Russell 氏批判了 Frege 氏「指称短语既有所指(denotation)也有意义(meaning)」，论述了「指称短语本质上是句子结构的一部分，其本身没有任何意思」，并给出了「将所有出现了指称短语的命题规约为不含这种短语的命题的方法」，而所谓「不含这种短语的命题」正是 Frege 氏的带量词公式。这种使用分析哲学处理传统形而上学问题带动了整个二十世纪哲学的发展。这是 Russell 氏逻辑原子主义（logical atomism）思想的具身，而这一思想正是肇始于该氏具有的数学基础的逻辑主义（logicism）。
Frege-Russell 两氏被认为是数学基础逻辑主义的代表人物。Frege 氏的理论特别是对自然数的处理流传百世，无愧乎逻辑主义的永恒纪念碑，但就其实现「将数学还原为逻辑」这一口号来说，仍然有可指摘。对 Frege 氏而言，他的等数定义本质上是一个二阶逻辑的句子，他需要澄清所有的命题构成的集合或者类，也就是说他需要集合论或者类论。即便当时的逻辑学家可以接受类论是逻辑学的自然主题，Russell 氏悖论的出现也使得类论过于逻辑自由的特点显得不合时宜。无论是引入集合论，或是按 Russell 氏一样使用类型论，都势必带来无法被公认为「逻辑」的符号或者公理，比如集合论的空集符号和分离原理、类型论对量词各种复杂公理都被当下的数学家和逻辑学家认为是非逻辑的。
* Russell, B. On Denoting. 1905.
如果说 Leibniz 氏的通用文字设想指导了若干个世纪后的逻辑主义思想，那么 Kant 氏则指导了数学基础的形式主义思想。在 Kant 氏看来数学的公理和定理并非逻辑原则，而是知觉材料的结构的描述。Hilbert 氏说
在进行逻辑推理和逻辑演算中所假定的东西，已经在表象中给出了，即某些非逻辑的具体对象，它们直观地表现为直接经验，并构成一切思想的基础。如果要确保逻辑思维的可靠性，就必须能对这些对象的各个部分进行全面考察；而且各部分的展示、区别、连续性、以及彼此之间的排列，都必须与对象本身一起给出，不能归结为其他任何东西，而且也确实没有必要进行这样的归结。
无论是 Kant 氏还是 Hilbert 氏都认同如果把数学限制在对某种具体对象的描述及其之间的逻辑关系上，那数学便不会出现矛盾，因为对具体对象的描述总是相容的。另一方面，按 Kant 氏的理论，理性理念（比如信仰）是与感知无关的，既不能从感知中抽象出来，又不能应用到感知中去，所以唯一可行的理性任务就是建立相容性，这也是该氏所说的「为信仰腾出地盘」。Hilbert 氏此时要处理的「实无穷」恰好也处于与理性理念相同的地位，所以建立数学的相容性概念于是呼之欲出。
自 Galileo 氏以降，物理工作的特点就是要把物理数学化。更早，自 Descarte 氏以来，数学工作的特点就是要把数学算术化。所以建立算术的相容性便首当其冲，并且我们确信算术作为知觉材料是没有矛盾的，建立算术的相容性对 Kant 氏纲领相当可欲，所差无非技术层面。另一方面，由于我们期待元理论问题要更加明确，在 Hilbert 氏看来这就意味着元理论能利用的资源本质上是有穷的、算术的。而逻辑主义的遗产实际上白送了 Hilbert 氏一套形式系统，所以形式主义数学基础的数学事业已经箭在弦上。但是根据 Godel 氏对形式系统的算术化的研究（见之前有关 Godel 不完备性的博文），我们知道算术相容性事业最后是失败的。
历史部分到此为止。
从历史角度我们可以回答为什么要进行数学的形式化。一是逻辑主义数学基础给予了我们充分多的智力遗产，一是 Kant 氏哲学要求我们辩护数学的相容性或者一致性，而为了定义这些概念一个形式化的数学系统是必需的。形式系统并不是数学真理本身，形式系统中的形式语言是无意义的符号的组合，满足事先给定的句法规则以模拟对象系统的知觉材料。形式系统是 Minecraft，而数学是真实世界，单个方块在 Minecraft 并没有在模拟真实世界的建筑中的某个方块所具有的那种意义。此外，在基础教育阶段我们便已经熟悉在数学中做出任何一个判断都需要理由，是故我们还需要一个推理系统，来模拟真实数学中所作的严格证明。
这样的形式系统，如果句法规则和推理系统都是本质有穷的，那比起具有无穷真理的数学材料来说容易把握太多了。这使我们能够把这个有穷系统当作一个数学对象以便对其性质进行研究，比如某些符号构成的句子是否可以证明，或者整个形式理论能产出的定理是不是就是对象系统的真相（Godel 说对 PA 并不）。
明白了形式化的深刻之后，一个很自然的问题是，我们是否可以形式化元理论？这是可以的。元理论可以形式化成 ZFC 集合论，在这里可以表达可证性、完备性、一致性的概念并且给出证明。当然有反对意见会认为，ZFC 集合论的资源太强了，我们应该效仿 Hilbert 氏对有穷和算术的追求。确实，对于一些性质，我们可以形式化，而且不需要借助非逻辑符号，也就是说，我们有逻辑来刻画一些性质。
对于句子 $p$ 的形式系统 $S$ 的可证性，我们可以引入模态算子 $\square p$ 表记可证。在推理系统中如果引入模态逻辑三条标准规则
- 必然性规则：$\vdash p$ 导出 $\vdash \square p$
- 分离规则：$p \to q,p$ 导出 $q$
- 分配公理：$\square(p\to q)\to (\square p\to\square q)$
此外只需再把著名的 Lob-Godel 定理加上并且钦定为公理
- Lob-Godel 公理：$\square(\square p\to p)\to\square p$
那么这个形式系统反映了任何形式系统的可证性，由于一切资源都是内建在标准模态逻辑中的，所以这套可证性的形式系统也叫「可证性逻辑」。
虽然形式化数学之中的这些形式系统有趣且深刻，但工作中的数学家并不青睐于认为形式化是数学工作的全部。研究形式系统的目的绝非为了把数学证明形式化，而是为了理解证明的本性，分析其固有能力和局限。数学家需要的并不是严谨地摆弄没有意义的符号，重要的是数学思想。在这个意义上，数学家需要能在其中自然表达数学思想的形式系统，在这一方面同伦类型论（Homotopy Type Theory, HoTT）是一个相当合适的备选项，它的泛等（univalent）公理正切合数学家们日常思考结构的方式。形式系统固然有可让机器验证证明的固有好处，真相也是数学家的毕生所求，但是对于真实的数学实践来说，即便是错误的证明可能也有惊世智慧、正确的陈述也可能索然无味，真实的数学家恰如郑乐隽所言
数学理论不争论孰对孰错，而是理论应该是什么样子的、研究的正确方式是什么。