一个定理是一个公式，它已经提供了零前提推导。我们将保留一个已证明定理的编号列表。在接下来的推导中，我们将继续使用我们的非正式约定，在假设的注释中添加一个公式，特别是我们希望通过新开始的子推导推导出的公式。
您可能记得，在 构建复杂推导 中，我们不得不使用一个愚蠢的技巧来将一个公式复制到正确的子推导中（第 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 |
|
因此，我们看到在推导中输入先前证明的定理仅仅是对将该定理的证明包含在推导中的简写。上面关于非简写推导的说明可以更加概括和严格，但我们将保持它们处于这种非正式状态。拥有生成正确非简写推导的说明证明了在推导中输入先前证明的定理的合理性。
将在接下来的两个模块中介绍其他定理。
