形式逻辑/命题逻辑/推导
| ← 翻译 | ↑ 命题逻辑 | 推理规则 → |
在 有效性 中，我们引入了公式和论证的有效性概念。在命题逻辑中，有效公式是重言式。到目前为止，我们可以用以下方法证明公式 是有效的（重言式）。
- 为 制作真值表。
- 获得 作为已知有效的公式的代入实例。
- 通过将等价替换应用于已知有效的公式，获得 。
然而，这些方法在谓词逻辑中失效，因为谓词没有真值表。如果没有替代方法，我们就无法使用第二种和第三种方法，因为它们依赖于对其他公式有效性的了解。另一种证明公式有效的方法——不使用真值表——是使用推导。本页和后续页面介绍了这种技术。请注意，推导证明论证有效的断言假设了一个健全的推导系统，参见下面的健全性。
推导是一系列编号行，每行都包含一个公式和一个注释。注释提供了将该行添加到推导的理由。推导是数学证明的高度形式化的类比——或者说是数学证明的模型。
一个典型的推导系统将允许以下几种类型的行
- 一行可以是公理。推导系统可以指定一组公式作为公理。这些公理在任何推导中都被认为是正确的。对于命题逻辑，公理集是重言式的固定子集。
- 一行可以是假设。推导可以有几种类型的假设。以下列出了标准情况。
- 前提。当试图证明一个论证的有效性时，可以假设该论证的前提。
- 用于子推导的临时假设。此类假设旨在仅在推导的一部分中有效，并且必须在推导完成之前被解除（使其失效）。子推导将在后面的页面中介绍。
- 一行可以是将推理规则应用于前几行得出的结果。推理是指对前几行进行的句法转换以生成新行。推理必须遵循推导系统定义的固定模式集之一。这些模式是系统的推理规则。其思想是，任何符合推理规则的推理都应该是有效的论证。
我们在 形式语义学 中注意到，像 这样的形式语言可以通过几种替代甚至相互竞争的语义规则集来解释。对于给定的语法语义对，还可以定义多种推导系统。由形式语法、形式语义和推导系统组成的三元组是一个逻辑系统。
推导旨在证明论证是有效的。零前提论证的推导旨在证明其结论是一个有效公式——在命题逻辑中，这意味着证明它是重言式。给定一个逻辑系统，如果推导系统实现了这些目标，则称该系统是健全的。也就是说，一个推导系统是健全的（具有健全性的属性），如果它的推导系统中可推导的每个公式（和论证）都是有效的（给定一个语法和一个语义）。
推导系统的另一个理想品质是完备性。给定一个逻辑系统，如果它的推导系统可以推导出每个有效公式，则称该系统是完备的。然而，对于某些逻辑，没有推导系统是或可以是完备的。
健全性和完备性是重要的结果。它们的证明在这里不作介绍，但在许多标准的元逻辑教科书中都有介绍。
符号有时被称为推导符号，特别是语义推导符号。我们之前介绍了该符号的以下三种用法。
| (1) | 满足 。 | ||||
| (2) | 是有效的。 | ||||
| (3) | 蕴含（具有逻辑结果）。 |
其中 是一个赋值，而 是一个前提集合，如 有效性 中所介绍。
推论具有与语义真值符对应的东西，即句法真值符。上面第（1）项没有句法对应项。但是，上面第（2）和（3）项有以下对应项。
| (4) | 是可证的。 | ||||
| (5) | 证明（具有推导结果）。 |
如果且仅当存在 从无前提中推导出的正确推导，则第（4）项为真。类似地，如果且仅当存在 的正确推导，该推导将 的成员作为前提，则第（5）项为真。
上面第（4）和（5）项的否定是
| (6) | |||
| (7) |
现在我们可以定义健全性和完备性如下
- 给定一个逻辑系统，如果且仅当
- 给定一个逻辑系统，其推导系统是完备的当且仅当
