形式陈述

$$ \frac{P\qquad P\to Q}{Q}. $$$$\frac{PP\to Q}{Q}.$$

若前提 $P$$P$ 为真且条件命题 $P\to Q$$P\to Q$ 为真，那么结论 $Q$$Q$ 必为真；因此该规则保持真值。

直觉

“条件已经满足，承诺的结果就可以使用。”它是演绎证明中最常出现的消去步骤。

例子与边界

由“若 $n$$n$ 为偶数，则 $n^2$$n^2$ 为偶数”和“$n$$n$ 为偶数”可推出“$n^2$$n^2$ 为偶数”。反过来从 $Q$$Q$ 与 $P\to Q$$P\to Q$ 推出 $P$$P$ 是肯定后件谬误，并不有效。

推论与应用

自然演绎中的蕴含消去、函数应用以及 Hoare 逻辑中的规则组合都体现了同一结构。

参考资料

• Michael Huth and Mark Ryan, Logic in Computer Science, 2nd ed., §1.2.
• Dirk van Dalen, Logic and Structure, 5th ed., Chapter 1.