Chapter 21 Derived rules
In this section, we will see why we introduced the rules of our proof system in two separate batches. In particular, we want to show that the additional rules of chapter 19 are not strictly speaking necessary, but can be derived from the basic rules of chapter 17.
21.1 Derivation of Reiteration
To illustrate what it means to derive a rule from other rules, first consider reiteration. It is a basic rule of our system, but it is also not necessary. Suppose you have some sentence on some line of your deduction:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\mathcal{A}$


You now want to repeat yourself, on some line $k$. You could just invoke the rule R. But equally well, you can do this with other basic rules of chapter 17:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\mathcal{A}$


$k$ 
0

$\mathcal{A}\wedge \mathcal{A}$

$\wedge $I $m$, $m$

$k+1$ 
0

$\mathcal{A}$

$\wedge $E $k$

To be clear: this is not a proof. Rather, it is a proof scheme. After all, it uses a variable, ‘$\mathcal{A}$’, rather than a sentence of TFL, but the point is simple: Whatever sentences of TFL we plugged in for ‘$\mathcal{A}$’, and whatever lines we were working on, we could produce a bona fide proof. So you can think of this as a recipe for producing proofs.
Indeed, it is a recipe which shows us the following: anything we can prove using the rule R, we can prove (with one more line) using just the basic rules of chapter 17 without R. That is what it means to say that the rule R can be derived from the other basic rules: anything that can be justified using R can be justified using only the other basic rules.
21.2 Derivation of Disjunctive Syllogism
Suppose that you are in a proof, and you have something of this form:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\mathcal{A}\vee \mathcal{B}$


$n$ 
0

$\neg \mathcal{A}$


You now want, on line $k$, to prove $\mathcal{B}$. You can do this with the rule of DS, introduced in chapter 19, but equally well, you can do this with the basic rules of chapter 17:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\mathcal{A}\vee \mathcal{B}$


$n$ 
0

$\neg \mathcal{A}$


$k$ 
open subproof,
1

$\mathcal{A}$

AS

$k+1$ 
1

$\perp $

$\neg $E $n$, $k$

$k+2$ 
1

$\mathcal{B}$

X $k+1$

$k+3$ 
close subproof,
open subproof,
1

$\mathcal{B}$

AS

$k+4$ 
1

$\mathcal{B}$

R $k+3$

$k+5$ 
close subproof,
0

$\mathcal{B}$

$\vee $E $m$, $k$–$k+2$, $k+3$–$k+4$

So the DS rule, again, can be derived from our more basic rules. Adding it to our system did not make any new proofs possible. Anytime you use the DS rule, you could always take a few extra lines and prove the same thing using only our basic rules. It is a derived rule.
21.3 Derivation of Modus Tollens
Suppose you have the following in your proof:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\mathcal{A}\to \mathcal{B}$


$n$ 
0

$\neg \mathcal{B}$


You now want, on line $k$, to prove $\neg \mathcal{A}$. You can do this with the rule of MT, introduced in chapter 19. Equally well, you can do this with the basic rules of chapter 17:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\mathcal{A}\to \mathcal{B}$


$n$ 
0

$\neg \mathcal{B}$


$k$ 
open subproof,
1

$\mathcal{A}$

AS

$k+1$ 
1

$\mathcal{B}$

$\to $E $m$, $k$

$k+2$ 
1

$\perp $

$\neg $E $n$, $k+1$

$k+3$ 
close subproof,
0

$\neg \mathcal{A}$

$\neg $I $k$–$k+2$

Again, the rule of MT can be derived from the basic rules of chapter 17.
21.4 Derivation of DoubleNegation Elimination
Consider the following deduction scheme:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\neg \neg \mathcal{A}$


$k$ 
open subproof,
1

$\neg \mathcal{A}$

AS

$k+1$ 
1

$\perp $

$\neg $E $m$, $k$

$k+2$ 
close subproof,
0

$\mathcal{A}$

IP $k$–$k+1$

Again, we can derive the DNE rule from the basic rules of chapter 17.
21.5 Derivation of Excluded Middle
Suppose you want to prove something using the LEM rule, i.e., you have in your proof
Line number

Subproof level

Formula

Justification


$m$ 
open subproof,
1

$\mathcal{A}$

AS

$n$ 
1

$\mathcal{B}$


$k$ 
close subproof,
open subproof,
1

$\neg \mathcal{A}$

AS

$l$ 
1

$\mathcal{B}$


You now want, on line $l+1$, to prove $\mathcal{B}$. The rule LEM from chapter 19 would allow you to do it. But can you do this with the basic rules of chapter 17?
One option is to first prove $\mathcal{A}\vee \neg \mathcal{A}$, and then apply $\vee $E, i.e., proof by cases:
Line number

Subproof level

Formula

Justification


$m$ 
open subproof,
1

$\mathcal{A}$

AS

$n$ 
1

$\mathcal{B}$


$k$ 
close subproof,
open subproof,
1

$\neg \mathcal{A}$

AS

$l$ 
1

$\mathcal{B}$


close subproof,
0

$\mathrm{\vdots}$



$i$ 
0

$\mathcal{A}\vee \neg \mathcal{A}$


$i+1$ 
0

$\mathcal{B}$

$\vee $E $i$, $m$–$n$, $k$–$l$

(We gave a proof of $\mathcal{A}\vee \neg \mathcal{A}$ using only our basic rules in section 18.6.)
Here is another way that is a bit more complicated than the ones before. What you have to do is embed your two subproofs inside another subproof. The assumption of the subproof will be $\neg \mathcal{B}$, and the last line will be $\perp $. Thus, the complete subproof is the kind you need to conclude $\mathcal{B}$ using IP. Inside the proof, you’d have to do a bit more work to get $\perp $:
Line number

Subproof level

Formula

Justification


$m$ 
open subproof,
1

$\neg \mathcal{B}$

AS

$m+1$ 
open subproof,
2

$\mathcal{A}$

AS

2

$\mathrm{\vdots}$



$n$ 
2

$\mathcal{B}$


$n+1$ 
2

$\perp $

$\neg $E $m$, $n$

$n+2$ 
close subproof,
open subproof,
2

$\neg \mathcal{A}$

AS

2

$\mathrm{\vdots}$



$l$ 
2

$\mathcal{B}$


$l+1$ 
2

$\perp $

$\neg $E $m$, $l$

$l+2$ 
close subproof,
1

$\neg \mathcal{A}$

$\neg $I ($m+1$)–($n+1$)

$l+3$ 
1

$\neg \neg \mathcal{A}$

$\neg $I ($n+2$)–($l+1$)

$l+4$ 
1

$\perp $

$\neg $E $l+3$, $l+2$

$l+5$ 
close subproof,
0

$\mathcal{B}$

IP $m$–($l+4$)

Note that because we add an assumption at the top and additional conclusions inside the subproofs, the line numbers change. You may have to stare at this for a while before you understand what’s going on.
21.6 Derivation of De Morgan rules
Here is a demonstration of how we could derive the first De Morgan rule:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\neg (\mathcal{A}\wedge \mathcal{B})$


$k$ 
open subproof,
1

$\mathcal{A}$

AS

$k+1$ 
open subproof,
2

$\mathcal{B}$

AS

$k+2$ 
2

$\mathcal{A}\wedge \mathcal{B}$

$\wedge $I $k$, $k+1$

$k+3$ 
2

$\perp $

$\neg $E $m$, $k+2$

$k+4$ 
close subproof,
1

$\neg \mathcal{B}$

$\neg $I ($k+1$)–($k+3$)

$k+5$ 
1

$\neg \mathcal{A}\vee \neg \mathcal{B}$

$\vee $I $k+4$

$k+6$ 
close subproof,
open subproof,
1

$\neg \mathcal{A}$

AS

$k+7$ 
1

$\neg \mathcal{A}\vee \neg \mathcal{B}$

$\vee $I $k+6$

$k+8$ 
close subproof,
0

$\neg \mathcal{A}\vee \neg \mathcal{B}$

LEM $k$–($k+5$), ($k+6$)–($k+7$)

Here is a demonstration of how we could derive the second De Morgan rule:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\neg \mathcal{A}\vee \neg \mathcal{B}$


$k$ 
open subproof,
1

$\mathcal{A}\wedge \mathcal{B}$

AS

$k+1$ 
1

$\mathcal{A}$

$\wedge $E $k$

$k+2$ 
1

$\mathcal{B}$

$\wedge $E $k$

$k+3$ 
open subproof,
2

$\neg \mathcal{A}$

AS

$k+4$ 
2

$\perp $

$\neg $E $k+3$, $k+1$

$k+5$ 
close subproof,
open subproof,
2

$\neg \mathcal{B}$

AS

$k+6$ 
2

$\perp $

$\neg $E $k+5$, $k+2$

$k+7$ 
close subproof,
1

$\perp $

$\vee $E $m$, ($k+3$)–($k+4$), ($k+5$)–($k+6$)

$k+8$ 
close subproof,
0

$\neg (\mathcal{A}\wedge \mathcal{B})$

$\neg $I $k$–($k+7$)

Similar demonstrations can be offered explaining how we could derive the third and fourth De Morgan rules. These are left as exercises.
Practice exercises
A. Provide proof schemes that justify the addition of the third and fourth De Morgan rules as derived rules.
B. The proofs you offered in response to the practice exercises of chapters 19 to 20 used derived rules. Replace the use of derived rules, in such proofs, with only basic rules. You will find some ‘repetition’ in the resulting proofs; in such cases, offer a streamlined proof using only basic rules. (This will give you a sense, both of the power of derived rules, and of how all the rules interact.)
C. Give a proof of $\mathcal{A}\vee \neg \mathcal{A}$. Then give a proof that uses only the basic rules.
D. Show that if you had LEM as a basic rule, you could justify IP as a derived rule. That is, suppose you had the proof:
Line number

Subproof level

Formula

Justification


$m$ 
open subproof,
1

$\neg \mathcal{A}$

AS

1

$\mathrm{\dots}$



$n$ 
1

$\perp $


How could you use it to prove $\mathcal{A}$ without using IP but with using LEM as well as all the other basic rules?
E. Give a proof of the first De Morgan rule, but using only the basic rules, in particular, without using LEM. (Of course, you can combine the proof using LEM with the proof of LEM. Try to find a proof directly.)