形式邏輯/命題邏輯/推論規則

← 定理

↑ 命題邏輯

推導中的析取式 →

推論規則

本頁介紹了推論規則的概念，並提供了一些此類規則。

推導推論規則

基礎

現在我們可以更進一步簡化縮寫。推論規則是推論系統中未給出的推論規則，但構成使用先前證明的定理的簡寫。特別是，假設我們已經證明了一個特定的定理。在這個定理中，用不同的希臘字母統一替換每個句子字母。假設結果具有以下形式。

$\varphi _{1}\land \varphi _{2}\land \ ...\,\land \ \varphi _{n}\rightarrow \psi \,\!$.

[評論：這以及下面的內容在我看來可能讓學生感到困惑。之前章節中避免元理論的意圖在這裡造成了一個問題，因為需要了解演繹定理才能使這個內容更有意義。]

然後我們可以引入一個推導推論規則，其形式為

$\varphi _{1}\,\!$

$\varphi _{2}\,\!$

$\ \vdots$

${\underline {\varphi _{n}}}\,\!$

$\psi \,\!$

應用推導規則可以透過用以下方式替換它來消除：

1. 先前證明的定理，
2. 重複應用合取式引入（KI）來構建定理的前件，以及
3. 應用條件式消去（CE）來獲得定理的後件。

先前證明的定理然後可以如上所述消除。這將使你得到一個未縮寫的推導。

當然，從推導中刪除縮寫並不理想，因為它使推導更加複雜，更難閱讀，但推導可以被取消縮寫的這一事實證明了使用縮寫的合理性，因此我們可以首先使用縮寫。

重複

我們的第一個推導推論規則將基於T1，它是

$\mathrm {P} \rightarrow \mathrm {P} \,\!$

用希臘字母替換句子字母，我們得到

$\varphi \rightarrow \varphi \,\!$

我們現在生成推導推論規則

重複 (R)

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

$\varphi \,\!$

現在我們可以展示這個規則如何簡化我們對T2的證明。

1.     $\mathrm {Q} \,\!$   假設    $[\mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!$     2.       $\mathrm {P} \,\!$   假設    $[\mathrm {P} \rightarrow \mathrm {Q} ]\,\!$ 3.       $\mathrm {Q} \,\!$   1 R     4.     $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   2–3 CI   5.   $\mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )\,\!$   1–4 CI

雖然這比我們最初證明T2只短了一行，但它不那麼令人討厭。我們可以使用一個推理規則，而不是一個愚蠢的技巧。因此，推導更容易閱讀和理解（更不用說更容易生成）。

雙重否定規則

接下來的兩個定理——以及基於它們的推導規則——利用了雙重否定公式與未否定公式之間的等價性。

雙重否定引入

$\mathbf {T3.} \quad \mathrm {P} \rightarrow \lnot \lnot \mathrm {P} \,\!$

1.     $\mathrm {P} \,\!$   假設    $[\mathrm {P} \rightarrow \lnot \lnot \mathrm {P} ]\,\!$     2.       $\lnot \mathrm {P} \,\!$   假設    $[\lnot \lnot \mathrm {P} ]\,\!$ 3.       $\mathrm {P} \,\!$   1 R     4.     $\lnot \lnot \mathrm {P} \,\!$   2–3 NI   5.   $\mathrm {P} \rightarrow \lnot \lnot \mathrm {P} \,\!$   1–4 CI

T3 證明了以下規則。

雙重否定引入 (DNI)

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

$\lnot \lnot \varphi \,\!$

雙重否定消除

$\mathbf {T4.} \quad \lnot \lnot \mathrm {P} \rightarrow \mathrm {P} \,\!$

1.     $\lnot \lnot \mathrm {P} \,\!$   假設    $[\lnot \lnot \mathrm {P} \rightarrow \mathrm {P} ]\,\!$     2.       $\lnot \mathrm {P} \,\!$   假設    $[\mathrm {P} ]\,\!$ 3.       $\lnot \lnot \mathrm {P} \,\!$   1 R     4.     $\mathrm {P} \,\!$   2–3 NE   5.   $\lnot \lnot \mathrm {P} \rightarrow \mathrm {P} \,\!$   1–4 CI

T4 證明了以下規則。

雙重否定消除（DNE）

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

$\varphi \,\!$

其他推導規則

矛盾

$\mathbf {T5.} \quad \mathrm {P} \land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$

1.     $\mathrm {P} \land \lnot \mathrm {P} \,\!$   假設    $[\mathrm {P} \land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!$     2.       $\lnot \mathrm {Q} \,\!$   假設    $[\mathrm {Q} ]\,\!$ 3.       $\mathrm {P} \,\!$   1 S 4.       $\lnot \mathrm {P} \,\!$   1 S     5.     $\mathrm {Q} \,\!$   2–4 NE   7.   $\mathrm {P} \land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!$   1–5 CI

我們的下一條規則基於T5。

矛盾（矛盾）

$\varphi \,\!$

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

$\psi \,\!$

當推匯出矛盾但想要的放縮規則不是 NI 或 NE 時，此規則偶爾有用。這樣可以避免完全瑣碎的子推導。矛盾規則將在下一個定理的證明中使用。

條件加法

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

1.     $\lnot \mathrm {P} \,\!$   假設    $[\lnot \mathrm {P} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!$     2.       $\mathrm {P} \,\!$   假設    $[\mathrm {P} \rightarrow \mathrm {Q} ]\,\!$ 3.       $\mathrm {Q} \,\!$   1, 2 矛盾     4.     $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   2–3 CI   5.   $\lnot \mathrm {P} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )\,\!$   1–4 CI

根據 **T2** 和 **T6**，我們引入以下推導規則。

條件加法，形式 I (CAdd)

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

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

條件加法，形式 II (CAdd)

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

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

“條件加法”這個名字並不常用。它是基於析取引入的傳統名稱“加法”。此規則不提供引入條件的通用方法。這是因為您需要的先行式行並不總是可推導的。然而，當先行式行恰好很容易獲得時，應用此規則比為條件引入產生子推導更簡單。

拒取式

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

1.     $(\mathrm {P} \rightarrow \mathrm {Q} )\land \lnot \mathrm {Q} \,\!$   假設    $[(\mathrm {P} \rightarrow \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \lnot \mathrm {P} ]\,\!$     2.       $\mathrm {P} \,\!$   假設    $[\lnot \mathrm {P} ]\,\!$ 3.       $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   1 KE 4.       $\mathrm {Q} \,\!$   2, 3 CE 5.       $\lnot \mathrm {Q} \,\!$   1 KE     6.     $\lnot \mathrm {P} \,\!$   2–5 NI   7.   $(\mathrm {P} \rightarrow \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \lnot \mathrm {P} \,\!$   1–6 CI

現在我們使用 **T7** 來證明以下規則。

否定後件式 (MT)

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

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

$\lnot \varphi \,\!$

否定後件式有時也被稱為“否定結論”。需要注意的是，以下推論**不是**否定後件式的例子，至少根據上面的定義。

$\lnot \mathrm {P} \rightarrow \lnot \mathrm {Q} \,\!$

${\underline {\mathrm {Q} \quad \quad \quad \quad }}\,\!$

$\mathrm {P} \,\!$

否定後件式的前提是條件語句及其結論的否定。這個推論的前提是條件語句及其結論的**反面**，而不是**否定**。這裡我們想要推出的結論需要透過以下方式得出。

1.   $\lnot \mathrm {P} \rightarrow \lnot \mathrm {Q} \,\!$   前提 2.   $\mathrm {Q} \,\!$   前提 3.   $\lnot \lnot \mathrm {Q} \,\!$   2 DNI 4.   $\lnot \lnot \mathrm {P} \,\!$   1, 3 CE 5.   $\mathrm {P} \,\!$   4 DNE

當然，我們可以證明以下定理

$(\lnot \mathrm {P} \rightarrow \lnot \mathrm {Q} )\land \mathrm {Q} \rightarrow \mathrm {P} \ .\,\!$

然後你可以根據這個定理新增一個新的推理規則，或者更可能的是，新增一個新的否定後件式形式。但是，我們這裡不做這個操作。

附加定理

目前給出的匯出規則對於消除推導過程中經常出現的繁瑣步驟非常有用。它們將有助於使你的推導更容易生成，也更容易閱讀。然而，由於它們確實是匯出規則，因此它們不是嚴格必要的，在理論上是可以省略的。

可以有效地新增許多其他定理和匯出規則。我們在這裡列出一些有用的定理，但將其證明以及與之相關的匯出推理規則的定義留給讀者。如果你構建了許多推導，你可能想要維護你自己的個人清單，其中包含你認為有用的規則。

包含雙條件語句的定理

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

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

$\mathbf {T10.} \quad \mathrm {P} \land \mathrm {Q} \rightarrow (\mathrm {P} \leftrightarrow \mathrm {Q} )\,\!$

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

包含否定符號的定理

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

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

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

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