公理系统（逻辑）

公理系统
术语名称	公理系统
英语名称	axiomatic system

公理系统(axiomatic system)是逻辑领域中形式化公理系统的一类， 通过几个公理模式和推理规则进行演算。 与普遍的形式化公理系统相比，公理系统的变换仅允许重复、使用规则、引入公理几种，不能使用假言推理规则。

本词条是数理逻辑领域中，被称为公理系统的、使用公理的形式化公理系统。

对于本义的使用公理的系统，见公理系统。

常见规则

命题逻辑通常允许以下规则：

• mp（分离规则）
• sub（基于公理的命题变元代入）

谓词逻辑通常允许以下规则：

• mp（分离规则）
• sub（基于公理的命题变元代入、个体变项代入）
• us/ui（全称特化）
• eg（存在推广）

一个最常见的公理系统是 Hilbert 表示。

特征

公理系统的典型特征是不允许进行假言推理，即推理过程中不引入假设，中间出现的每一行公式都在不需要额外前提的条件下成立。

证明论
形式化公理系统（形式化、公理化）
形式化范式	公理系统、自然演绎系统、相继式演算
证明、演绎	证明、可证明、演绎、可演绎
命题、定理	公理、定理、元定理、变形规则
推理规则性质	保存真实性、保存重言性
公理系统性质	可靠性、完全性、一致性、独立性