形式化公理系统（逻辑）

形式化公理系统(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] 是形式系统的起始点的有限集合。对逻辑运算，称为公理。

种类

公理的数目和推理规则的数目是相权衡的，根据权衡的结果有不同的类别。 推理规则较多而不使用公理的属于自然演绎系统； 相反，使用公理的称为公理系统。 公理系统中极端地使用尽可能少的推理规则，而公理较多的是希尔伯特表示，一般仅使用一两条规则。

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