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

[[分类:证明论]]{{DEFAULTSORT:gong1li3}}
{{#seo:
|keywords=证明论, 公理, 公理模式, 公设
|description=证明论中，不需要进行证明，当作不证自明的命题称为公理。本文介绍了公理的定义、性质及其衍生术语。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-01
}}
{{InfoBox
|name=公理
|eng_name=axiom
|a;oases=公设,postulate
}}
{{InfoBox
|name=公理模式
|eng_name=axiom schema
}}
'''公理'''('''axiom''')指没有经过证明，被当作不证自明的命题。
若规定符合某形式的公式都是公理，则称为'''公理模式'''('''axiom schema''')。
公理在相关理论中其真实性理所当然，且是作为推导、演绎的起点。
在推理系统中，描述命题形式推理规则的称为逻辑公理，
其他涉及非逻辑部分的公理是非逻辑公理，也称为'''公设'''('''postulate''')。

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

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

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

=== 分类 ===

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


{{证明论}}