语义蕴涵

先用前提筛选允许的情形，再检查结论能否在剩下的情形中失败。因此，语义蕴涵并不要求结论本身永真；前提已经排除的情形，不会成为这次推理的反例。

例如规则说“门打开时警报亮”，又已知门打开。只考察这两项同时成立的状态，警报就必须亮。警报在其他状态可以不亮，这不影响推理。反过来，只知道警报亮，仍容许门关闭且因别的原因报警的状态。

语义蕴涵是对全部允许情形的数学断言。暂时没有搜索到反例，不等于已经证明没有反例；只有搜索确实覆盖了所需范围，或有一般论证排除了它们，才能下结论。

从前提中筛出模型 ​

令 $P$ 为“门打开”，$Q$ 为“警报亮”。对前提 $\{P\to Q,P\}$，$P$ 必须真；此时要让 $P\to Q$ 也真，$Q$ 只能真。因此

若把第二个前提改为 $Q$，赋值 $P=0,Q=1$ 同时满足两个前提，却使结论 $P$ 为假，故 $\{P\to Q,Q\}⊭P$。这个赋值就是反模型。只展示一个使前提和结论都真的状态，既不能证明蕴涵，也不能驳倒它。

结构和变量都不能换掉 ​

在一阶语言中，$\{\mathrm{\forall }x(A(x)\to B(x)),A(c)\}\models B(c)$。任取满足前提的结构，全称前提可用于常量 $c$ 所指的对象；该对象又满足 $A$，所以满足 $B$。这里不要求论域只有一个对象。

但 $\{\mathrm{\exists }xA(x)\}⊭A(c)$。取论域 $\{u,v\}$，让 $A$ 只对 $u$ 成立，而 $c$ 指向 $v$：存在量词有见证，结论却假。存在某个对象满足性质，不能把见证随意换成指定对象。

前提不可能同时成立时 ​

$\{P,\mathrm{\neg }P\}$ 没有模型，所以它蕴涵任意 $R$。定义要求检查的前提真行一行也没有，因而不存在反模型。这叫空真，不提供关于 $R$ 内容的独立信息。若验证工具从规范推出每个目标，应该检查规范是否已经互相冲突。

在经典语义下，$\mathrm{\Gamma }\models \phi$ 等价于 $\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}$ 不可满足：两边排除的是完全相同的反模型。若 $\mathrm{\Gamma }$ 有限，还可把前提写成一个合取公式；若 $\mathrm{\Gamma }$ 无限，一般不能直接写成普通有限语法中的“无限合取”。

句法可推导理路句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。 $\mathrm{\Gamma }⊢\phi$ 则要求按指定规则构造证明。可靠性保证可推导必语义蕴涵；完备性保证反向成立。它们是关于所选证明系统与语义的定理，不是两个符号可互换的默认约定。

命题反模型搜索可交给 SAT 求解器；带背景理论的公式通常需要 SMT 或相应理论的推理工具。一般一阶逻辑不能直接用有限真值表穷尽全部结构。模型检查理路模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。另有一项固定输入：给定状态模型 $M$，检查 $M\models \phi$。它与在整个结构类上证明 $\mathrm{\Gamma }\models \phi$ 的问题范围不同。