形式逻辑/命题逻辑/推导中的析取

← 推导出的推理规则

↑ 命题逻辑

命题逻辑结束 →

推导中的析取

从当前的推理规则来看，推导中的析取很难处理。使用已推出的析取并应用析取消去规则（DE）并不太糟糕，但有一个更易于使用的替代方法。首先推导出析取更困难。我们的析取引入规则（DI）对于此任务来说是一个相当无力的工具。在本模块中，我们介绍了推导规则，这些规则为处理推导中的析取提供了替代方法。

使用已推出的析取

拒取式假言推理

我们从一个新的（即将推出的）推理规则开始。这将为析取消去规则（DE）提供一个有用的替代方案。

拒取式假言推理，形式 I (MTP)

$(\varphi \lor \psi )\,\!$

${\underline {\lnot \varphi \quad \quad }}\,\!$

$\psi \,\!$

拒取式假言推理，形式 II (MTP)

$(\varphi \lor \psi )\,\!$

${\underline {\lnot \psi \quad \quad }}\,\!$

$\varphi \,\!$

拒取式假言推理有时被称为析取三段论，偶尔也被称为“狗的规则”。

支持定理

这个新规则需要以下两个支持定理。

$\mathbf {T16.} \quad (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$

1.     $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \,\!$   假设    $[(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!$ 2.     $\mathrm {P} \lor \mathrm {Q} \,\!$   1 KE 3.     $\lnot \mathrm {P} \,\!$   1 KE 4.     $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   3 CAdd 5.     $\mathrm {Q} \rightarrow \mathrm {Q} \,\!$   T1 [P/Q] 6.     $\mathrm {Q} \,\!$   2, 4, 5 DE   7.   $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$   1–6 CI

$\mathbf {T17.} \quad (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} \,\!$

1.     $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \,\!$   假设    $[(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} ]\,\!$ 2.     $\mathrm {P} \lor \mathrm {Q} \,\!$   1 KE 3.     $\lnot \mathrm {Q} \,\!$   1 KE 4.     $\mathrm {Q} \rightarrow \mathrm {P} \,\!$   3 CAdd 5.     $\mathrm {P} \rightarrow \mathrm {P} \,\!$   T1 6.     $\mathrm {P} \,\!$   2, 4, 5 DE   7.   $(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} \,\!$   1–6 CI

示例推导

为了使用 MTP 的示例，我们将重新进行构建复杂推导中的示例推导。

$\mathrm {P} \land \mathrm {R} \rightarrow \mathrm {T} ,\ \ \mathrm {S} \land \lnot \mathrm {T} ,\ \ \mathrm {S} \rightarrow \lnot \mathrm {Q} \,\!$   ∴   $\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} \,\!$

1.   $\mathrm {P} \land \mathrm {R} \rightarrow \mathrm {T} \,\!$   前提 2.   $\mathrm {S} \land \lnot \mathrm {T} \,\!$   前提 3.   $\mathrm {S} \rightarrow \lnot \mathrm {Q} \,\!$   前提   4.     $\mathrm {P} \lor \mathrm {Q} \,\!$   假设    $[\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!$     5.       $\mathrm {R} \,\!$   假设    $[\lnot \mathrm {R} ]\,\!$ 6.       $\mathrm {S} \,\!$   2 KE 7.       $\lnot \mathrm {Q} \,\!$   3, 6 CE 8.       $\mathrm {P} \,\!$   4, 7 MTP 9.       $\mathrm {P} \land \mathrm {R} \,\!$   5, 8 KI 10.       $\mathrm {T} \,\!$   1, 9 CE 11.       $\lnot \mathrm {T} \,\!$   2 KE     12.     $\lnot \mathrm {R} \,\!$   5–11 NI   13.   $\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} \,\!$   4–12 CI

在第 4 行之后，我们没有费心去推导出 DE 所需的前提行，而是直接进行结论的后件的子推导。在第 8 行，我们应用了 MTP。

推导析取

条件析取

下一个推导规则显著减少了推导析取的步骤，因此为析取引入 (DI) 提供了一个有用的替代方案。

条件析取 (CDJ)

${\underline {(\lnot \varphi \rightarrow \psi )}}\,\!$

$(\varphi \lor \psi )\,\!$

支持定理

$\mathbf {T18.} \quad (\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} \,\!$

1.     $\lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$   假设    $[(\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} ]\,\!$     2.       $\lnot (\mathrm {P} \lor \mathrm {Q} )\,\!$   假设    $[\mathrm {P} \lor \mathrm {Q} ]\,\!$       3.         $\mathrm {P} \,\!$   假设    $[\lnot \mathrm {P} ]\,\!$         4.         $\mathrm {P} \lor \mathrm {Q} \,\!$   3 DI 5.         $\lnot (\mathrm {P} \lor \mathrm {Q} )\,\!$   2 R       6.       $\lnot \mathrm {P} \,\!$   3–5 NI 7.       $\mathrm {Q} \,\!$   1, 6 CE 8.       $\mathrm {P} \lor \mathrm {Q} \,\!$   7 DI     9.     $\mathrm {P} \lor \mathrm {Q} \,\!$   2–8 NI   10.   $(\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} \,\!$   1–9 CI

示例推导

这个推导将使用 **T12**（在 推导推理规则 中引入），即使它的证明留给读者作为练习。以下推导的正确性，尤其是第 2 行，假设您已经证明了 **T12**。

∴   $(\mathrm {P} \rightarrow \mathrm {Q} )\lor (\mathrm {Q} \rightarrow \mathrm {R} )\,\!$

1.     $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\,\!$   假设    $[\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )]\,\!$ 2.     $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \land \lnot \mathrm {Q} \,\!$   T12 3.     $\mathrm {P} \land \lnot \mathrm {Q} \,\!$   1, 2 CE 4.     $\lnot \mathrm {Q} \,\!$   3 KE 5.     $\mathrm {Q} \rightarrow \mathrm {R} \,\!$   4 CAdd   7.   $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )\,\!$   1–6 CI 8.   $(\mathrm {P} \rightarrow \mathrm {Q} )\lor (\mathrm {Q} \rightarrow \mathrm {R} )\,\!$   7 CDJ

这里我们试图通过首先推导出 CDJ 所需的前件行来推导出所需的条件。