概念-形式系统
形式系统（Formal System）是本书的核心概念之一，它是一个抽象的、基于符号操作的系统，用于严谨地研究推理和证明的本质。
形式系统的构成
一个形式系统通常由以下几个部分组成：
- 符号（Symbols）：一个有限的、明确定义的符号集合，是构成系统内所有“表达式”或“串”的基础。
- 公理（Axioms）：一组预先给定的、无需证明的初始符号串。它们是系统内所有推导的起点。一个形式系统可以有零条、一条或无穷多条公理（通过“公理模式”来定义）。
- 推理规则（Rules of Inference）：一组精确的、纯形式化的规则，用于从已有的定理（包括公理）生成新的定理。这些规则只关心符号的形状和排列，不关心其概念-意义。
- 定理（Theorems）：所有可以从公理出发，通过有限次地应用推理规则而生成的符号串。
本书中心的概念之一是形式系统。我用的这种形式系统是美国逻辑学家艾米尔·波斯特在二十世纪二十年代发明的，通常被称为“波斯特产生式系统”。
J方式与W方式
本书提出了两种与形式系统互动的方式：
- 机方式（J-mode）：在系统内部工作，像机器一样机械地、不加思考地应用规则来生成定理。
- 惟方式（W-mode）：跳出系统，从外部对系统进行观察、思考和评论，发现其中的模式和性质。
在研究形式系统时，很重要的一点是要区分在系统之内的工作，和做出关于系统的判断或说明。
意义与同构
形式系统本身是无意义的纯符号游戏。然而，当一个形式系统的定理集合能够与某个我们熟知的领域（如算术）中的真理集合建立起概念-同构关系时，这个形式系统便获得了意义。
这些人的想法是：建立一个形式系统，它的定理同构地反映一部分现实世界。
一致性与完全性
形式系统有两个重要的元数学性质：
概念-哥德尔不完全性定理证明了，任何一个足够强（能表达初等算术）、且一致的形式系统，必然是不完全的。
书中讨论的形式系统
- 形式系统-WJU系统
- 形式系统-pq系统
- 形式系统-tq系统
- 形式系统-命题演算
- 印符数论（TNT）