形式化公理系统（逻辑）

形式化公理系统(formal axiomatic system)，通常指形式化的、公理化的推理系统，即含有一系列公理、使用形式语言的推理系统。 按形式语言的定义，有原子集合和算子集合； 此外，作为公理化系统，包含一个公理的集合； 作为逻辑的演算系统，还包含一个推演规则的集合。 在这些推演规则下，可以结合公理对公式（前提）进行一系列演绎； 不需要前提，仅需要公理和推演规则就能进行的演绎称为证明，其结果是系统中的定理。

记号

通常记形式化公理系统为 [math]\displaystyle{ \mathcal{L} = \mathcal{L} \langle A, \Omega, Z, I \rangle }[/math]，四元组中：

• [math]\displaystyle{ A }[/math] 是语言中的原子公式或句子的终端元素的集合。对逻辑演算，包括全部原子命题，即命题常量及命题变元。
• [math]\displaystyle{ \Omega }[/math] 是语言中的全部算子符号的集合。对逻辑运算，是全部逻辑联结词的有限集合。
• [math]\displaystyle{ Z }[/math] 是形式系统的全部变换规则的有限集合。对逻辑演算，称为推理规则。每个规则都由原子公式和算子符号构成。
• [math]\displaystyle{ I }[/math] 是形式系统的起始点的有限集合。对逻辑运算，称为公理。

种类

公理的数目和推理规则的数目是相权衡的，根据权衡的结果有不同的类别。 推理规则较多而不使用公理的属于 Gentzen 风格系统，主要有自然演绎系统和相继式演算等； 相反，使用公理的称为 Hilbert 风格系统或公理系统。 公理系统中极端地使用尽可能少的推理规则，而公理较多的是 Hilbert 表示，一般仅使用一两条规则。

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