否定后件

否定后件
术语名称	否定后件
英语名称
别名	MT, 拒取式

否定后件(modus tollens, denying the consequent, MT)是命题逻辑中的定理，指从条件命题及其后件的否定可以推出前件的否定。与肯定前件的形式对应，有时也作为基本推理规则。

定理

永真式 [math]\displaystyle{ \vDash \lnot Q \land (P \rightarrow Q) \rightarrow \lnot P }[/math] 称为否定后件式(modus tollens)，常缩写为 MT 。

常见等价表达：

• [math]\displaystyle{ \vDash (P \rightarrow Q) \land \lnot Q \rightarrow \lnot P }[/math]
• 在只能使用否定和推出时，也写为 [math]\displaystyle{ \vDash (P \rightarrow Q) \rightarrow \lnot Q \rightarrow \lnot P }[/math] 此时形式与假言易位律相同。

谓词逻辑否定后件式

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

模态逻辑否定后件式

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

意义

• 在自然演绎系统中，否定后件是与肯定前件对应的定理或推理规则。
  • 蕴涵消去： [math]\displaystyle{ P, P \rightarrow Q \vdash Q }[/math] 。
• 在 Hilbert 系统中，否定后件是重要定理。
• 否定后件也是部分反证法和逆否证法的核心逻辑，是证伪一个命题的主要手段。

非经典逻辑中的情况

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