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