形式系统作为有向图
一个形式公理系统定义了一个有向图:
- 顶点: 所有从系统符号构建的良好公式
- 边: 推理步骤 —— 一个公式通过推理规则从其他公式中继承
- 公理: 特别的源顶点没有入边
- 定理: 所有从公理集可达的顶点
一个关于定理 T 的证明: 从公理集到 T 的有向路径。证明是一个顶点序列 A₁, A₂, ..., Aₙ = T，其中每个步骤都遵循一个推理规则。
形式系统的两个基本属性, 以几何方式表达:
一致性: 一个公式 F 和它的否定 ¬F 都是可达的。几何方式: 定理顶点 F 和定理顶点 ¬F 不是都可达的。没有"爆炸"路径。
完备性: 每个公式 F 或 ¬F 都是定理(可达)。几何方式: 图是强连通的, 这意味着对于每个顶点 F, 至少一个 F 或 ¬F 从公理集有路径。
Gödel 不完整性作为几何属性
库尔特 Gödel 在 1931 年证明了, 任何足够强大的一致形式系统, 基本算术都可以表达, 是不完整的: 存在公式 G, 使得 G 或者 ¬G 都不能被证明。
几何方式: 在任何足够强大的一致形式系统中, 图中存在无法从公理集可达的顶点 —— G 或者 ¬G 都没有路径从公理集。
Gödel 的构造: 他编码了一个公式 G, 实质上说, "我不是可证明的." 如果 G 可以被证明, 系统将是不一致的(一个真实的陈述说它不是可证明的)。如果 ¬G 可以被证明, 系统将是不一致的(G 将是假的但系统证明了它)。所以 G 或者 ¬G 都不能被证明 —— G 是一致系统中不可达的顶点。
不完整性不是所选公理的缺陷：哥德尔证明了这是一种任何足够表达算术的一致系统的结构性质。无法达到的顶点无法通过添加更多公理而移除，除非产生新的公理。
数学对象作为空间中的点
可以将柏拉图的数学观点以几何方式形式化：数学对象生活在一个抽象空间中，这个空间的点就是这些对象本身，空间的结构由它们之间的关系决定。
考虑自然数 ℕ = {0, 1, 2, 3, ...}。可分性关系定义了一个偏序：m 除以 n 当且仅当 m | n。这一偏序定义了一个几何——可分性格的 Hasse 图。
每个质数都处于 1 上面的最小位置。每个合数都在其质因数上方。这一空间的结构包含了所有的数论。
使这一观点柏拉图化：结构存在于任何心灵研究它之外。7 是质数的事实——7 没有7 之间的除数——是7 在可分性格的位置的客观事实，与符号、文化或文明无关。
任何探索计数和可分性质的文明都会发现相同的结构。数字系统的几何是普遍的。
导航可分性格网
在可分性格网中，两个数的最小公倍数 (lcm) 对应于它们的 联合（最低上界），而最大公约数 (gcd) 对应于它们的 交汇点（最大下界）。
最大公约数可以通过欧几里得算法计算：gcd(a, b) = gcd(b, a mod b)，直到 b = 0 为止。
抽象所抹去的内容
几何抽象：将高维对象投影到低维子空间。投影丢失信息（子空间之外的坐标），但完美保留子空间结构。
数学抽象的工作方式相同。一个群集是一组满足四个公理的二元运算的元素。将群集抽象为群结构时，抹去：特定的元素，特定的运算的计算规则，任何额外的结构（顺序、度量、拓扑）。剩下的：四个公理的骨架。
收益： 对所有群集的每个定理都有效——整数的加法、旋转的组合、置换的组合、分子结构的对称性、多项式方程的伽罗瓦群同时。抽象的定理只需要一次证明；它的实例是免费的。
这就是为什么纯数学家抵制添加领域特定假设的原因：每加一个假设都会限制定理的适用范围。关于域的定理（要求乘法逆元）适用于比关于环的定理（不需要乘法逆元）更少的结构。
精确性与普遍性的权衡
存在权衡：更抽象的定理适用范围更广，但对特定实例说得少。关于向量空间基于域的定理对ℝ^n说得比对特定地ℝ^n（其中距离和角度被定义）少。
Hamming的暗示规则：尽可能地抽象，但保留所需的属性。抽象过多，你的定理变得空洞（任何集合与任何操作满足...）。抽象不足，你的定理无法转移到新应用。