查看“︁公理系统（逻辑）”︁的源代码

[[分类:证明论]]
{{InfoBox
|name=公理系统
|eng_name=axiomatic system
}}
'''公理系统'''('''axiomatic system''')是逻辑领域中[[形式化公理系统（逻辑）|形式化公理系统]]的一类，
通过几个[[公理模式]]和推理规则进行演算。
与普遍的形式化公理系统相比，公理系统的变换仅允许重复、使用规则、引入公理几种，不能使用假言推理规则。

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

对于本义的使用公理的系统，见[[公理系统]]。
</blockquote>

== 常见规则 ==
[[:分类:命题逻辑|命题逻辑]]通常允许以下规则：
* [[分离规则|mp（分离规则）]]
* sub（基于公理的[[命题变元代入]]）
[[:分类:谓词逻辑|谓词逻辑]]通常允许以下规则：
* [[分离规则|mp（分离规则）]]
* sub（基于公理的[[命题变元代入]]、[[个体变项代入]]）
* [[全称特化|us/ui（全称特化）]]
* [[存在推广|eg（存在推广）]]

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

== 特征 ==

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


{{证明论}}