形式逻辑/命题逻辑/子推导和放缩规则

← 构造一个简单推导

↑ 命题逻辑

构造一个复杂推导 →

子推导和放缩规则

如前所述，我们需要三个额外的推理规则：条件引入 (CI)、否定引入 (NI) 和否定消去 (NE)。这些规则需要子推导。

推导条件语句

示例推导

我们从一个示例推导开始，它说明了条件引入，然后进行解释。一个推导出以下论证的推导：

$\mathrm {Q} \land \mathrm {R} \!$   ∴   $\mathrm {P} \rightarrow \mathrm {Q}$

如下所示

1.   $\mathrm {Q} \land \mathrm {R} \,\!$   前提   2.     $\mathrm {P} \,\!$   假设 3.     $\mathrm {Q} \,\!$   1 KE   4.   $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   2–3 CI

第 2 行和第 3 行构成了一个子推导。它从假设所需公式的前件开始，以推导出所需公式的后件结束。在行号和公式之间有两个垂直分隔符，将它与推导的其余部分隔开，并指示它的从属地位。第 2 行下面有一个水平分隔符，将假设与子推导的其余部分隔开。第 4 行是条件引入的应用。它不是来自一两行，而是来自整个子推导（第 2 行到第 3 行）整体。

条件引入是一个放缩规则。它放缩（使无效）该假设，实际上使整个子推导无效。一旦应用放缩规则，子推导中的任何行（这里，第 2 行和第 3 行）都不能在推导中进一步使用。

条件引入规则

要推导出公式 $(\varphi \rightarrow \psi )\,\!$，条件引入 (CI) 规则通过首先在子推导中假设前件 $\varphi$ 为真，然后推导出 $\psi$ 作为子推导的结论而应用。符号上，CI 写作

${\underline {{\text{Assume }}\varphi {\text{, derive }}\psi }}$

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

这里，后续行不是从一个或多个前件行推断出来的，而是从整个子推导中推断出来的。注释是子推导所占行的范围和缩写 CI。与之前介绍的推理规则不同，条件引入不能通过真值表来证明。而是由在命题联结词性质中介绍的演绎原理来证明。我们假设$\varphi$以推导出$(\varphi \rightarrow \psi )\,\!$背后的直觉是，如果$\varphi$为假，则根据定义$(\varphi \rightarrow \psi )\,\!$为真。因此，如果我们证明了每当$\varphi$碰巧为真时，$\psi$为真，那么$(\varphi \rightarrow \psi )\,\!$必须为真。

请注意，前件子推导可以包含一个单行，该行既作为假设的$\varphi \,\!$，也作为推导出的$\psi \,\!$，如下面的推导所示

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

1.     $\mathrm {P} \,\!$   假设   2.   $\mathrm {P} \rightarrow \mathrm {P} \,\!$   1 CI

否定

示例推导

为了说明否定引入，我们将提供一个关于以下论证的推导

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

1.   $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {R} \,\!$   前提 2.   $\mathrm {P} \land \lnot \mathrm {Q} \,\!$   前提   3.     $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   假设 4.     $\mathrm {P} \,\!$   2 KE 5.     $\mathrm {Q} \,\!$   3, 4 CE 6.     $\lnot \mathrm {Q} \,\!$   2 KE   7.   $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\,\!$   3–6 NI 8.   $\mathrm {R} \,\!$   1, 7 CE 9.   $\mathrm {Q} \lor \mathrm {R} \,\!$   8 DI

第 3 行到第 6 行构成一个子推导。它首先假设所需公式的相反，最后假设一个矛盾（一个公式及其否定）。和以前一样，行号和公式之间有两个垂直的栅栏，将它与推导的其余部分隔开，并表明它的从属状态。第 3 行下的水平栅栏再次将假设与子推导的其余部分隔开。第 7 行是从整个子推导得出的，是否定引入的应用。

在第 9 行，请注意注释“5 DI”是不正确的。虽然根据 DI 从 $\mathrm {Q} \,\!$ 推断出 $\mathrm {Q} \lor \mathrm {R} \,\!$ 是有效的，当我们到达第 9 行时，第 5 行不再处于活动状态。因此，我们不允许在那个时候从第 5 行推导出任何东西。

否定引入规则

否定引入 (NI)

${\underline {{\text{Assume }}\varphi {\text{, derive }}\psi {\text{ and }}\lnot \psi }}$

$\lnot \varphi \,\!$

推论结果行是从整个子推导推断出的。注释是子推导所占行的范围，缩写是 NI。否定引入有时用拉丁语名称Reductio ad Absurdum，有时用反证法。

与条件引入一样，否定引入不能用真值表来证明。相反，它是通过在 命题连接词的性质 中介绍的归谬原理来证明的。

另一个示例推导

为了说明否定消去，我们将为以下论证提供一个推导

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

1.   $\lnot (\lnot \mathrm {P} \lor \lnot \mathrm {Q} )\land \mathrm {R} \,\!$   前提   2.     $\lnot \mathrm {P} \,\!$   假设 3.     $\lnot \mathrm {P} \lor \lnot \mathrm {Q} \,\!$   2 DI 4.     $\lnot (\lnot \mathrm {P} \lor \lnot \mathrm {Q} )\,\!$   1 KE   5.   $\mathrm {P} \,\!$   2–4 NE

第 2 行到第 4 行构成一个子推导。正如前面例子中一样，它从假设所需公式的反面开始，并以假设矛盾（公式及其否定）结束。第 5 行紧随整个子推导，是否定消除的应用。

否定消除规则

否定消除 (NE)

${\underline {{\text{Assume }}\lnot \varphi {\text{, derive }}\psi {\text{ and }}\lnot \psi }}$

$\varphi \,\!$

后面的行从整个子推导中推断出来。注释是子推导所占行的范围，缩写是 NE。像否定引入一样，否定消除有时被称为拉丁名字 Reductio ad Absurdum，有时被称为 反证法。

像否定引入一样，否定消除是根据在 命题连接词的性质 中介绍的归谬原则来证明的。这个规则在引入/消除命名约定中的位置有点尴尬，不像其他消除规则，这个规则消除的否定并没有出现在已经推导出的行中。而是消除的否定出现在子推导的假设中。

术语

在本模块中介绍的推理规则，条件引入和否定引入，都是放缩规则。为了避免使用更好的术语，我们可以将 推理规则 中介绍的推理规则称为“标准规则”。标准规则 是推理规则，其前件是一组行。放缩规则 是推理规则，其前件是一个子推导。

推导中一行深度 是该行号与公式之间隔开的篱笆数量。推导的所有行都至少有 1 的深度。每个临时假设都会将深度增加 1。每个放缩规则都会将深度减少 1。

活动行 是一行，可作为标准推理规则的前件行使用。特别是，它是一行，其深度小于或等于当前行的深度。非活动行是不活动的行。

放缩规则被称为放缩 假设。它使前件子推导中的所有行都变为非活动行。