Now we can carry the abbreviation a step further. A derived inference rule is an inference rule not given to us as part of the derivation system but which constitutes an abbreviation using a previously proved theorem. In particular, suppose we have proved a particular theorem. In this theorem, uniformly replace each sentence letter with a distinct Greek letter. Suppose the result has the following form.
.
[Comment: This and what follows seems to me to be potentially confusing to students. The intention stated in earlier sections to avoid metatheory creates a problem here as one needs to know about the Deduction Theorem for this to make more sense.]
We may then introduce a derived inference rule having the form
An application of the derived rule can be eliminated by replacing it with
the previously proved theorem,
repeated applications of Conjunction Introduction (KI) to build up the theorem's antecedent, and
an application of Conditional Elimination (CE) to obtain the theorem's consequent.
The previously proved theorem can then be eliminated as described above. That would leave you with an unabbreviated derivation.
Removing abbreviations from a derivation is not desirable, of course, because it makes the derivation more complicated and harder to read, but the fact that a derivation could be unabbreviated justifies the use of abbreviations, so that we can employ abbreviations in the first place.
Our first derived inference rule will be based on T1, which is
Replace the sentence letters with Greek letters, and we get:
We now generate the derived inference rule:
Repetition (R)
Now we can show how this rule could have simplified our proof of T2.
1.
Assumption
2.
Assumption
3.
1 R
4.
2–3 CI
5.
1–4 CI
While this is only one line shorter than our original proof of T2, it is less obnoxious. We can use an inference rule instead of a silly trick. As a result, the derivation is easier to read and understand (not to mention easier to produce).
This rule is occasionally useful when you have derived a contradiction but the discharge rule you want is not NI or NE. This then avoids a completely trivial subderivation. The rule of Contradiction will be used in the proof of the next theorem.
On the basis of T2 and T6, we introduce the following derived rule.
Conditional Addition, Form I (CAdd)
Conditional Addition, Form II (CAdd)
The name 'Conditional Addition' is not in common use. It is based on the traditional name for Disjunction Introduction, namely 'Addition'. This rule does not provide a general means of introducing a conditional. This is because the antecedent line you would need is not always derivable. However, when the antecedent line just happens to be easily available, then applying this rule is simpler than producing the subderivation needed for a Conditional Introduction.
Modus Tollens is also sometimes known as 'Denying the Consequent'. Note that the following is not an instance of Modus Tollens, at least as defined above.
The premise lines of Modus Tollens are a conditional and the negation of its consequent. The premise lines of this inference are a conditional and the opposite of its consequent, but not the negation of its consequent. The desired inference here needs to be derived as below.
1.
Premise
2.
Premise
3.
2 DNI
4.
1, 3 CE
5.
4 DNE
Of course, it is possible to prove as a theorem:
Then you can add a new inference rule—or, more likely, a new form of Modus Tollens—on the basis of this theorem. However, we won't do that here.
The derived rules given so far are quite useful for eliminating frequently used bits of obnoxiousness in our derivations. They will help to make your derivations easier to generate and also more readable. However, because they are indeed derived rules, they are not strictly required but rather are theoretically dispensable.
A number of other theorems and derived rules could usefully be added. We list here some useful theorems but leave their proofs and the definition of their associated derived inference rules to the reader. If you construct many derivations, you may want to maintain your own personal list that you find useful.
![{\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 {P} \rightarrow \lnot \lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5a010f77ae19f9aea6fabf12869899e6216e77bc)
![{\displaystyle [\lnot \lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d56c2499de3ac67a73cdcaca427dce5605b4320b)
![{\displaystyle [\lnot \lnot \mathrm {P} \rightarrow \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d1bb69f44806a433fd72926eb47f9b4ffa7a043c)
![{\displaystyle [\mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/81936377579d3940eeb3983f919467358a9f12aa)
![{\displaystyle [\mathrm {P} \land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/218e914cb2dfec118a310f2d3b6de200ee6e08d2)
![{\displaystyle [\mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b99e6e42dce9a0938a5354e1018054a02fca2ad3)
![{\displaystyle [\lnot \mathrm {P} \rightarrow (\mathrm {P} \rightarrow \mathrm {Q} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de406ff15ac87549e0b995a4fa7d7e4dc2b2fea1)
![{\displaystyle [(\mathrm {P} \rightarrow \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/822876910ec839e4e6294e59bb10a63c5aa3d174)
![{\displaystyle [\lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ebecf005a1793b292d92ddec0a677c0612909c89)
