我们的推导包含两种类型的元素。
- 行号。 这使得在之后可以引用该行。
- 公式。 推导的目的是推导出公式，而这是在该行推导出的公式。
- 注释。 这指定了将公式添加到推导中的理由。
- 行号和公式之间的垂直线。这些用于划分子推导，我们将在下一个模块中介绍。
- 分隔前提和临时假设与其他行的水平线。当我们进入谓词逻辑时，对使用前提和临时假设有限制。以易于识别的形式将它们划分开有助于遵守这些限制。
我们通常非正式地谈论公式，就好像它是整行一样，但该行还包括行号和注释。
前提的注释为“前提”。我们要求推导中使用的所有前提都出现在第一行。不允许任何非前提行出现在前提之前。理论上，一个论证可以有无限多个前提。然而，推导只有有限多个行，因此推导中只能使用有限多个前提。我们不要求所有前提都出现在其他行之前。对于具有无限多个前提的论证，这是不可能的。但我们确实要求推导中使用的所有前提都出现在任何其他行之前。
要求在推导中使用的前提出现在其第一行，比绝对必要的要求更严格。但是，当我们进入谓词逻辑时，某些需要的限制使得该要求至少成为一个有用的约定。
我们在上一个模块中介绍了除两个之外的所有推理规则，并将在下个模块中介绍另外两个规则。
这个推导系统没有任何公理。
我们将为以下论证构建一个推导
∴ 
首先，我们将前提输入推导
| |
| 1.
|
|
|
|
前提 |
| 2.
|
|
|
|
前提 |
| 3.
|
|
|
|
前提 |
|
请注意行号和公式之间的垂直线。 这是控制子推导的围栏的一部分。 我们将在下一模块中学习子推导。 在此之前，我们只需在推导的整个长度上放置一条垂直线。 还要注意前提下的水平线。 这是帮助区分前提与推导中其他行的围栏。
现在我们需要使用前提。 对第一个前提应用 KE 两次，我们添加以下行
| |
| 4.
|
|
|
|
1 KE |
| 5.
|
|
|
|
1 KE |
|
现在我们需要通过应用 CE 使用第二个前提。 由于 CE 有两条前件行，所以我们需要先推导出另一条需要使用的行。 因此，我们添加这些行
| |
| 6.
|
|
|
|
4 DI |
| 7.
|
|
|
|
2, 6 CE |
|
现在我们将通过应用 CE 使用第三个前提。 同样，我们需要先推导出另一条需要使用的行。 新行是
| |
| 8.
|
|
|
|
5, 7 KI |
| 9.
|
|
|
|
3, 8 CE |
|
第 9 行是 ，是我们论证的结论，所以我们完成了。 结论并不总是那么容易得到，但这里却得到了。 完整的推导如下
| |
| 1.
|
|
|
|
前提 |
| 2.
|
|
|
|
前提 |
| 3.
|
|
|
|
前提 |
| 4.
|
|
|
|
1 KE |
| 5.
|
|
|
|
1 KE |
| 6.
|
|
|
|
4 DI |
| 7.
|
|
|
|
2, 6 CE |
| 8.
|
|
|
|
5, 7 KI |
| 9.
|
|
|
|
3, 8 CE |
|
