A theorem is a formula for which a zero-premise derivation has been provided. We will keep a numbered list of proved theorems. In the derivations that follow, we will continue our informal convention of adding a formula to the annotations of assumptions, in particular the formula we hope to derive by means of the newly started subderivation.
You may remember from Constructing a Complex Derivation that we had to employ a silly trick to copy a formula into the proper subderivation (Lines 16 and 17). We can prove a theorem that will help us avoid such obnoxiousness.
1.
Assumption
2.
1 CI
Derivations can be abbreviated by allowing a line to be entered whose formula is a substitution instance of a previously proved theorem. The annotation will be 'Tn' where n is the number of the theorem. Although we won't require it officially, we will also show the substitution, if any, in the annotation (see Line 3 in the derivation below). The proof of the next theorem will use T1.
1.
Assumption
2.
Assumption
3.
T1 [P/Q]
4.
1, 3 CE
5.
2–4 CI
6.
1–5 CI
Justification: Converting to unabbreviated derivation
We need to justify using theorems in derivations in this way. To do that, we show how to produce a correct, unabbreviated derivation of T2, one without citing the theorem we used in its abbreviated proof.
Observe that when we entered Line 3 into our derivation of T2, we substituted for in T1. Suppose you were to apply the same substitution on each line of our proof for T1. You would then end up with the following equally correct derivation.
1.
Assumption
2.
1 CI
Suppose now you were to replace Line 3 of our proof for T2 with this derivation. You would need to adjust the line numbers so that you would have only one line per line number. You would also need to adjust the annotations so the line numbers they would continue to refer correctly. But, with these adjustments, you would end up with the following correct unabbreviated derivation of T2.
1.
Assumption
2.
Assumption
3.
Assumption
4.
3 CI
5.
1, 4 CE
6.
2–5 CI
7.
1–6 CI
Thus we see that entering a previously proved theorem into a derivation is simply an abbreviation for including that theorem's proof into a derivation. The instructions above for unabbreviating a derivation could be made more general and more rigorous, but we will leave them in this informal state. Having instructions for generating a correct unabbreviated derivation justifies entering previously proved theorems into derivations.
![{\displaystyle [\mathrm {P} \rightarrow \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/79933dc3c8b22ad47c5f28386ff6e8976b768d5e)
![{\displaystyle [\mathrm {Q} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b8be83a1ab88d731a8b904852f116034ad2939)
![{\displaystyle [\mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/97cf4af3c1bca8188faa85c99bb829c88690a523)
![{\displaystyle [\mathrm {Q} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c3c0af0222220bbc7f981fe3c5a3d969cb2fd7a9)