公理系统（逻辑）：修订间差异

2026年1月15日 (四) 13:13的最新版本

公理系统
术语名称	公理系统
英语名称	axiomatic system
别名	希尔伯特风格系统, 希尔伯特式系统, Hilbert-style system

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

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

常见规则

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

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

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

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

特征

公理系统的典型特征是不允许进行假言推理，即推理过程中不引入假设，这是公理系统的根本分类依据。由于不使用假设，推理中出现的每一行公式都在不需要额外前提的条件下成立。

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

@@ 第1行： / 第1行： @@
-[[分类:证明论]]
+[[分类:证明论]]{{DEFAULTSORT:gong1li3xi4tong3}}
+{{#seo:
+|keywords=希尔伯特风格系统, 希尔伯特式系统, 公理系统
+|description=希尔伯特风格系统指一类形式化公理化的推理系统中不使用假言推理规则，即不使用假设的推理系统，每一行的公式被满足都不需要前提。本文介绍这一类系统的特点、常见规则、性质。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-09
+}}
 {{InfoBox
 |name=公理系统
 |eng_name=axiomatic system
+|aliases=希尔伯特风格系统,希尔伯特式系统,Hilbert-style system
 }}
-'''公理系统'''('''axiomatic system''')是逻辑领域中[[形式化公理系统（逻辑）|形式化公理系统]]的一类，
+'''公理系统'''('''axiomatic system''')也称 '''Hilbert 风格系统'''/'''Hilbert 式系统'''，
-通过几个[[公理模式]]和推理规则进行演算。
+是逻辑领域中[[形式化公理系统（逻辑）|形式化公理系统]]的一类，通过几个[[公理模式]]和推理规则进行演算。
 与普遍的形式化公理系统相比，公理系统的变换仅允许重复、使用规则、引入公理几种，不能使用假言推理规则。
@@ 第17行： / 第24行： @@
 [[:分类:命题逻辑|命题逻辑]]通常允许以下规则：
 * [[分离规则|mp（分离规则）]]
-* sub（基于公理的[[代入]]）
+* sub（基于公理的[[命题变元代入]]）
 [[:分类:谓词逻辑|谓词逻辑]]通常允许以下规则：
+* [[分离规则|mp（分离规则）]]
+* sub（基于公理的[[命题变元代入]]、[[个体变项代入]]）
 * [[全称特化|us/ui（全称特化）]]
 * [[存在推广|eg（存在推广）]]
+一个最常见的公理系统是 [[Hilbert 表示]]。
+== 特征 ==
+公理系统的典型特征是不允许进行假言推理，即推理过程中不引入假设，这是公理系统的根本分类依据。
+由于不使用假设，推理中出现的每一行公式都在不需要额外前提的条件下成立。
 {{证明论}}