概念

证明论

把数学证明本身作为研究对象，通过自然演绎、相继式演算等形式系统分析证明结构，序数分析用于衡量理论的一致性强度。

阅读路径

参考可汗学院 Get ready 机制：先修概念 → 当前概念 → 进阶概念，✓ 表示已读。

证明论逻辑与集合论

01定义

证明论把「证明」本身当作数学对象研究：自然演绎与相继式演算给出证明的精细语法，切消定理说明证明可化为无引理跳跃的直接形式，序数分析则度量理论的一致性强度。

切消：经引理 B 的间接证明化为直接证明

自然演绎贴近数学家的推理习惯（引入/消去规则成对）；相继式演算（Gentzen）便于元数学分析——两者等价而各有所长。

无切证明只含结论的子公式——「证明不引入新概念」；由此可得一致性证明与判定过程，是构造性数学的引擎。

用序数为理论标定「证明论强度」：PA 的强度是 $\varepsilon_0$ ——理论的一致性可归约为某序数的良序性（Gentzen 1936）。

\frac{\Gamma\Rightarrow A\quad A,\Delta\Rightarrow C}{\Gamma,\Delta\Rightarrow C}\ (\text{切规则})

希尔伯特纲领要求用有限方法证明数学的一致性；根岑 1930 年代以相继式演算与切消定理回应，并给出 PA 的序数分析——证明论由此独立成科。

Curry-Howard 对应把证明解释为程序（类型论与函数式编程的理论根基）；自动化定理证明与程序验证的核心理论。

自然演绎：换质位定理的证明树逐步展开：从假设出发，按推理规则向上生长出完整证明树

展开步骤0