Hilbert 纲领

希尔伯特纲领
术语名称	希尔伯特纲领
英语名称	Hilbert's program
别名	希尔伯特计划

Hilbert 纲领(Hilbert's program)指历史上由 D. Hilbert 提出的研究计划，将数学规约为形式化系统，并通过有限的推理方法（称为有穷主义方法）进行元数学研究，以尝试得到一个一致的、有穷的、绝对可靠的形式系统，以避免再次出现类似集合论悖论的矛盾。

后来这些元数学研究的结果发展成了分类:证明论。

Gödel 不完备定理说明了这样的元理论不可能存在。 Gödel 第二不完备性定理说明，推理系统一旦足够强大到描述 Peano 公理，这一系统就无法证明自身的一致性，需要引入更高一层的元理论进行一致性的描述，保证这一系统可靠的人物会转移到保证这更高一层元理论的可靠性上。换句话说，一个强大到表达算术理论的系统，如果想要证明其一致，则必须引入一个更强大的、也需要证明一致性的系统，也就是说无论如何都不可能保证所有系统都可以证明满足一致性。而有穷主义的方法比 Peano 公理更弱，更不可能证明自身的一致性，计划中使用有穷推理无穷的简化方法是不可能实现的。

证明论
研究动机与结果	Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理
结构化证明	推理系统 形式化公理系统 （形式化、公理化）	Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示
		Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎
		Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算
	证明、演绎	演绎、可演绎、证明、可证明
	命题、定理	命题、元命题、公理/公理模式、定理、元定理
	推理规则性质描述	保存真实性、保存重言性
	推理系统性质描述	可靠性、完备性/完全性、一致性、独立性
	重要元定理	演绎定理、切消定理（切割消除定理）
		（某种推理系统的）可靠性定理、完备性定理
序数分析	证明论序数
构造性证明 程序化证明	Curry–Howard 对应
	证明复杂度理论	证明复杂度