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

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

形式化公理系统(formal axiomatic system)，通常指形式化的、公理化的推理系统，即含有一系列公理、使用形式语言的推理系统。按形式语言的定义，有原子集合和算子集合；此外，作为公理化系统，包含一个公理的集合；作为逻辑的演算系统，还包含一个推演规则的集合。在这些推演规则下，可以结合公理对公式（前提）进行一系列演绎；不需要前提，仅需要公理和推演规则就能进行的演绎称为证明，其结果是系统中的定理。

记号

通常记形式化公理系统为 [math]\displaystyle{ \mathcal{L} = \mathcal{L} \langle A, \Omega, Z, I \rangle }[/math]，四元组中：

[math]\displaystyle{ A }[/math] 是语言中的原子公式或句子的终端元素的集合。对逻辑演算，包括全部原子命题，即命题常量及命题变元。
[math]\displaystyle{ \Omega }[/math] 是语言中的全部算子符号的集合。对逻辑运算，是全部逻辑联结词的有限集合。
[math]\displaystyle{ Z }[/math] 是形式系统的全部变换规则的有限集合。对逻辑演算，称为推理规则。每个规则都由原子公式和算子符号构成。
[math]\displaystyle{ I }[/math] 是形式系统的起始点的有限集合。对逻辑运算，称为公理。

种类

公理的数目和推理规则的数目是相权衡的，根据权衡的结果有不同的类别。推理规则较多而不使用公理的属于 Gentzen 风格系统，主要有自然演绎系统和相继式演算等；相反，使用公理的称为 Hilbert 风格系统或公理系统。公理系统中极端地使用尽可能少的推理规则，而公理较多的是 Hilbert 表示，一般仅使用一两条规则。

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

@@ 第1行： / 第1行： @@
-[[分类:证明论]]
+[[分类:证明论]]{{DEFAULTSORT:xing2shi4hua4gong1li3xi4tong3}}
+{{#seo:
+|keywords=形式化公理系统
+|description=形式化公理系统指形式化的、公理化的系统，在逻辑领域中特指用于推理的形式化的公理系统。本文讲述了形式化公理系统的定义、相关记号、分类和常见的例子。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-09
+}}
 '''形式化公理系统'''('''formal axiomatic system''')，通常指形式化的、公理化的推理系统，即含有一系列[[公理（逻辑）|公理]]、使用[[形式语言]]的推理系统。
 按形式语言的定义，有原子集合和算子集合；
@@ 第16行： / 第22行： @@
 == 种类 ==
 公理的数目和推理规则的数目是相权衡的，根据权衡的结果有不同的类别。
-推理规则较多而不使用公理的属于[[自然演绎系统]]；
+推理规则较多而不使用公理的属于 Gentzen 风格系统，主要有[[自然演绎系统]]和[[相继式演算]]等；
-相反，使用公理的称为[[公理系统（逻辑）|公理系统]]。
+相反，使用公理的称为 Hilbert 风格系统或[[公理系统（逻辑）|公理系统]]。
 公理系统中极端地使用尽可能少的推理规则，而公理较多的是 [[Hilbert 表示]]，一般仅使用一两条规则。
 {{证明论}}