形式系统

形式化的目的，是把“这一推理看起来合理”拆成可逐步核对的问题：公式是否良构，当前有哪些可用假设，所引规则是否适用，以及侧条件是否满足。读者不必重复发明证明思路，便能检查已经给出的证书。

Hilbert 演算常用少数公理模式和公式序列组织证明；自然演绎用引入、消去规则并追踪假设的解除；相继式演算直接把上下文写在判断两侧。同一个推理可以采用不同展示方式，自然演绎也可以写成带子证明范围的行式证明，不能仅凭“树还是序列”判定演算种类。

规则模式如何变成具体证明 ​

考虑只有合取引入与合取消去的片段：从 $A,B$ 得 $A\wedge B$；从 $A\wedge B$ 可分别得 $A$ 或 $B$。由前提 $P\wedge Q$ 可依次推出

这里最后一步将引入规则中的 $A$ 实例化为 $Q$，$B$ 实例化为 $P$。规则所用的 $A,B$ 是表示任意公式的元变量，不是要求证明中必须出现字面字母 A、B。

反之，从 $P\vee (Q\wedge R)$ 不能直接用合取消去得到 $Q$，因为整个前提的最外层联结词是析取。局部规则检查要识别完整语法结构，不能只在字符串中找到一个 $\wedge$ 就套用规则。

假设范围与有效性 ​

在自然演绎里，临时假设 $P$ 并得到 $P$，解除该假设后可证明 $P\to P$；却不能随后继续把已解除的那条 $P$ 当作无条件事实。若忽略假设范围，这样一个看似细小的记账错误就会让系统“证明”任意命题。

命题逻辑演算、带归纳公理模式的 Peano 算术、带集合论公理模式的 ZF理路ZF 集合论公理系统ZF set theory · Zermelo–Fraenkel set theory以成员关系为唯一非逻辑关系，并受控规定集合存在性的标准一阶公理系统。，都是熟悉的例子。后两者还要指定背景逻辑，单列数学公理而不说明推理规则并不是完整演算说明。

如果某条规则要求“该一阶句在所有结构中为真”才可使用，这个条件并未给出一般的有效核验算法。反过来，即使每份证书都可检查，也不保证能对每个输入判定是否存在证书；检查证明与寻找证明是不同问题。

句法可推导关系理路句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。由合法证明的存在性定义；语义蕴涵理路语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。则考察所有模型。可靠性防止规则从真前提出发导出假结论，完备性要求规则能捕获全部语义后承，两者都必须证明，不能由“规则写得精确”自动获得。

形式系统为类型检查、自动定理证明和证明助理提供共同基础。证明搜索可以很复杂，但最终证书可交给较小的检查核心验证；关于一致性、不可判定性和不完备性的研究，也以这层精确接口为起点。