一阶逻辑可靠性定理

一阶可靠性定理说，形式证明不能从真前提出发推出语义上的假结论。证明对推导逐步归纳：公理在任意结构下有效，每条规则都是局部保真的，有限串联后仍然保真。它保证证明系统不会“制造”语义错误，但不保证所有语义真理都能证明，后者属于完备性。

从 $\mathrm{\forall }x(P(x)\to Q(x))$ 与 $P(a)$ 推出 $Q(a)$，在任意同时满足两前提的结构中都成立。若 $\mathrm{\Gamma }$ 有模型而演算可靠，则不可能同时推出 $\psi$ 与 $\mathrm{\neg }\psi$，所以语义可满足性蕴含语法一致性。反之，可靠性本身不保证所有语义后果都可证明；一个只含少数规则的演算可能可靠却严重不完备。

modus ponens 的可靠性来自：若 $\phi$ 与 $\phi \to \psi$ 都真，则 $\psi$ 真。全称化规则需限制被量化变量不自由出现在未关闭假设中，否则会从某个特定赋值成立错误推出对所有对象成立。若系统加入一条不保真的公理，可靠性立即失效。

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