Solutions to Chapter 43 Natural deduction for ML ‣ Solutions to selected exercices ‣ forall x: Calgary

A. Provide proofs for all of the following:

1.

$\Box(A\wedge B)\vdash_{\mathbf{K}}\Box A\wedge\Box B$

Line number	Subproof level	Formula	Justification
1	0	$\Box(A\wedge B)$
2	open subproof, 1	$\Box$
3	1	$A\wedge B$	$\Box$ E 1
4	1	$A$	$\wedge$ E 3
5	close subproof, 0	$\Box A$	$\Box$ I 3–4
6	open subproof, 1	$\Box$
7	1	$A\wedge B$	$\Box$ E 1
8	1	$B$	$\wedge$ E 7
9	close subproof, 0	$\Box B$	$\Box$ I 6–8
10	0	$\Box A\wedge\Box B$	$\wedge$ I 5, 9

2.

$\Box A\wedge\Box B\vdash_{\mathbf{K}}\Box(A\wedge B)$

Line number	Subproof level	Formula	Justification
1	0	$\Box A\wedge\Box B$
2	0	$\Box A$	$\wedge$ E 1
3	0	$\Box B$	$\wedge$ E 1
4	open subproof, 1	$\Box$
5	1	$A$	$\Box$ E 2
6	1	$B$	$\Box$ E 3
7	1	$A\wedge B$	$\wedge$ I 5, 6
8	close subproof, 0	$\Box(A\wedge B)$	$\Box$ I 4–7

3.

$\Box A\vee\Box B\vdash_{\mathbf{K}}\Box(A\vee B)$

Line number	Subproof level	Formula	Justification
1	0	$\Box A\vee\Box B$
2	open subproof, 1	$\Box A$
3	open subproof, 2	$\Box$
4	2	$A$	$\Box$ E 2
5	2	$A\vee B$	$\vee$ I 4
6	close subproof, 1	$\Box(A\vee B)$	$\Box$ I 3–5
7	close subproof, open subproof, 1	$\Box B$
8	open subproof, 2	$\Box$
9	2	$B$	$\Box$ E 7
10	2	$A\vee B$	$\vee$ I 9
11	close subproof, 1	$\Box(A\vee B)$	$\Box$ I 8–10
12	close subproof, 0	$\Box(A\vee B)$	$\vee$ E 1, 2–6, 7–11

4.

$\Box(A\leftrightarrow B)\vdash_{\mathbf{K}}\Box A\leftrightarrow\Box B$

Line number	Subproof level	Formula	Justification
1	0	$\Box(A\leftrightarrow B)$
2	open subproof, 1	$\Box A$
3	open subproof, 2	$\Box$
4	2	$A\leftrightarrow B$	$\Box$ E 1
5	2	$A$	$\Box$ E 2
6	2	$B$	$\leftrightarrow$ E 4, 5
7	close subproof, 1	$\Box B$	$\Box$ I 3–6
8	close subproof, open subproof, 1	$\Box B$
9	open subproof, 2	$\Box$
10	2	$A\leftrightarrow B$	$\Box$ E 1
11	2	$B$	$\Box$ E 8
12	2	$A$	$\leftrightarrow$ E 10, 11
13	close subproof, 1	$\Box A$	$\Box$ I 9–12
14	close subproof, 0	$\Box A\leftrightarrow\Box B$	$\leftrightarrow$ I 2–7, 8–13

B. Provide proofs for the following (without using Modal Conversion!):

1.

$\neg\Box A\vdash_{\mathbf{K}}\Diamond\neg A$

Line number	Subproof level	Formula	Justification
1	0	$\neg\Box A$
2	open subproof, 1	$\Box\neg\neg A$
3	open subproof, 2	$\Box$
4	2	$\neg\neg A$	$\Box$ E 2
5	2	$A$	DNE 4
6	close subproof, 1	$\Box A$	$\Box$ I 3–5
7	1	$\bot$	$\neg$ E 1, 6
8	close subproof, 0	$\neg\Box\neg\neg A$	$\neg$ I 2–6
9	0	$\Diamond\neg A$	Def $\Diamond$ 8

2.

$\Diamond\neg A\vdash_{\mathbf{K}}\neg\Box A$

Line number	Subproof level	Formula	Justification
1	0	$\Diamond\neg A$
2	0	$\neg\Box\neg\neg A$	Def $\Diamond$ 1
3	open subproof, 1	$\Box A$
4	open subproof, 2	$\Box$
5	open subproof, 3	$\neg A$
6	3	$A$	$\Box$ E 3
7	3	$\bot$	$\neg$ E 5, 6
8	close subproof, 2	$\neg\neg A$	$\neg$ I 5–7
9	close subproof, 1	$\Box\neg\neg A$	$\Box$ I 4–8
10	1	$\bot$	$\neg$ E 2, 9
11	close subproof, 0	$\neg\Box A$	$\neg$ I 3–10

3.

$\neg\Diamond A\vdash_{\mathbf{K}}\Box\neg A$

Line number	Subproof level	Formula	Justification
1	0	$\neg\Diamond A$
2	open subproof, 1	$\neg\Box\neg A$
3	1	$\Diamond A$	Def $\Diamond$ 2
4	1	$\bot$	$\neg$ E 1, 3
5	close subproof, 0	$\neg\neg\Box\neg A$	$\neg$ I 2–4
6	0	$\Box\neg A$	DNE 5

4.

$\Box\neg A\vdash_{\mathbf{K}}\neg\Diamond A$

Line number	Subproof level	Formula	Justification
1	0	$\Box\neg A$
2	open subproof, 1	$\Diamond A$
3	1	$\neg\Box\neg A$	Def $\Diamond$ 2
4	1	$\bot$	$\neg$ E 1, 3
5	close subproof, 0	$\neg\Diamond A$	$\neg$ I 2–4

C. Provide proofs of the following (and now feel free to use Modal Conversion!):

1.

$\Box(A\rightarrow B),\Diamond A\vdash_{\mathbf{K}}\Diamond B$

Line number	Subproof level	Formula	Justification
1	0	$\Box(A\rightarrow B)$
2	0	$\Diamond A$
3	0	$\neg\Box\neg A$	Def $\Diamond$ 2
4	open subproof, 1	$\Box\neg B$
5	open subproof, 2	$\Box$
6	2	$A\rightarrow B$	$\Box$ E 1
7	2	$\neg B$	$\Box$ E 4
8	2	$\neg A$	MT 5, 6
9	close subproof, 1	$\Box\neg A$	$\Box$ I 5–8
10	1	$\bot$	$\neg$ E 3, 9
11	close subproof, 0	$\neg\Box\neg B$	$\neg$ I 4–10
12	0	$\Diamond B$	Def $\Diamond$ 11

2.

$\Box A\vdash_{\mathbf{K}}\neg\Diamond\neg A$

Line number	Subproof level	Formula	Justification
1	0	$\Box A$
2	open subproof, 1	$\Diamond\neg A$
3	1	$\neg\Box A$	MC 2
4	1	$\bot$	$\neg$ E 1, 3
5	close subproof, 0	$\neg\Diamond\neg A$	$\neg$ I 2–4

3.

$\neg\Diamond\neg A\vdash_{\mathbf{K}}\Box A$

Line number	Subproof level	Formula	Justification
1	0	$\neg\Diamond\neg A$
2	0	$\Box\neg\neg A$	MC 1
3	open subproof, 1	$\Box$
4	1	$\neg\neg A$	$\Box$ E 2
5	1	$A$	DNE 4
6	close subproof, 0	$\Box A$	$\Box$ I 3–5

D. Provide proofs for the following:

1.

$P\vdash_{\mathbf{T}}\Diamond P$

Line number	Subproof level	Formula	Justification
1	0	$P$
2	open subproof, 1	$\Box\neg P$
3	1	$\neg P$	R $\mathbf{T}$ 2
4	1	$\bot$	$\neg$ E 1, 3
5	close subproof, 0	$\neg\Box\neg P$	$\neg$ I 2–4
6	0	$\Diamond P$	Def $\Diamond$ 5

2.

$\vdash_{\mathbf{T}}(A\wedge B)\vee(\neg\Box A\vee\neg\Box B)$

Line number	Subproof level	Formula	Justification
1	open subproof, 1	$\Box A\wedge\Box B$
2	1	$\Box A$	$\wedge$ E 1
3	1	$\Box B$	$\wedge$ E 1
4	1	$A$	R $\mathbf{T}$ 2
5	1	$B$	R $\mathbf{T}$ 3
6	1	$A\wedge B$	$\wedge$ I 4, 5
7	1	$(A\wedge B)\vee(\neg\Box A\vee\neg\Box B)$	$\vee$ I 6
8	close subproof, open subproof, 1	$\neg(\Box A\wedge\Box B)$
9	1	$\neg\Box A\vee\neg\Box B$	DeM 8
10	1	$(A\wedge B)\vee(\neg\Box A\vee\neg\Box B)$	$\vee$ I 9
11	close subproof, 0	$(A\wedge B)\vee(\neg\Box A\vee\neg\Box B)$	LEM 1–7, 8–10

E. Provide proofs for the following:

1.

$\Box(\Box A\rightarrow B),\Box(\Box B\rightarrow C),\Box A\vdash_{\mathbf{S4}}% \Box\Box C$

Line number	Subproof level	Formula	Justification
1	0	$\Box(\Box A\rightarrow B)$
2	0	$\Box(\Box B\rightarrow C)$
3	0	$\Box A$
4	open subproof, 1	$\Box$
5	1	$\Box A$	R $\mathbf{4}$ 3
6	1	$\Box(\Box A\rightarrow B)$	R $\mathbf{4}$ 1
7	1	$\Box(\Box B\rightarrow C)$	R $\mathbf{4}$ 2
8	open subproof, 2	$\Box$
9	2	$\Box A$	R $\mathbf{4}$ 5
10	2	$\Box(\Box A\rightarrow B)$	R $\mathbf{4}$ 6
11	open subproof, 3	$\Box$
12	3	$\Box A$	R $\mathbf{4}$ 9
13	3	$\Box A\rightarrow B$	$\Box$ E 10
14	3	$B$	$\rightarrow$ E 12, 13
15	close subproof, 2	$\Box B$	$\Box$ I 11–14
16	2	$\Box B\rightarrow C$	$\Box$ E 7
17	2	$C$	$\rightarrow$ E 15, 16
18	close subproof, 1	$\Box C$	$\Box$ I 8–17
19	close subproof, 0	$\Box\Box C$	$\Box$ I 4–18

2.

$\Box A\vdash_{\mathbf{S4}}\Box(\Box A\vee B)$

Line number	Subproof level	Formula	Justification
1	0	$\Box A$
2	open subproof, 1	$\Box$
3	1	$\Box A$	R $\mathbf{4}$ 1
4	1	$\Box A\vee B$	$\vee$ I 4
5	close subproof, 0	$\Box(\Box A\vee B)$	$\Box$ I 2–4

3.

$\Diamond\Diamond A\vdash_{\mathbf{S4}}\Diamond A$

Line number	Subproof level	Formula	Justification
1	0	$\Diamond\Diamond A$
2	open subproof, 1	$\Box\neg A$
3	1	$\neg\Box\neg\Diamond A$	Def $\Diamond$ 1
4	open subproof, 2	$\Box$
5	2	$\Box\neg A$	R $\mathbf{4}$ 2
6	2	$\neg\Diamond A$	MC 5
7	close subproof, 1	$\Box\neg\Diamond A$	$\Box$ I 4–6
8	1	$\bot$	$\neg$ E 3, 7
9	close subproof, 0	$\neg\Box\neg A$	$\neg$ I 2–8
10	0	$\Diamond A$	Def $\Diamond$ 9

F. Provide proofs for the following:

1.

$\neg\Box\neg A,\Diamond B\vdash_{\mathbf{S5}}\Box(\Diamond A\wedge\Diamond B)$

Line number	Subproof level	Formula	Justification
1	0	$\neg\Box\neg A$
2	0	$\Diamond B$
3	0	$\neg\Box\neg B$	Def $\Diamond$ 2
4	open subproof, 1	$\Box$
5	1	$\neg\Box\neg A$	R $\mathbf{5}$ 1
6	1	$\Diamond A$	Def $\Diamond$ 5
7	1	$\neg\Box\neg B$	R $\mathbf{5}$ 3
8	1	$\Diamond B$	Def $\Diamond$ 7
9	1	$\Diamond A\wedge\Diamond B$	$\wedge$ I 6, 8
10	close subproof, 0	$\Box(\Diamond A\wedge\Diamond B)$	$\Box$ I 4–9

2.

$A\vdash_{\mathbf{S5}}\Box\Diamond A$

Line number	Subproof level	Formula	Justification
1	0	$A$
2	open subproof, 1	$\Box\neg A$
3	1	$\neg A$	R $\mathbf{T}$ 2
4	1	$\bot$	$\neg$ E 1, 3
5	close subproof, 0	$\neg\Box\neg A$
6	open subproof, 1	$\Box$
7	1	$\neg\Box\neg A$	R $\mathbf{5}$ 5
8	1	$\Diamond A$	Def $\Diamond$ 7
9	close subproof, 0	$\Box\Diamond A$	$\Box$ I 6–8

3.

$\Diamond\Diamond A\vdash_{\mathbf{S5}}\Diamond A$

Line number	Subproof level	Formula	Justification
1	0	$\Diamond\Diamond A$
2	0	$\neg\Box\neg\Diamond A$	Def $\Diamond$ 1
3	open subproof, 1	$\Box$
4	open subproof, 2	$\Box\neg A$
5	open subproof, 3	$\Box$
6	open subproof, 4	$\Diamond A$
7	4	$\neg\Box\neg A$	Def $\Diamond$ 6
8	4	$\Box\neg A$	R $\mathbf{4}$ 4
9	4	$\bot$	$\neg$ E 7, 8
10	close subproof, 3	$\neg\Diamond A$	$\neg$ I 5–9
11	close subproof, 2	$\Box\neg\Diamond A$	$\Box$ I 5–10
12	2	$\neg\Box\neg\Diamond A$	R $\mathbf{5}$ 2
13	2	$\bot$	$\neg$ E 11, 12
14	close subproof, 1	$\neg\Box\neg A$	$\neg$ I 4–13
15	1	$\Diamond A$	Def $\Diamond$ 14
16	close subproof, 0	$\Box\Diamond A$	$\Box$ I 3–15
17	0	$\Diamond A$	R $\mathbf{T}$ 16