形式系统作为有向图
形式公理系统定义了一个有向图：
- 顶点： 由系统符号可构造的所有良构公式
- 边： 推理步骤——一个公式通过推理规则由其他公式得出
- 公理： 没有入边的特殊源顶点
- 定理： 从公理集合可达的所有顶点
定理 T 的证明：从公理集合到 T 的有向路径。证明是顶点序列 A₁, A₂, ..., Aₙ = T，其中每一步遵循推理规则。
形式系统的两个基本性质，用几何方式表达：
相容性： 没有公式 F 和其否定 ¬F 都从公理可达。几何上：定理顶点 F 和定理顶点 ¬F 不能都可达。不存在'爆炸'路径。
完全性： 每个公式 F 或 ¬F 都是定理（可达）。几何上：对于每个顶点 F，F 或 ¬F 中至少有一个从公理有路径。
哥德尔不完全性作为几何性质
库尔特·哥德尔在 1931 年证明了任何足够强大以表达基本算术的相容形式系统都是不完全的：存在公式 G 使得 G 和 ¬G 都不可证。
几何上：在任何足够丰富的相容形式系统中，公式图中有顶点不能从公理可达——既没有从公理到顶点 G 的路径，也没有到顶点 ¬G 的路径。
哥德尔的构造：他编码了一个公式 G，它实际上说'我是不可证的'。如果 G 可证，系统就不相容（真陈述说它不可证）。如果 ¬G 可证，系统就不相容（G 会是假的但系统证明它）。所以 G 和 ¬G 都不可证——G 是相容系统中无法到达的顶点。
这种不完全性不是所选公理的缺陷：哥德尔证明了它是任何足够强大处理算术的相容系统的结构性质。无法到达的顶点不能通过添加更多公理来消除而不产生新的无法到达的顶点。
数学对象作为空间中的点
数学的柏拉图式观点可以几何形式化：数学对象存在于一个抽象空间中，其点是对象本身，其结构由它们之间的关系给出。
考虑自然数 ℕ = {0, 1, 2, 3, ...}。整除关系定义了偏序：m 整除 n 当且仅当 m | n。这个偏序定义了一个几何——整除格的哈塞图。
每个素数都坐在 1 上方的极小位置。每个合数都坐在其素因子上方。这个空间的结构编码了所有数论。
使其柏拉图式的是：无论是否有任何心智研究它，这个结构都存在。7 是素数的事实——7 在 1 和 7 之间没有因子——是 7 在整除格中位置的事实，与记号、文化或文明无关。
任何调查计数和整除的文明都会发现同样的结构。数字系统的几何是通用的。
在整除格中导航
在整除格中，两个数的最小公倍数（lcm）对应其并（最小上界），最大公约数（gcd）对应其交（最大下界）。
gcd 可以通过欧几里得算法计算：gcd(a, b) = gcd(b, a mod b)，当 b = 0 时终止。
抽象剥离的内容
几何抽象：将高维对象投影到低维子空间。投影丧失信息（不在子空间中的坐标），但完美保留子空间结构。
数学抽象的工作方式相同。群是具有一个二元运算满足四个公理的集合。抽象到群结构时剥离：特定元素、特定运算的计算规则、任何额外结构（序、度量、拓扑）。剩下的是四公理骨架。
收益： 关于群的每个定理都适用于所有群——整数在加法下、旋转在复合下、排列在复合下、分子的对称性、多项式方程的伽罗瓦群——同时应用。抽象定理证明一次；其实例免费得出。
这就是为什么纯数学家抵制添加领域特定的假设：每个添加的假设都限制定理的适用性。关于域的定理（添加乘法逆元）适用于比关于环的定理（不需要乘法逆元）更少的结构。
精度-通用性权衡
有一个权衡：更抽象的定理适用更广泛但关于具体实例说得更少。关于向量空间（在一个域上定义，具有向量加法和标量乘法满足 8 个公理）的定理比专门关于 ℝ^n 的定理说得少（其中距离和角度被定义）。
哈明的隐含规则：尽可能抽象，同时保留你需要的性质。抽象太远你的定理变得空泛（'任何有任何运算的集合满足...'）。抽象太少你的定理无法转移到新应用。