形式系统是一套精确定义的框架，用于构造符号表达式，并按照明确的规则推导结论。在逻辑学和数学中，它通常由语言、公理和推理规则组成。其根本特征在于：一个推导是否合乎要求，取决于它的形式结构，而不是对表达式含义的某些未明言的直觉。如果系统的描述是有效的，这些要求就可以通过机械程序来检查。(plato.stanford.edu)
组成部分与推导
形式系统区分可以写出的表达式与能够算作合法结论的表达式。它通常包含以下组成部分：
- **形式语言：**由符号和形成规则组成，规定哪些表达式是允许的，即哪些是合式公式。在谓词语言中，这些规则区分表示对象的项与表达条件或断言的公式。
- **公理：**在系统内无需推导、直接作为起点接受的公式。公理模式通过允许适当的替换来规定一族公理。
- **推理规则：**规定如何从指定前提推导结论，并须遵守所列出的限制条件。
- **形式证明：**有限且具有明确结构的推导，其中每一步都以公理、假设或推理规则为依据。一个公式若在没有未消解假设的情况下得到证明，就是该系统的定理。(builds.openlogicproject.org)
例如，肯定前件式允许从 (P) 和 (P\rightarrow Q) 推出 (Q)。这里的字母代表任意公式，而不是特定的英语句子。因此，这条规则描述的是一种可反复使用的演绎推理模式。相比之下，形成规则决定的是 (P\rightarrow Q) 这样的表达式是否属于该语言，而不是将这些表达式确立为定理。(builds.openlogicproject.org)
不同的证明体系以不同方式组织推导。公理式演算通常采用公式序列，并使用相对较少的推理规则。自然演绎允许引入临时假设，并提供消解这些假设的规则。相继式演算则使用将一组前提与结论联系起来的判断。不同演算可以刻画同一种后承关系，同时明确呈现证明结构的不同方面。(builds.openlogicproject.org)
句法与解释
句法与语义学之间的区分至关重要。句法涉及符号、公式和推导。语义学提供解释，使公式具有意义和真值条件。在命题逻辑中，解释为命题变元指派真值。在一阶逻辑中，解释规定一个论域，并为语言中的常量、函数符号和关系符号赋予意义。(builds.openlogicproject.org)
记号 [ \Gamma\vdash\varphi ] 表示可以从假设 (\Gamma) 形式地推导出 (\varphi)。相比之下， [ \Gamma\models\varphi ] 表示每一个满足 (\Gamma) 中所有公式的解释也都满足 (\varphi)。两者分别表达句法上的可推导性与语义上的后承关系。它们之间的对应关系需要证明，并非由记号本身规定。(forallx.openlogicproject.org)
形式系统不一定只有一种预期解释。一个理论的模型是满足其公理的结构，而这些结构之间可能存在很大差异。模型论研究这些结构及其与理论的关系，证明论则研究推导及其数学性质。关于某个系统的陈述，例如确立其可靠性的定理，属于该系统的元理论，而不会自动成为该系统内部的定理。(builds.openlogicproject.org)
可靠性、一致性与完备性
以下几种性质描述了形式系统的不同方面：
相对于某种语义而言，可靠性意味着可推导性蕴含语义后承关系：若 (\Gamma\vdash\varphi)，则 (\Gamma\models\varphi)。可靠的演算不会推导出在指定解释规则下并不由其前提推出的结论。(forallx.openlogicproject.org)
在通常的经典逻辑背景下，一致性意味着不存在一个语句及其否定都可被证明的情况。可靠性与一致性并不相同：可靠性将证明与语义相比较，而一致性关注的是哪些内容可以被推导出来。对于经典逻辑而言，一个可靠且具有模型的理论是一致的。(plato.stanford.edu)
语义完备性意味着每一个语义后承都可以被推导出来。哥德尔完备性定理为标准一阶逻辑确立了这一对应关系。然而，理论的完备性意味着，对于其语言中的每一个语句，该理论都能证明这个语句或其否定。因此，完备的逻辑演算也可以承载不完备的理论。(forallx.openlogicproject.org)
如果一个公理无法从其余公理推导出来，它就独立于其余公理。独立性问题关乎特定假设的强度，而不只是底层推理规则是否正确。(builds.openlogicproject.org)
有效程序与局限
一个具有有效描述的系统允许使用算法检查其证明。然而，检查一个给定的证明，与判定是否存在某个证明，是不同的问题。通过有效枚举证明，最终可以找到某个定理的推导；但如果所考察的陈述不是定理，这一过程可能永远持续下去。经典命题逻辑中的有效性可以通过有限真值表判定，而一般的一阶逻辑有效性则是不可判定的。(plato.stanford.edu)
哥德尔不完备定理确立了进一步的局限。每一个一致、可有效公理化且足够强以表达初等算术的理论，都包含既不能被该理论证明、也不能被其否证的语句。在满足适当的强度和形式化条件时，这样的理论也无法证明其自身的标准一致性陈述。这些结果并非不加区分地适用于所有符号演算，也不与一阶逻辑的语义完备性相冲突。(plato.stanford.edu)
历史发展与计算机辅助证明
戈特洛布·弗雷格于1879年出版的《概念文字》引入了一个形式逻辑框架，用于分析含有量词的陈述和数学证明。此后，大卫·希尔伯特通过希尔伯特纲领推动对形式化数学的研究，其中包括寻求有限主义的一致性证明。哥德尔于1931年得到的结果，对这一纲领最初的目标构成了重大限制。(plato.stanford.edu)
形式系统也是证明助手和形式验证的基础。在Lean证明助手中，数学断言在类型论框架内表达，内核则依据底层规则检查证明项。通过检查意味着该断言可从所使用的定义和公理推导出来；这并不能独立确立该形式陈述准确表达了预期的非形式含义，也不能确立所假定的每条公理都有充分依据。(lean-lang.org)