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\,\neg A(x)$
$m+1$	open subproof, 1	$\exists x\,A(x)$	AS
$m+2$	open subproof, 2	$A(c)$	AS
$m+3$	2	$\neg A(c)$	$\forall$ E $m$
$m+4$	2	$\bot$	$\neg$ E $m+3$ , $m+2$
$m+5$	close subproof, 1	$\bot$	$\exists$ E $m+1$ , ( $m+2$ )–( $m+4$ )
$m+6$	close subproof, 0	$\neg\exists x\,A(x)$	$\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\,\neg A(x)$
$m+1$	open subproof, 1	$\forall x\,A(x)$	AS
$m+2$	open subproof, 2	$\neg A(c)$	AS
$m+3$	2	$A(c)$	$\forall$ E $m+1$
$m+4$	2	$\bot$	$\neg$ E $m+2$ , $m+3$
$m+5$	close subproof, 1	$\bot$	$\exists$ E $m$ , ( $m+2$ )–( $m+4$ )
$m+6$	close subproof, 0	$\neg\forall x\,A(x)$	$\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.