公理（逻辑）

公理
术语名称	公理
英语名称	axiom

公理模式
术语名称	公理模式
英语名称	axiom schema

公理(axiom)指没有经过证明，被当作不证自明的命题。 若规定符合某形式的公式都是公理，则称为公理模式(axiom schema)。 公理在相关理论中其真实性理所当然，且是作为推导、演绎的起点。 在推理系统中，描述命题形式推理规则的称为逻辑公理， 其他涉及非逻辑部分的公理是非逻辑公理，也称为公设(postulate)。

对于被解释到真实场景中的推理系统，公理往往要求是这个系统中不证自明的命题。 但这些命题不总是能确认其成立的，比如平行公设。

定义

（形式化）推理系统中，通过变换规则从命题引入新的命题。由于变换规则本身不一定具有引入任意命题的能力，可以引入一些命题作为推理的起点，也就是公理系统（形式化公理系统），这些作为起点命题即称为公理系统中的公理。

“公理”一词有其他使用场景，其共同点是不需要被演绎证明，且用于演绎证明其他定理。

分类

• 描述公式中逻辑符号之间关系的公理称为逻辑公理。
• 描述公式中非逻辑符号之间关系的公理称为非逻辑公理或公设(postulate)。
• 数理逻辑中，给定公理系统语言中一个合式公式，约定将其中的项或命题变元替换为任何项或任何公式后，都是系统中的公理。这种情况下称为公理模式(axiom schema)。

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