一阶逻辑可靠性定理

可靠性把一个可能很长的证明拆成可以分别检查的小步。若每条规则都把满足当前未撤销假设的解释带到真结论，那么把这些规则接成有限证明，也不会产生反模型。这是关于整套演算的元定理，而不是要求逐条枚举所有模型。

量词规则比命题规则多一个危险：某个对象满足性质，不等于所有对象都满足。自然演绎中的“任意对象”必须确实任意，不能依赖未撤销假设对它施加的特殊条件。规则的侧条件正是在保护这一点。

以全称引入的自由变量记法为例，由 $\mathrm{\Gamma }⊢\psi$ 推出 $\mathrm{\Gamma }⊢\mathrm{\forall }x\psi$，要求 $x$ 不自由出现在 $\mathrm{\Gamma }$ 中。归纳假设给出 $\mathrm{\Gamma }\models \psi$。固定满足 $\mathrm{\Gamma }$ 的结构 $\mathcal{M}$ 与赋值 $s$，任取论域元素 $d$；因为 $x$ 不在开放假设中自由出现，改成 $s[x\mapsto d]$ 后仍满足 $\mathrm{\Gamma }$。归纳假设于是给出 $\mathcal{M},s[x\mapsto d]\models \psi$。这对每个 $d$ 都成立，恰好说明 $\mathcal{M},s\models \mathrm{\forall }x\psi$。新参数版本则改变该参数的解释，论证中的独立性条件相同。

一次推导的语义核对 ​

从 $\mathrm{\forall }x(P(x)\to Q(x))$ 与 $P(a)$ 推出 $Q(a)$，分为两步：全称消去利用替换引理理路一阶替换引理Substitution lemma for first-order logic语法上的无捕获项替换与语义上的变量赋值更新相一致。先得到 $P(a)\to Q(a)$，再由肯定前件理路肯定前件Modus ponens · Implication elimination从命题 P 和蕴含 P→Q 推出 Q 的基本推理规则。规则得到 $Q(a)$。取任意同时满足两前提的结构，第一步读取全称句在 $a$ 所指对象上的实例；第二步只使用蕴涵的真值条件。两步都不依赖论域具体是数字、人还是图顶点。

删去侧条件会发生什么 ​

在整数结构中把 $P(x)$ 解释为“$x=0$”，并令赋值满足 $s(x)=0$。假设 $P(x)$ 为真，但 $\mathrm{\forall }xP(x)$ 为假，因为整数 $1$ 不满足它。因此从尚未撤销的 $P(x)$ 直接全称化是不可靠的；要求 $x$ 不自由出现在这些假设中，排除了这个反例。

证明系统也可能可靠而不完备。例如只允许重复前提的演算不会推出错误结论，却无法从 $P\wedge Q$ 得到 $P$。可靠性只限制“不应多证”，完备性另外要求“该证的都能证”。

如果 $\mathrm{\Gamma }$ 有模型，可靠性保证不能同时证明 $\psi$ 和 $\mathrm{\neg }\psi$。若 $\mathrm{\Gamma }$ 本来无模型，$\mathrm{\Gamma }\models \phi$ 对任意 $\phi$ 都真，这种空真不说明前提描述了真实存在的对象。

句法推导理路句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。由规则产生，语义蕴涵理路语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。由所有模型定义；可靠性给出前者包含于后者，也允许用一个反模型立即否定可推导性。与 一阶完备性定理理路一阶逻辑完备性定理Gödel completeness theorem · Completeness theorem for first-order logic每个语义有效的一阶公式都可在合适证明系统中形式证明。合并后，两种后果关系一致，为程序验证、自动定理证明、证明助理内核和形式化数学提供理论保证。