证明论——把证明当作可计算、可度量的对象

父级：logic

把证明当作一个形式数学对象：将它规范化、运行它、度量它的强度。

Gentzen：自然演绎、相继式演算、割消

Gentzen 重新组织了逻辑，让证明有了结构。割规则（cut rule）——也就是"引用一条引理"。他的主要定理（Hauptsatz，即割消定理）：任何证明都能被转换为一个无割的证明——没有引理，没有绕道——而这样的证明随即具有子公式性质（证明中出现的一切，早已出现在待证目标之中）。

割消 = 范式化

从一个证明中消去一次割，恰好对应于其相应程序的一次β 归约（curry-howard）。将证明范式化 = 运行一个程序；一个无割证明就是一个值。

度量证明的强度：序数分析

Gentzen（1936）用直到序数ε₀的超穷归纳，证明了PA 是一致的。这个 ε₀ 就是 PA 的证明论序数——衡量该理论力量的一个数值指标；更强的理论对应更大的序数。Gödel's second theorem 指出 PA 无法证明自身的一致性，所以这个证明必须爬得恰好超过 PA（也就是那个 ε₀-归纳）——不完备性，在序数中被量化了。

逆向数学与证明抽取

• 逆向数学通过定理所最少需要的公理来校准它们（二阶算术的"五大"子系统）——"这个定理在等价意义上，需要哪些公理？"
• 计算内容： 一个范式化/无割的证明携带着一个程序（可实现性；程序抽取）。一个对 ∀x∃y. R(x,y) 的构造性证明，就是一个从 x 计算出 y 的算法。

为什么这在这里重要

割消＝范式化，正是让 Lean 能够运行证明、抽取出经验证代码的引擎；序数分析则是不完备性变成可度量资源的地方（参见 quantitative-incompleteness）。证明论是 Curry–Howard 的"动态"那一半——type theory 是"静态"那一半。