“完备性是模型论与证明论之间的桥梁，两侧的搬运都富有成果。由"证明只用有限多前提"立即得到紧致性定理：有限可满足的理论整体可满足——非标准分析的无穷小模型、图着色的从有限到无限的提升都由此而来…”
形式陈述
形式演算先指定语法：符号、项、公式、绑定和避免变量捕获的代换规则。它再指定一种或多种 judgment 形状，例如
公理是零前提规则，公理模式则代表一族可实例化规则。推导是以目标 judgment 为根、每个节点由规则实例支持的良基证明对象；通常规则只有有限前提，抽象的无穷演算也可允许无限分支。常见机械证明系统要求语法、规则实例和有限推导均可有效检查，但“有效可检查”是重要的附加设计条件，并非所有抽象形式演算的定义必然项。
直觉
形式系统把“哪些表达式有意义”“正在证明哪类判断”和“局部推理怎样连接”分开写清。Hilbert 演算把上下文藏在公理与序列中，自然演绎会显式打开并解除假设，相继式演算直接让上下文成为判断两侧；它们的证明形状不同，却都能由“judgment 加规则生成推导”这一接口容纳。语义可用于评价演算是否可靠、完备，却不是句法推导本身的一部分。
例子与边界
命题逻辑、皮亚诺算术与 ZF 集合论都是形式系统。形式系统只规定语法和推导；公式在某个模型中是否为真属于语义问题，不能与“可证明”混为一谈。
命题 Hilbert 系统可只用少量公理模式与 modus ponens；自然演绎则用引入、消去规则组织假设。一个规则若要求“该句在所有模型中为真”才能应用，就不再是纯粹有效可检验的句法规则。形式系统也可能一致但不完备，或规则可枚举却定理集合不可判定。
推论与应用
它是命题逻辑、一阶逻辑、类型系统以及机器可检查证明的共同入口。形式语言只给出表达式集合；形式系统还必须固定 judgment、规则和推导对象。
句法可推导关系由合法推导对象定义，语义蕴涵提供外部正确性标准。Gödel 不完备定理、自动定理证明与证明助理都依赖证明对象的形式化和机械核验。
参考资料
- Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001, §1.
- Elliott Mendelson, Introduction to Mathematical Logic, 6th ed., Chapman and Hall/CRC, 2015, Chapter 1.