Logic Text Chapter 7 Solutions

Chapter 7: Natural Deduction

Basic

Question {7.1}

A ⊃ ~ B ⊢ B ⊃ ~ A :

1B ⊢ BAx.
2A ⊃ ~ B ⊢ A ⊃ ~ BAx.
3A ⊢ AAx.
4A ⊃ ~ B, A ⊢ ~ B2,3 (⊃ E)
5A ⊃ ~ B, A, B ⊢ \bot 1,4 (~ E)
6A ⊃ ~ B, B ⊢ ~ A5 (~ I)
7A ⊃ ~ B ⊢ B ⊃ ~ A6 (⊃ I)

~ ~ ~ A ⊢ ~ A :

1~ ~ ~ A ⊢ ~ ~ ~ AAx.
2A ⊢ AAx.
3~ A ⊢ ~ AAx.
4A, ~ A ⊢ \bot 2,3 (~ E)
5A ⊢ ~~ A4 (~ I)
6~ ~ ~ A, A ⊢ \bot 1,5 (~ E)
7~ ~ ~ A ⊢ ~ A6 (~ I)

~ A ∨ ~ B ⊢ ~(A & B) :

1~ A ∨ ~ B ⊢ ~ A ∨ ~ BAx.
2A & B, ~ A ⊢ A & BAx.
3A & B, ~ A ⊢ A2 (& E)
4A & B, ~ A ⊢ ~ AAx.
5A & B, ~ A ⊢ \bot 3,4 (~ E)
6A & B, ~ B ⊢ A & BAx.
7A & B, ~ B ⊢ B6 (& E)
8A & B, ~ B ⊢ ~ BAx.
9A & B, ~ B ⊢ \bot 7,8 (~ E)
10~ A ∨ ~ B, (A & B) ⊢ \bot 1,5,9 (∨ E)
11~ A ∨ ~ B ⊢ ~(A & B)10 (~ I)

~(A ∨ B) ⊢ ~ A & ~ B :

1~(A ∨ B) ⊢ ~(A ∨ B)Ax.
2A ⊢ AAx.
3A ⊢ A ∨ B2 (∨ I)
4~(A ∨ B), A ⊢ \bot 1,3 (~ E)
5~(A ∨ B) ⊢ ~ A4 (~ I)
6B ⊢ BAx.
7B ⊢ A ∨ B6 (∨ I)
8~(A ∨ B), B ⊢ \bot 1,7 (~ E)
9~(A ∨ B) ⊢ ~ B8 (~ I)
10~(A ∨ B) ⊢ ~ A & ~ B5,9 (& I)

A & ~ B ⊢ ~(A ⊃ B) :

1A & ~ B ⊢ A & ~ BAx.
2A & ~ B ⊢ ~ B1 (& E)
3A & ~ B ⊢ A1 (& E)
4A ⊃ B ⊢ A ⊃ BAx.
5A & ~ B, A ⊃ B ⊢ B3,4 (⊃ E)
6A & ~ B, A ⊃ B ⊢ \bot 2,5 (~ E)
7A & ~ B ⊢ ~(A ⊃ B)6 (~ I)

Question {7.2}

⊢ ((A ⊃ B) ⊃ A) ⊃ A :

1~ A ⊢ ~ AAx.
2A ⊢ AAx.
3~ A, A ⊢ \bot 1,2 (~ E)
4~ A, A ⊢ B3 (\bot E)
5~ A ⊢ A ⊃ B4 (⊃ I)
6(A ⊃ B) ⊃ A ⊢ (A ⊃ B) ⊃ AAx.
7(A ⊃ B) ⊃ A, ~ A ⊢ A5,6 (⊃ E)
8(A ⊃ B) ⊃ A, ~ A ⊢ \bot 1,7 (~ E)
9(A ⊃ B) ⊃ A ⊢ ~~ A8 (~ I)
10(A ⊃ B) ⊃ A ⊢ A9 (DNE)
11⊢ ((A ⊃ B) ⊃ A) ⊃ A10 (⊃ I)

~(A & B) ⊢ ~ A ∨ ~ B :

1~(~ A ∨ ~ B) ⊢ ~(~ A ∨ ~ B)Ax.
2~ A ⊢ ~ AAx.
3~ A ⊢ ~ A ∨ ~ B2 (∨ I)
4~(~ A ∨ ~ B), ~ A ⊢ \bot 1,3 (~ E)
5~(~ A ∨ ~ B) ⊢ ~~ A4 (~ I)
6~(~ A ∨ ~ B) ⊢ A5 (DNE)
7~ B ⊢ ~ BAx.
8~ B ⊢ ~ A ∨ ~ B7 (∨ I)
9~(~ A ∨ ~ B), ~ B ⊢ \bot 1,8 (~ E)
10~(~ A ∨ ~ B) ⊢ ~~ B9 (~ I)
11~(~ A ∨ ~ B) ⊢ B10 (DNE)
12~(~ A ∨ ~ B) ⊢ A & B6,11 (& I)
13~(A & B) ⊢ ~(A & B)Ax.
14~(A & B), ~(~ A ∨ ~ B) ⊢ \bot 12,13 (~ E)
15~(A & B) ⊢ ~~(~ A ∨ ~ B)14 (~ I)
16~(A & B) ⊢ ~ A ∨ ~ B15 (DNE)

⊢ A ∨ (A ⊃ B) :

1~(A ∨ (A ⊃ B)) ⊢ ~(A ∨ (A ⊃ B))Ax.
2A ⊢ AAx.
3~ A ⊢ ~ AAx.
4A, ~ A ⊢ \bot 2,3 (~ E)
5A, ~ A ⊢ B4 (\bot E)
6~ A ⊢ A ⊃ B5 (⊃ I)
7~ A ⊢ A ∨ (A ⊃ B)6 (∨ I)
8~(A ∨ (A ⊃ B)), ~ A ⊢ \bot 1,7 (~ E)
9~(A ∨ (A ⊃ B)) ⊢ ~~ A8 (~ I)
10~(A ∨ (A ⊃ B)) ⊢ A9 (DNE)
11~(A ∨ (A ⊃ B)) ⊢ A ∨ (A ⊃ B)10 (∨ I)
12~(A ∨ (A ⊃ B)) ⊢ \bot 1,11 (~ I)
13⊢ ~~(A ∨ (A ⊃ B))12 (~ I)
14⊢ A ∨ (A ⊃ B)13 (DNE)

~ A ⊃ ~ B ⊢ B ⊃ A :

1~ A ⊢ ~ AAx.
2~ A ⊃ ~ B ⊢ ~ A ⊃ ~ BAx.
3~ A ⊃ ~ B, ~ A ⊢ ~ B1,2 (⊃ E)
4B ⊢ BAx.
5~ A ⊃ ~ B, ~ A, B ⊢ \bot 3,4 (~ E)
6~ A ⊃ ~ B, B ⊢ ~~ A5 (~ I)
7~ A ⊃ ~ B, B ⊢ A6 (DNE)
8~ A ⊃ ~ B ⊢ B ⊃ A7 (⊃ I)

(A & B) ⊃ C ⊢ (A ⊃ C) ∨ (B ⊃ C) :

1A ⊢ AAx.
2B ⊢ BAx.
3A, B ⊢ A & B1,2 (& I)
4(A & B) ⊃ C ⊢ (A & B) ⊃ CAx.
5(A & B) ⊃ C, A, B ⊢ C3,4 (⊃ E)
6(A & B) ⊃ C, A ⊢ B ⊃ C5 (⊃ I)
7(A & B) ⊃ C, A ⊢ (A ⊃ C) ∨ (B ⊃ C)6 (∨ I)
8~((A ⊃ C) ∨ (B ⊃ C)) ⊢ ~((A ⊃ C) ∨ (B ⊃ C))Ax.
9(A & B) ⊃ C, A, ~((A ⊃ C) ∨ (B ⊃ C)) ⊢ \bot 7,8 (~ E)
10(A & B) ⊃ C, A, ~((A ⊃ C) ∨ (B ⊃ C)) ⊢ C9 (\bot E)
11(A & B) ⊃ C, ~((A ⊃ C) ∨ (B ⊃ C)) ⊢ A ⊃ C10 (⊃ I)
12(A & B) ⊃ C, ~((A ⊃ C) ∨ (B ⊃ C)) ⊢ (A ⊃ C) ∨ (B ⊃ C)11 (∨ I)
13(A & B) ⊃ C, ~((A ⊃ C) ∨ (B ⊃ C)) ⊢ \bot 8,12 (~ E)
14(A & B) ⊃ C ⊢ ~~((A ⊃ C) ∨ (B ⊃ C))13 (~ I)
15(A & B) ⊃ C ⊢ (A ⊃ C) ∨ (B ⊃ C)14 (DNE)