语义蕴涵

$\mathrm{\Gamma }\models \phi$ 表示每个满足全部前提 $\mathrm{\Gamma }$ 的模型也满足结论 $\phi$。换个角度说，只要找不到“前提全真而结论为假”的反例世界，结论就被前提逻辑强制。它是对所有模型的外部量化，与具体证明系统无关，只关心真假保持而不关心推导长度。若 $\mathrm{\Gamma }$ 本身不可满足，它便语义蕴涵任意公式；这是因为根本没有满足前提的反模型，属于真空成立。

$\{P\to Q,P\}\models Q$，但 $\{P\to Q,Q\}⊭P$，取 $P$ 假、$Q$ 真即可给出反模型；同理，$P\vee Q⊭P$。自然语言中的因果“导致”与语义蕴涵不同，这里不涉及时间或因果，只比较同一赋值下的真值约束。若 $\mathrm{\Gamma }=\{P,\mathrm{\neg }P\}$，不存在满足前提的赋值，于是对任意 $R$ 都有 $\mathrm{\Gamma }\models R$；这不是证明了 $R$ 的内容，而是前提集无模型。爆炸性的这一边界也说明，建模前应先检查前提的一致性，否则任何目标都会被平凡蕴涵。

满足关系公理库满足关系Satisfaction relation · Tarski semantics用对公式构造的递归定义刻画结构与赋值何时满足一阶公式。定义模型，句法可推导公理库句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。则由证明规则定义。可靠性给出 $⊢\Rightarrow \models$，完备性给出反向；求反例时，命题公式或有限 Boolean 编码可交给 SAT，带背景理论的公式通常交给 SMT，而一般一阶有效性需要定理证明或模型查找，不能统称为“交给 SAT”。模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。又是另一层问题：它先固定状态模型 $M$，再判定 $M\models \phi$，并不对语义结构类中的所有模型做 $\mathrm{\Gamma }\models \phi$ 的外部量化。分清固定模型的满足、全体模型上的蕴涵与所选验证算法，才能准确解释一份反例究竟否定哪层断言。