肯定前件

肯定前件
术语名称	肯定前件
英语名称
别名	MP, 分离规则

肯定前件(modus ponens, affirming the antecedent, MP)是命题逻辑中最重要的推理规则之一，指从条件命题及其前件可以推出后件。

作为推理规则时，称为分离规则。

定理

永真式 [math]\displaystyle{ \vDash P \land (P \rightarrow Q) \rightarrow Q }[/math] 称为肯定前件式(modus ponens)，常缩写为 MP 。

常见等价表达：

• [math]\displaystyle{ \vDash (P \rightarrow Q) \land P \rightarrow Q }[/math]

谓词逻辑肯定前件式

[math]\displaystyle{ \vDash \forall x (P(x) \rightarrow Q(x)) \rightarrow P(a) \rightarrow Q(a) }[/math]

模态逻辑肯定前件式

[math]\displaystyle{ \vDash \Box(P \rightarrow Q) \rightarrow \Box P \rightarrow \Box Q }[/math]

意义

• 在自然演绎系统中，肯定前件是最核心的推理规则之一。
  • 蕴涵消去： [math]\displaystyle{ P, P \rightarrow Q \vdash Q }[/math] 。
• 在 Hilbert 系统中，肯定前件通常作为唯一的推理规则，称为分离规则或 mp 规则，见对应条目：
  • 所有其他推理都可以通过公理和肯定前件推导出来；
  • 这种设计的简洁性体现了肯定前件的根本重要性。
• 肯定前件在日常推理和科学论证中有规范应用：
  • 从一般规律和具体条件推导出特定结论，本质上就是一种肯定前件，对应从一般到特殊的推理规则；
  • 在数学证明、计算机科学的自动推理中都有核心作用。

非经典逻辑中的情况

• 经典逻辑中，作为最基本的推理规则。
• 直觉主义逻辑中同样接受肯定前件，其有效性不依赖于排中律。
• 模糊逻辑中，肯定前件的结论具有真值度，结论的真值度使用特定的蕴含算子和合取算子由前提的真值度计算得出。