句法可推导关系

句法可推导 $\mathrm{\Gamma }⊢\phi$ 意味着存在一份有限证明证书，其中局部节点都由演算规则核验。上下文的引入、解除和结构规则是 judgment 的一部分，不能总压成“前面出现过哪些公式”的线性历史。它只依赖符号与规则，不直接询问所有模型中的真假；即使前提集 $\mathrm{\Gamma }$ 无限，某份有限证明也只会用到其中有限多条。可靠性与完备性研究它何时与语义蕴涵吻合。

在自然演绎中 $P\wedge Q⊢P$。符号 $⊢$ 依赖所选语言、公理和规则，不是对象语言中的蕴含联结词，也不自动表示语义真。

在含 modus ponens 的系统中，从 $P$ 与 $P\to Q$ 可推导 $Q$。若某公式在所有真值赋值下成立，却系统缺少足够公理，它可能语义有效但不可推导。记号 $\mathrm{\Gamma }⊬\phi$ 断言不存在证明，不能由“目前没找到”直接得出。

形式系统公理库形式系统Formal system · Formal calculus由符号、形成规则、公理与推导规则组成的精确定义系统。规定证明规则，语义蕴涵公理库语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。提供外部比较。演绎定理、一致性、可判定性和证明检查都以句法推导为共同接口，可靠性公理库一阶逻辑可靠性定理Soundness theorem for first-order logic一阶证明系统中可证的公式在每个模型中都语义有效。与完备性则连接它和语义的两个方向；可枚举性、证明长度和不可判定性也都以句法推导为研究对象。