Solutions to Chapter 40 Derived rules ‣ Solutions to selected exercices ‣ forall x: Calgary

A. Offer proofs which justify the addition of the second and fourth CQ rules as derived rules.

Justification for the second rule:

Line number	Subproof level	Formula	Justification
$1$	0	$\neg\exists x\,A(x)$
$2$	open subproof, 1	$A(a)$
$3$	1	$\exists x\,A(x)$	$\exists$ I $2$
$4$	1	$\bot$	$\neg$ E $3$ , $1$
$5$	close subproof, 0	$\neg A(a)$	$\neg$ I $2$ – $4$
$6$	0	$\forall x\neg A(x)$	$\forall$ I $5$

The fourth rule is harder to justify. Here is a proof that is relatively straightforward, but uses the derived rule DNE:

Line number	Subproof level	Formula	Justification
$1$	0	$\neg\forall x\,A(x)$
$2$	open subproof, 1	$\neg\exists x\neg A(x)$
$3$	open subproof, 2	$\neg A(a)$
$4$	2	$\exists x\neg A(x)$	$\exists$ I $3$
$5$	2	$\bot$	$\neg$ E $4$ , $2$
$6$	close subproof, 1	$\neg\neg A(a)$	$\neg$ I $3$ – $5$
$7$	1	$A(a)$	DNE $6$
$8$	1	$\forall x\,A(x)$	$\forall$ I $7$
$9$	1	$\bot$	$\neg$ E $8$ , $1$
$10$	close subproof, 0	$\neg\neg\exists x\neg A(x)$	$\neg$ I $2$ – $9$
$11$	0	$\exists x\neg A(x)$	DNE $10$

And here is a proof that does not use any derived rules:

Line number	Subproof level	Formula	Justification
$1$	0	$\neg\forall x\,A(x)$
$2$	open subproof, 1	$\exists x\neg A(x)$
$3$	1	$\exists x\neg A(x)\wedge\exists x\neg A(x)$	$\wedge$ I $2$
$4$	1	$\exists x\neg A(x)$	$\wedge$ E $3$
$5$	close subproof, open subproof, 1	$\neg\exists x\neg A(x)$
$6$	open subproof, 2	$A(b)$
$7$	2	$A(b)\wedge A(b)$	$\wedge$ I $6$
$8$	2	$A(b)$	$\wedge$ E $7$
$9$	close subproof, open subproof, 2	$\neg A(b)$
$10$	2	$\exists x\neg A(x)$	$\exists$ I $9$
$11$	2	$\bot$	$\neg$ E $10$ , $5$
$12$	2	$A(b)$	X $11$
$13$	close subproof, 1	$A(b)$	LEM $6$ – $8$ , $9$ – $12$
$14$	1	$\forall x\,A(x)$	$\forall$ I $13$
$15$	1	$\bot$	$\neg$ E $14$ , $1$
$16$	1	$\exists x\neg A(x)$	X $15$
$17$	close subproof, 0	$\exists x\neg A(x)$	LEM $2$ – $4$ , $5$ – $16$