我們的推導包含兩種型別的元素。
- 行號。 這使得在之後可以引用該行。
- 公式。 推導的目的是推匯出公式，而這是在該行推匯出的公式。
- 註釋。 這指定了將公式新增到推導中的理由。
- 行號和公式之間的垂直線。這些用於劃分子推導，我們將在下一個模組中介紹。
- 分隔前提和臨時假設與其他行的水平線。當我們進入謂詞邏輯時，對使用前提和臨時假設有限制。以易於識別的形式將它們劃分開有助於遵守這些限制。
我們通常非正式地談論公式，就好像它是整行一樣，但該行還包括行號和註釋。
前提的註釋為“前提”。我們要求推導中使用的所有前提都出現在第一行。不允許任何非前提行出現在前提之前。理論上，一個論證可以有無限多個前提。然而，推導只有有限多個行，因此推導中只能使用有限多個前提。我們不要求所有前提都出現在其他行之前。對於具有無限多個前提的論證，這是不可能的。但我們確實要求推導中使用的所有前提都出現在任何其他行之前。
要求在推導中使用的前提出現在其第一行，比絕對必要的要求更嚴格。但是，當我們進入謂詞邏輯時，某些需要的限制使得該要求至少成為一個有用的約定。
我們在上一個模組中介紹了除兩個之外的所有推理規則，並將在下個模組中介紹另外兩個規則。
這個推導系統沒有任何公理。
我們將為以下論證構建一個推導
∴ 
首先，我們將前提輸入推導
| |
| 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 |
|
