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

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

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

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


{{证明论}}