← 推导
↑ 命题逻辑
构建简单推导 →
推理规则[编辑 | 编辑源代码]
概述[编辑 | 编辑源代码]
推理规则将以以下示例中的格式显示。
条件消除 (CE) ( φ → ψ ) {\displaystyle (\varphi \rightarrow \psi )\,\!}
φ _ {\displaystyle {\underline {\varphi \quad \quad \quad }}\,\!}
ψ {\displaystyle \psi \,\!}
此推理规则称为“条件消除”，缩写为“CE”。如果上面一行中具有上述形式的公式出现在推导中的活动行中，则可以应用此规则。这些被称为此推理的前件行。应用此规则将添加具有下面一行中形式的公式。这被称为此推理的后件行。新推导行的注释是前件行的行号和缩写“CE”。
注意：您可能会看到前提行和结论行代替前件行和后件行。您也可能会看到其他术语，因为大多数教科书都会避免在这里给出任何特殊的术语。
每个命题连接词将有两个推理规则，每个规则都属于以下类型。
引入规则。给定连接词的引入规则允许我们推导出一个以给定连接词为其主要连接词的公式。
消除规则。给定连接词的消除规则允许我们使用一个公式，该公式已出现在推导中，并以给定连接词为其主要连接词。
三个规则（否定引入、否定消除和条件引入）将在下一页中介绍。这些是所谓的放电规则，将在我们介绍子推导时解释。
三个规则（合取消除、析取引入和双条件消除）将各有两种形式。我们多少有些随意地将这两种模式视为同一规则的不同形式，而不是单独的规则。
可以使用真值表来证明此页上的推理的有效性。
推理规则[编辑 | 编辑源代码]
否定[编辑 | 编辑源代码]
否定引入 (NI)
将在下一页介绍。
否定消除 (NE)
将在下一页介绍。
合取[编辑 | 编辑源代码]
合取引入 (KI)
φ {\displaystyle \varphi \,\!}
ψ _ {\displaystyle {\underline {\psi \quad \quad \ \ }}\,\!}
( φ ∧ ψ ) {\displaystyle (\varphi \land \psi )\,\!}
合取引入传统上被称为并置或合取。
合取消除，形式 I (KE)
( φ ∧ ψ ) _ {\displaystyle {\underline {(\varphi \land \psi )}}\,\!}
φ {\displaystyle \varphi \,\!}
合取消除，形式 II (KE)
( φ ∧ ψ ) _ {\displaystyle {\underline {(\varphi \land \psi )}}\,\!}
ψ {\displaystyle \psi \,\!}
合取消除传统上被称为化简。
析取[编辑 | 编辑源代码]
析取引入，形式 I (DI)
φ _ {\displaystyle {\underline {\varphi \quad \quad \ \ }}\,\!}
( φ ∨ ψ ) {\displaystyle (\varphi \lor \psi )\,\!}
析取引入，形式 II (DI)
ψ _ {\displaystyle {\underline {\psi \quad \quad \ \ }}\,\!}
( φ ∨ ψ ) {\displaystyle (\varphi \lor \psi )\,\!}
析取引入传统上被称为加法。
析取消去 (DE)
φ ∨ ψ {\displaystyle \varphi \lor \psi \,\!}
( φ → χ ) {\displaystyle (\varphi \rightarrow \chi )\,\!}
( ψ → χ ) _ {\displaystyle {\underline {(\psi \rightarrow \chi )}}\,\!}
χ {\displaystyle \chi \,\!}
析取消去传统上被称为情况分离。
条件[编辑 | 编辑源代码]
条件引入 (CI)
将在下一页介绍。
条件消除 (CE)
( φ → ψ ) {\displaystyle (\varphi \rightarrow \psi )\,\!}
φ _ {\displaystyle {\underline {\varphi \quad \quad \quad }}\,\!}
ψ {\displaystyle \psi \,\!}
条件消去传统上被称为拉丁文肯定前件，或更不常见的是肯定前项。
双条件[编辑 | 编辑源代码]
双条件引入 (BI)
( φ → ψ ) {\displaystyle (\varphi \rightarrow \psi )\,\!}
( ψ → φ ) _ {\displaystyle {\underline {(\psi \rightarrow \varphi )}}\,\!}
( φ ↔ ψ ) {\displaystyle (\varphi \leftrightarrow \psi )\,\!}
双条件消去，形式 I (BE)
( φ ↔ ψ ) {\displaystyle (\varphi \leftrightarrow \psi )\,\!}
φ _ {\displaystyle {\underline {\varphi \quad \quad \quad }}\,\!}
ψ {\displaystyle \psi \,\!}
双条件消去，形式 II (BE)
( φ ↔ ψ ) {\displaystyle (\varphi \leftrightarrow \psi )\,\!}
ψ _ {\displaystyle {\underline {\psi \quad \quad \quad }}\,\!}
φ {\displaystyle \varphi \,\!}
示例[编辑 | 编辑源代码]
推理规则很容易应用。从以下几行
(1) P ∧ Q → ( S ↔ T ) {\displaystyle \mathrm {P} \land \mathrm {Q} \rightarrow (\mathrm {S} \leftrightarrow \mathrm {T} )\,\!}
以及
(2) P ∧ Q {\displaystyle \mathrm {P} \land \mathrm {Q} \,\!}
我们可以应用条件消去来添加
(3) S ↔ T {\displaystyle \mathrm {S} \leftrightarrow \mathrm {T} \,\!}
到推导中。
注释将是 (1) 和 (2) 的行号以及条件消去的缩写，即 '1, 2, CE'。前提行的顺序无关紧要；无论 (1) 出现在 (2) 之前还是之后，推理都是允许的。
必须记住，推理规则是严格的句法。语义上明显的变体是不允许的。例如，不允许从 (1) 和以下推导出 (3)
(4) Q ∧ P {\displaystyle \mathrm {Q} \land \mathrm {P} \,\!}
但是，你可以从 (1) 和 (4) 推导出 (3)，方法是先推导出
(5) Q {\displaystyle \mathrm {Q} \,\!}
以及
(6) P {\displaystyle \mathrm {P} \,\!}
根据连接词消去（KE）规则，我们可以得到 (6)。然后，我们可以通过连接词引入 (KI) 规则得到 (2)，最后通过条件消去 (CE) 规则，从 (1) 和 (2) 推导出 (3)。一些推导系统中有一个规则，通常被称为重言式蕴涵，允许你从之前的行中推导出任何重言式结论。然而，这应该被视为一个（公认有用的）缩写。在后面的页面中，我们将实现这个缩写的受限版本。
一般来说，通过应用消去规则来分解前提、其他假设（将在后面的页面中介绍）——然后继续分解结果，这是很有用的。假设这就是我们对 (1) 和 (2) 应用 CE 的原因，那么推导出以下结论可能会有用：
(7) S → T {\displaystyle \mathrm {S} \rightarrow \mathrm {T} \,\!}
以及
(8) T → S {\displaystyle \mathrm {T} \rightarrow \mathrm {S} \,\!}
通过对 (3) 应用双条件消去 (BE) 规则。为了进一步分解，你可以尝试推导出 S {\displaystyle \mathrm {S} \,\!} 或者 T {\displaystyle \mathrm {T} \,\!} ，这样你就可以对 (7) 或 (8) 应用 CE。
如果你知道要推导哪一行，你可以通过应用引入规则来构建它。这就是从 (5) 和 (6) 推导出 (2) 的策略。