Chapter 40 Derived rules
As in the case of TFL, we first introduced some rules for FOL as basic (in chapter 36), and then added some further rules for conversion of quantifiers (in chapter 38). In fact, the CQ rules should be regarded as derived rules, for they can be derived from the basic rules of chapter 36. (The point here is as in chapter 21.) Here is a justification for the first CQ rule:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\forall x\mathrm{\neg}A(x)$


$m+1$ 
open subproof,
1

$\exists xA(x)$

AS

$m+2$ 
open subproof,
2

$A(c)$

AS

$m+3$ 
2

$\mathrm{\neg}A(c)$

$\forall $E $m$

$m+4$ 
2

$\perp $

$\mathrm{\neg}$E $m+3$, $m+2$

$m+5$ 
close subproof,
1

$\perp $

$\exists $E $m+1$, ($m+2$)–($m+4$)

$m+6$ 
close subproof,
0

$\mathrm{\neg}\exists xA(x)$

$\mathrm{\neg}$I ($m+1$)–($m+5$)

Here is a justification of the third CQ rule:
Line number

Subproof level

Formula

Justification


$m$ 
0

$\exists x\mathrm{\neg}A(x)$


$m+1$ 
open subproof,
1

$\forall xA(x)$

AS

$m+2$ 
open subproof,
2

$\mathrm{\neg}A(c)$

AS

$m+3$ 
2

$A(c)$

$\forall $E $m+1$

$m+4$ 
2

$\perp $

$\mathrm{\neg}$E $m+2$, $m+3$

$m+5$ 
close subproof,
1

$\perp $

$\exists $E $m$, ($m+2$)–($m+4$)

$m+6$ 
close subproof,
0

$\mathrm{\neg}\forall xA(x)$

$\mathrm{\neg}$I ($m+1$)–($m+5$)

This explains why the CQ rules can be treated as derived. Similar justifications can be offered for the other two CQ rules.
Practice exercises
A. Offer proofs which justify the addition of the second and fourth CQ rules as derived rules.