知识/定理
希尔伯特形式主义纲领：把数学公理化后，用有限元数学证明「公理系统一致」——数学的自我辩护。
公式
证明论：无矛盾性 $\text{Con}(T)$ 在有限可证框架内证明。
证明思路
（元数学）把证明本身形式化为符号演算对象，用「直观有限」方法证明无矛盾。
应用/例子
证明论、元数学、自动化推理；直接面对哥德尔的挑战。
意义/影响
数学基础工程的蓝图；哥德尔不完备定理证明其不可能——纲领的悲壮遗产。
DOXA · 数学编年史 · 知识详情
1920s ｜ 希尔伯特 ｜ 逻辑 ｜ 学派
希尔伯特形式主义纲领：把数学公理化后，用有限元数学证明「公理系统一致」——数学的自我辩护。
证明论：无矛盾性 $\text{Con}(T)$ 在有限可证框架内证明。
（元数学）把证明本身形式化为符号演算对象，用「直观有限」方法证明无矛盾。
证明论、元数学、自动化推理；直接面对哥德尔的挑战。
数学基础工程的蓝图；哥德尔不完备定理证明其不可能——纲领的悲壮遗产。