一個定理是一個公式，它已經提供了零前提推導。我們將保留一個已證明定理的編號列表。在接下來的推導中，我們將繼續使用我們的非正式約定，在假設的註釋中新增一個公式，特別是我們希望透過新開始的子推導推匯出的公式。
您可能記得，在 構建複雜推導 中，我們不得不使用一個愚蠢的技巧來將一個公式複製到正確的子推導中（第 16 行和第 17 行）。我們可以證明一個定理，它將幫助我們避免這種令人不愉快的事情。
| |
| 1.
|
|
|
|
|
假設 ![{\displaystyle [\mathrm {P} \rightarrow \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/79933dc3c8b22ad47c5f28386ff6e8976b768d5e) |
|
|
|
|
|
|
| 2.
|
|
|
|
1 CI |
|
推導可以透過允許輸入一個公式作為先前已證明定理的替換例項來簡化。註釋將是 'Tn'，其中 n 是定理的編號。雖然我們不會正式要求，但我們也會在註釋中顯示替換，如果有的話（見下面的推導中的第 3 行）。下一個定理的證明將使用 T1。
| |
| 1.
|
|
|
|
|
假設 ![{\displaystyle [\mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b8be83a1ab88d731a8b904852f116034ad2939) |
|
|
|
|
|
|
|
| 2.
|
|
|
|
|
|
假設 ![{\displaystyle [\mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97cf4af3c1bca8188faa85c99bb829c88690a523) |
| 3.
|
|
|
|
|
|
T1 [P/Q] |
| 4.
|
|
|
|
|
|
1, 3 CE |
|
|
|
|
|
|
|
| 5.
|
|
|
|
|
2–4 CI |
|
|
|
|
|
|
| 6.
|
|
|
|
1–5 CI |
|
我們需要證明以這種方式在推導中使用定理是合理的。為此，我們展示如何生成 **T2** 的正確、非簡寫推導，即不引用其簡寫證明中使用的定理的推導。
觀察到，當我們在 **T2** 的推導中輸入第 3 行時，我們在 **T1** 中用 替換了 。假設你對 **T1** 的證明的每一行應用相同的替換。那麼你將得到以下同樣正確的推導。
| |
| 1.
|
|
|
|
|
假設 ![{\displaystyle [\mathrm {Q} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c3c0af0222220bbc7f981fe3c5a3d969cb2fd7a9) |
|
|
|
|
|
|
| 2.
|
|
|
|
1 CI |
|
假設現在你用這個推導替換 **T2** 證明的第 3 行。你需要調整行號，以便每行號只有一行。你還需要調整註釋，以便它們繼續正確引用行號。但是，透過這些調整，你將得到以下 **T2** 的正確非簡寫推導。
| |
| 1.
|
|
|
|
|
假設 |
|
|
|
|
|
|
|
| 2.
|
|
|
|
|
|
假設 |
|
|
|
|
|
|
|
|
| 3.
|
|
|
|
|
|
|
假設 |
|
|
|
|
|
|
|
|
| 4.
|
|
|
|
|
|
3 CI |
| 5.
|
|
|
|
|
|
1, 4 CE |
|
|
|
|
|
|
|
| 6.
|
|
|
|
|
2–5 CI |
|
|
|
|
|
|
| 7.
|
|
|
|
1–6 CI |
|
因此，我們看到在推導中輸入先前證明的定理僅僅是對將該定理的證明包含在推導中的簡寫。上面關於非簡寫推導的說明可以更加概括和嚴格，但我們將保持它們處於這種非正式狀態。擁有生成正確非簡寫推導的說明證明了在推導中輸入先前證明的定理的合理性。
將在接下來的兩個模組中介紹其他定理。
