肯定前件

肯定前件是逻辑学中的一条推理规则，允许从前提“如果 (P)，那么 (Q)”和 (P) 推出结论 (Q)。它是演绎推理的一种基本形式，适用于命题逻辑以及表达能力更强的逻辑系统。它也称为蕴涵消去，规定了当前件已经成立时，如何运用一个已成立的条件命题。这条规则的核心特征是保真性：在蕴涵的标准解释下，真前提不可能产生假结论。(en.wikipedia.org)

形式与解释

这条规则通常表示为：

[ \frac{P\rightarrow Q\qquad P}{Q}. ]

这里，(P) 是条件命题 (P\rightarrow Q) 的前件，(Q) 是其后件。横线将前提与结论分开；它本身不是逻辑语言中的联结词。这些字母可以代表复杂公式，而不只是原子命题。应用这条规则时，单独确立的前提必须与条件命题的前件一致。(plato.stanford.edu)

例如：

如果一个整数能被四整除，那么它就能被二整除。
十二能被四整除。
因此，十二能被二整除。

这一推理依赖的是论证的形式，而不是其具体涉及的数学内容。同样的模式也适用于 (P\rightarrow(Q\land R))：一旦 (P) 成立，肯定前件规则就能推出整个后件 (Q\land R)，而不只是其中的某一个部分。(plato.stanford.edu)

语义有效性

在经典逻辑中，条件命题通常按实质蕴涵解释。只有当前件为真而后件为假时，条件命题才为假。因此，可以用真值表验证肯定前件规则：

(P)	(Q)	(P\rightarrow Q)	两个前提是否都为真？
真	真	真	是
真	假	假	否
假	真	真	否
假	假	真	否

两个前提都为真的唯一一行，也使结论为真。这就确立了该规则的逻辑有效性：不存在使前提为真而结论为假的解释。有效性并不能证明某个具体论证的前提实际上为真；那是另一个问题。(plato.stanford.edu)

与之对应的公式

[ ((P\rightarrow Q)\land P)\rightarrow Q ]

在经典逻辑中是一个重言式。不过，公式与推理规则的作用不同。公式是逻辑语言中可被赋予真值的表达式；规则则允许在推导过程中从一些表达式过渡到另一个表达式。(iep.utm.edu)

在证明系统中的作用

在自然演绎中，肯定前件是蕴涵的消去规则，通常记作 (\rightarrow E)。与之对应的蕴涵引入规则，是在临时假设 (P) 下推导出 (Q)，然后解除该假设，从而确立 (P\rightarrow Q)。蕴涵消去则利用一个已有的条件命题及其前件。这两条互补的规则说明了如何证明和使用蕴涵。(plato.stanford.edu)

在希尔伯特式证明系统中，配合适当的公理模式，肯定前件可以作为命题逻辑唯一的推理规则。此时，形式证明由一系列公式构成，其中每个公式要么是公理的实例，要么是对先前公式应用肯定前件规则的结果。如果没有公理或前提，单凭这条规则并不能构成完整的逻辑演算。这种组织方式在证明论中十分重要，例如可用于证明某个演算具有保真性。(iep.utm.edu)

肯定前件也用于一阶逻辑，与量词规则配合使用。直觉主义逻辑同样保留了这条规则：应用蕴涵并不需要双重否定消去这一经典逻辑特有的原则。(plato.stanford.edu)

历史发展

斯多葛学派的逻辑中已经出现了与肯定前件相对应的古代推理形式；这一逻辑尤其由公元前三世纪的克律西波发展起来。斯多葛学派承认一种基本的“不可证明式”论证，它从条件命题及其前件推出后件。他们以命题为基础的方法，不同于与亚里士多德相关、以词项为基础的三段论。这里的历史连续性体现在推理模式上；不应直接将古代对条件命题的解释等同于现代的实质蕴涵。(plato.stanford.edu)

计算解释

在柯里—霍华德对应下，蕴涵被解释为函数类型。(P\rightarrow Q) 的证明相当于一个函数，它接受 (P) 的证明并返回 (Q) 的证明；肯定前件则对应于函数应用。这种解释将逻辑推理与类型论及机器核验的证明联系起来。例如，在Lean证明助手中，如果有 h : P → Q 和 hp : P，那么表达式 h hp 就是 Q 的一个证明。对两个前提的依赖直接体现在证明项中。(docs.lean-lang.org)

形式与解释

语义有效性

在证明系统中的作用

相关模式与无效模式

历史发展

计算解释