句法可推导关系

$\mathrm{\Gamma }⊢\phi$ 是“存在一份合规则的证明证书”，不是“目前看起来大概可以证明”。拿到证书后逐步核验，和在所有可能证书中寻找一个，是两种不同任务；前者可行并不保证后者总能终止。

$⊢$ 是元语言中的关系符号，它谈论前提、公式和证明；$\to$ 则是对象语言中组合公式的联结词。二者可通过演绎定理或蕴含引入规则联系，但并不是同一种符号。类似地，$\models$ 谈模型真假，不能从定义上代换成 $⊢$。

一份逐步可查的推导 ​

令 $\mathrm{\Gamma }=\{P\wedge Q,P\to R\}$。下表给出 $\mathrm{\Gamma }⊢R\wedge Q$ 的自然演绎证明：

这份证书展示了怎样推导；若前提库还含无穷多其他公式，检查它仍只需这里实际用到的两条前提。

临时假设 $P$ 并由它得到 $P$，再解除假设，可以证明 $⊢P\to P$。解除后上下文已经改变，不能再把临时的 $P$ 引用为无条件结论，否则会错误得到 $⊢P$。

不可推导需要理由 ​

在可靠的经典演算中，$P⊬Q$ 可用反赋值证明：取 $P$ 真、$Q$ 假，若存在从 $P$ 到 $Q$ 的证明，可靠性便被违反。这与“搜索十分钟没找到证明”不同；后者没有排除更长证明。

不可推导也不等于可推导否定。仍以前提 $P$ 为例，取 $P,Q$ 同真，便说明 $P⊬\mathrm{\neg }Q$；因此 $Q$ 与 $\mathrm{\neg }Q$ 都可能推不出来。另一方面，若人为只保留前提重复规则而删去逻辑公理与其他规则，空前提下就推不出 $P\vee \mathrm{\neg }P$，尽管它在经典语义下永真。这揭示完备性是演算的实质性质。

在通常经典演算中，增加前提不会毁掉已有证明；把对中间结论的证明接到使用该结论的位置，还可组合证明。这些性质支撑演绎定理、证明模块化以及一致性的研究，但在限制假设复制或丢弃的演算中，要重新检查对应结构规则。

语义蕴涵理路语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。给出外部标准：可靠性理路一阶逻辑可靠性定理Soundness theorem for first-order logic一阶证明系统中可证的公式在每个模型中都语义有效。说明可推导必然语义有效，一阶完备性说明所有语义后承都可推导。配合证明只用有限前提的性质，可以进一步理解紧致性定理为何把无限模型问题归结到有限子集。

若语法和规则实例都可有效检查，且所用公理及前提可递归枚举，可给每次引用附上它在枚举中出现的有限运行见证。这样就能系统枚举并检查有限证明，从而半判定可推导性：存在证明时最终会找到，不存在时却可能永远搜索。证明长度、定理可枚举性和不可判定性，都在研究这个“有限证书存在”的关系。