形式陈述

一个形式系统通常写成四元组 $(\Sigma,\mathcal F,\mathcal A,\mathcal R)$$(\mathrm{\Sigma },\mathcal{F},\mathcal{A},\mathcal{R})$：$\Sigma$$\mathrm{\Sigma }$ 是指定的符号表，$\mathcal F$$\mathcal{F}$ 是合式公式集合，$\mathcal A\subseteq\mathcal F$$\mathcal{A}\subseteq \mathcal{F}$ 是公理，$\mathcal R$$\mathcal{R}$ 是推导规则。常见可有效处理的系统取有限或可数符号表，并让每条规则只有有限多个前提；但这不是“形式系统”一词在所有文献中的逻辑必然条件，亦存在不可数语言和无穷前提演算。标准有限证明中的定理，是从公理经有限次规则应用得到的公式。

直觉

形式系统把“什么句子合法”与“什么推理允许”完全写成机械规则，使证明可以逐步检查，而不依赖自然语言中的省略和暗示。

例子与边界

命题逻辑、皮亚诺算术与 ZF 集合论都是形式系统。形式系统只规定语法和推导；公式在某个模型中是否为真属于语义问题，不能与“可证明”混为一谈。

推论与应用

它是命题逻辑、一阶逻辑、类型系统、自动机语言以及机器可检查证明的共同入口。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., §1.
• Elliott Mendelson, Introduction to Mathematical Logic, 6th ed., Chapter 1.