形式逻辑/命题逻辑/推论规则

← 定理

↑ 命题逻辑

推导中的析取式 →

推论规则

本页介绍了推论规则的概念，并提供了一些此类规则。

推导推论规则

基础

现在我们可以更进一步简化缩写。推论规则是推论系统中未给出的推论规则，但构成使用先前证明的定理的简写。特别是，假设我们已经证明了一个特定的定理。在这个定理中，用不同的希腊字母统一替换每个句子字母。假设结果具有以下形式。

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