← 推匯出的推理規則

↑ 命題邏輯

命題邏輯結束 →

推導中的析取

從當前的推理規則來看，推導中的析取很難處理。使用已推出的析取並應用析取消去規則（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} ]\,\!$

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} ]\,\!$

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 所需的前件行來推匯出所需的條件。