命题逻辑可靠性与完备性定理

可靠性说形式演算不会证明语义错误的结论，完备性说它不会漏掉任何由命题真值结构强制的结论。两者合起来使 $\mathrm{\Gamma }⊢\phi$ 与 $\mathrm{\Gamma }\models \phi$ 完全一致：句法既不越界，也不遗漏有效后果。证明系统可以采用不同的具体规则，但目标都是刻画同一个语义关系。

因为 $\{p,p\to q\}\models q$，完备性保证在完整演算中可推出 $q$；因为 $p\vee q⊭p$，可靠性保证不能从前者合法推出后者。一个只含 modus ponens 而没有足够公理的弱系统可能可靠却不完备；加入不保真的规则则会越过语义边界，极端时甚至证明所有公式。可靠性通常对推导长度归纳，逐条验证公理永真且规则保真；完备性则可用真值表、规范形或极大一致集构造反赋值。定理始终针对已指定并分别核验两个方向的演算，不会自动授予任意符号规则。

该定理把句法可推导与命题逻辑页自足定义的真值语义后承对齐，证明命题推理既可信又充分，因而支持证明搜索、自动验证和等价变换。它保证搜索找到证明时结论正确，也解释 SAT 反例为何能见证不可推导；命题变量有限时真值表会终止，这与命题逻辑的可判定性一致。模型论中的一般语义蕴涵公理库语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。以及一阶逻辑公理库一阶逻辑First-order logic · Predicate logic在命题逻辑上加入对象、关系、函数与量词的形式语言和模型语义。完备性沿相同问题意识展开，但使用更丰富的结构语义。