正式系统
形式系统是用于通过一组推理规则从公理中推断出理论的公理系统的抽象结构或形式化。
1921年，戴维·希尔伯特（David Hilbert）建议将正式系统作为数学知识的基础。
形式主义一词有时是正式系统的粗略同义词，但它也指给定的符号风格，例如，保罗·迪拉克（Paul Dirac ）的胸罩式符号。
概念
正式系统具有以下内容：
如果公理和推理规则集分别是可决定的，则形式系统是递归（IE有效）或递归枚举的。
形式语言
形式语言是由正式系统定义的语言。像语言学中的语言一样，形式语言通常有两个方面：
通常，仅通过形式语法的概念来考虑形式语言的语法。正式语法的两个主要类别是生成语法的类别，它们是如何编写语言字符串以及分析语法（或还原语法）的规则集，这是字符串如何成为字符串的规则集分析以确定它是否是该语言的成员。
演绎系统
演绎系统，也称为演绎设备，由公理（或公理架构）和推理规则组成，可用于得出系统的定理。
这种演绎系统保留了系统中表达的公式中的演绎质量。通常，我们关注的质量是真理，而不是虚假。但是，可以保留其他方式，例如理由或信念。
为了维持其演绎诚信，必须定义一个演绎设备，而无需参考任何对语言的预期解释。目的是确保派生的每一行只是先前的线的逻辑结果。对语言的任何解释都不应有任何要素，这些语言与系统的演绎性质有关。
该系统通过其逻辑基础的逻辑后果（或索引）是将形式系统与其他系统区分开来的，这些系统可能在抽像模型中具有某种依据。通常，正式系统将是与更大的理论或领域（例如欧几里得几何形状）相符合现代数学（例如模型理论）一致的基础。
演绎系统的一个示例是一阶逻辑。
演绎系统的两种主要类型是证明系统和正式语义。
证明系统
形式证明是形成良好的公式（或简称WFF）的序列，它们可能是公理，或者是在证明序列中对以前的WFF应用推断规则的产物。序列中的最后一个WFF被认为是定理。
一旦给出了正式系统，就可以定义可以在正式系统中证明的定理集。该集合由所有有证据的WFF组成。因此，所有公理都被视为定理。与wff的语法不同，不能保证会有决定给定的WFF是否为定理的决策程序。
生成正式证据的观点通常是数学的观点通常称为形式主义。戴维·希尔伯特（David Hilbert）创立了MetAmashematics ，作为讨论正式系统的学科。任何人用来谈论正式系统的语言都称为金属语言。金属语言可能是一种自然语言，或者可能是部分形式化的，但通常比正在检查的正式系统的正式语言组成部分完全正式化，然后被称为对象语言，即讨论中的讨论。刚刚定义的定理概念不应与有关形式系统的定理相混淆，为了避免混乱，通常称为元膜。
逻辑系统的正式语义
逻辑系统是演绎系统（最常见的一阶逻辑），以及其他非逻辑公理。根据模型理论，可以给出逻辑系统的解释，以描述给定的结构- 公式对特定含义的映射 - 满足形成良好的公式。满足正式系统所有公理的结构被称为逻辑系统的模型。
逻辑系统是：
逻辑系统的一个例子是Peano算术。算术的标准模型将话语的领域设置为非负整数，并赋予符号通常的含义。还有非标准的算术模型。
历史
早期的逻辑系统包括印度的Pāṇini逻辑，亚里士多德的三段论逻辑，斯多葛派的命题逻辑以及Gongsun Long的中国逻辑（公元前325 - 250年）。最近，贡献者包括乔治·布尔，奥古斯都·德·摩根和戈特洛布·弗莱格。数学逻辑是在19世纪欧洲开发的。
戴维·希尔伯特（David Hilbert）煽动了一项名为希尔伯特（Hilbert）计划的形式主义运动，以此作为对数学基础危机的拟议解决方案，最终被戈德尔（Gödel）的不完整定理所缓解。 QED宣言代表了随后的，尚未成功的努力，旨在正式化已知数学。