公理系统（逻辑）
| 公理系统 | |
|---|---|
| 术语名称 | 公理系统 |
| 英语名称 | axiomatic system |
| 别名 | 希尔伯特风格系统, 希尔伯特式系统, Hilbert-style system |
公理系统(axiomatic system)也称 Hilbert 风格系统/Hilbert 式系统， 是逻辑领域中形式化公理系统的一类，通过几个公理模式和推理规则进行演算。 与普遍的形式化公理系统相比，公理系统的变换仅允许重复、使用规则、引入公理几种，不能使用假言推理规则。
本词条是数理逻辑领域中，被称为公理系统的、使用公理的形式化公理系统。
对于本义的使用公理的系统，见公理系统。
常见规则
命题逻辑通常允许以下规则：
谓词逻辑通常允许以下规则：
- mp（分离规则）
- sub（基于公理的命题变元代入、个体变项代入）
- us/ui（全称特化）
- eg（存在推广）
一个最常见的公理系统是 Hilbert 表示。
特征
公理系统的典型特征是不允许进行假言推理，即推理过程中不引入假设，这是公理系统的根本分类依据。 由于不使用假设，推理中出现的每一行公式都在不需要额外前提的条件下成立。
| 证明论 | ||
|---|---|---|
| 研究动机与结果 | Gödel 完备性定理、 Hilbert 纲领、 Gödel 不完备定理 | |
| 结构化证明 | 推理系统 形式化公理系统 （形式化、公理化） |
Hilbert 风格/公理系统（在无前提的定理间推理）： Hilbert 表示 |
| Gentzen 风格-自然演绎系统（在有前提、有假设的结论间推理）： Gentzen 式自然演绎、 Fitch 式自然演绎、 Suppes–Lemmon 式自然演绎 | ||
| Gentzen 风格-相继式演算（在描述可演绎关系的元定理间推理）： Gentzen 式相继式演算 | ||
| 证明、演绎 | 演绎、可演绎、证明、可证明 | |
| 命题、定理 | 命题、元命题、公理/公理模式、定理、元定理 | |
| 推理规则性质描述 | 保存真实性、保存重言性 | |
| 推理系统性质描述 | 可靠性、完备性/完全性、一致性、独立性 | |
| 重要元定理 | 演绎定理、切消定理（切割消除定理） | |
| （某种推理系统的）可靠性定理、完备性定理 | ||
| 序数分析 | 证明论序数 | |
| 构造性证明 程序化证明 |
Curry–Howard 对应 | |
| 证明复杂度理论 | 证明复杂度 | |