4.2.xa. Exercise answers

1. a.
│A ∧ B 1
├─
1 Ext │A
1 Ext │B (3)
│
││¬ A
│├─
││●
│├─
3 QED ││B 2
├─
2 PE │A ∨ B
b.
│A ∧ B 1
├─
1 Ext │A
1 Ext │B (3)
│
││¬ C
│├─
││●
│├─
3 QED ││B 2
├─
2 PE │B ∨ C
c.
│A ∨ B 1
│¬ A (3)
├─
││A (3)
│├─
│││¬ B
││├─
│││●
││├─
3 Nc │││⊥ 2
│├─
2 IP ││B 1
│
││B (4)
│├─
││●
│├─
4 QED ││B 1
├─
1 PC │B
d.
│A ∨ (A ∧ B) 1
├─
││A (2)
│├─
││●
│├─
2 QED ││A 1
│
││A ∧ B 3
│├─
3 Ext ││A (4)
3 Ext ││B
││●
│├─
4 QED ││A 1
├─
1 PC │A
e.
│A ∨ B 2
│¬ (A ∧ C) 3
│¬ (B ∧ C) 7
├─
││C (6),(10)
│├─
│││A (5)
││├─
│││││●
││││├─
5 QED │││││A 4
││││
│││││●
││││├─
6 QED │││││C 4
│││├─
4 Cnj ││││A ∧ C 3
││├─
3 CR │││⊥ 2
││
│││B (9)
││├─
│││││●
││││├─
9 QED │││││B 8
││││
│││││●
││││├─
10 QED │││││C 8
│││├─
8 Cnj ││││B ∧ C 7
││├─
7 CR │││⊥ 2
│├─
2 PC ││⊥ 1
├─
1 RAA │¬ C
f.
│A ∧ (B ∨ C) 1
├─
1 Ext │A (5)
1 Ext │B ∨ C 2
│
││B (6)
│├─
│││¬ C
││├─
││││●
│││├─
5 QED ││││A 4
│││
││││●
│││├─
6 QED ││││B 4
││├─
4 Cnj │││A ∧ B 3
│├─
3 PE ││(A ∧ B) ∨ C 2
│
││C (8)
│├─
│││¬ (A ∧ B)
││├─
│││●
││├─
8 QED │││C 7
│├─
7 PE ││(A ∧ B) ∨ C 2
├─
2 PC │(A ∧ B) ∨ C
g.
│A ∨ B 1
│C (5),(9)
├─
││A (4)
│├─
│││¬ (B ∧ C)
││├─
││││●
│││├─
4 QED ││││A 3
│││
││││●
│││├─
5 QED ││││C 3
││├─
3 Cnj │││A ∧ C 2
│├─
2 PE ││(A ∧ C) ∨ (B ∧ C) 1
│
││B (8)
│├─
│││¬ (A ∧ C)
││├─
││││●
│││├─
8 QED ││││B 7
│││
││││●
│││├─
9 QED ││││C 7
││├─
7 Cnj │││B ∧ C 6
│├─
6 PE ││(A ∧ C) ∨ (B ∧ C) 1
├─
1 PC │(A ∧ C) ∨ (B ∧ C)
h.
│A ∨ B 1
│¬ A ∨ C 2
├─
││A (5)
│├─
│││¬ A (5)
││├─
││││¬ B
│││├─
│││││¬ C
││││├─
│││││●
││││├─
5 Nc │││││⊥ 4
│││├─
4 IP ││││C 3
││├─
3 PE │││B ∨ C 2
││
│││C (7)
││├─
││││¬ B
│││├─
││││●
│││├─
7 QED ││││C 6
││├─
6 PE │││B ∨ C 2
│├─
2 PC ││B ∨ C 1
│
││B (9)
│├─
│││¬ C
││├─
│││●
││├─
9 QED │││B 8
│├─
8 PE ││B ∨ C 1
├─
1 PC │B ∨ C
i.
│A (3),(7)
├─
││¬ (A ∧ B) 5
│├─
│││●
││├─
3 QED │││A 2
││
││││B (8)
│││├─
││││││●
│││││├─
7 QED ││││││A 6
│││││
││││││●
│││││├─
8 QED ││││││B 6
││││├─
6 Cnj │││││A ∧ B 5
│││├─
5 CR ││││⊥ 4
││├─
4 RAA │││¬ B 2
│├─
2 Cnj ││A ∧ ¬ B 1
├─
1 PE │(A ∧ B) ∨ (A ∧ ¬ B)
 
│(A ∧ B) ∨ (A ∧ ¬ B) 1
├─
││A ∧ B 2
│├─
2 Ext ││A (3)
2 Ext ││B
││●
│├─
3 QED ││A 1
│
││A ∧ ¬ B 4
│├─
4 Ext ││A (5)
4 Ext ││¬ B
││●
│├─
5 QED ││A 1
├─
1 PC │A
2. a.
│A ∨ A 1
├─
││A (2)
│├─
││●
│├─
2 QED ││A 1
│
││A (3)
│├─
││●
│├─
3 QED ││A 1
├─
1 PC │A
 
│A (2)
├─
││¬ A
│├─
││●
│├─
2 QED ││A 1
├─
1 PE │A ∨ A
b.
│A ∨ B 1
├─
││A (3)
│├─
│││¬ B
││├─
│││●
││├─
3 QED │││A 2
│├─
2 PE ││B ∨ A 1
│
││B
│├─
│││¬ A (5)
││├─
│││●
││├─
5 QED │││B 4
│├─
4 PE ││B ∨ A 1
├─
1 PC │B ∨ A
 
│B ∨ A 2
├─
││¬ A (5)
│├─
│││B (3)
││├─
│││●
││├─
3 QED │││B 2
││
│││A (5)
││├─
││││¬ B
│││├─
││││●
│││├─
5 Nc ││││⊥ 4
││├─
4 IP │││B 2
│├─
2 PC ││B 1
├─
1 PE │A ∨ B
  c.
│(A ∨ B) ∨ C 3
├─
││¬ A (6)
│├─
│││¬ B (8)
││├─
││││A ∨ B 4
│││├─
│││││A (6)
││││├─
││││││¬ C
│││││├─
││││││●
│││││├─
6 Nc ││││││⊥ 5
││││├─
5 IP │││││C 4
││││
│││││B (8)
││││├─
││││││¬ C
│││││├─
││││││●
│││││├─
8 Nc ││││││⊥ 7
││││├─
7 IP │││││C 4
│││├─
4 PC ││││C 3
│││
││││C (9)
│││├─
││││●
│││├─
9 QED ││││C 3
││├─
3 PC │││C 2
│├─
2 PE ││B ∨ C 1
├─
1 PE │A ∨ (B ∨ C)

This is the second of the two derivations needed; the first appears in 4.2.3. In that one, disjunctive resources are exploited before disjunctive goals are planned for while the derivation at the left here illustrates the opposite approach.

  d.
│A ∨ (B ∧ ¬ B) 1
├─
││A (2)
│├─
││●
│├─
2 QED ││A 1
│
││B ∧ ¬ B 3
│├─
3 Ext ││B (5)
3 Ext ││¬ B (5)
││
│││¬ A
││├─
│││●
││├─
5 Nc │││⊥ 4
│├─
4 IP ││A 1
├─
1 PC │A
 
│A (2)
├─
││¬ (B ∧ ¬ B)
│├─
││●
│├─
2 QED ││A 1
├─
1 PE │A ∨ (B ∧ ¬ B)
  e.
│¬ (A ∨ B) 3,7
├─
│││A (5)
││├─
│││││¬ B
││││├─
│││││●
││││├─
5 QED │││││A 4
│││├─
4 PE ││││A ∨ B 3
││├─
3 CR │││⊥ 2
│├─
2 RAA ││¬ A 1
│
│││B (9)
││├─
│││││¬ A
││││├─
│││││●
││││├─
9 QED │││││B 8
│││├─
8 PE ││││A ∨ B 7
││├─
7 CR │││⊥ 6
│├─
6 RAA ││¬ B 1
├─
1 Cnj │¬ A ∧ ¬ B
 
│¬ A ∧ ¬ B 1
├─
1 Ext │¬ A (4)
1 Ext │¬ B (5)
│
││A ∨ B 3
│├─
│││A (4)
││├─
│││●
││├─
4 Nc │││⊥ 3
││
│││B (5)
││├─
│││●
││├─
│││⊥ 3
│├─
3 PC ││⊥ 2
├─
2 RAA │¬ (A ∨ B)
  f.
│¬ (A ∧ B) 3
├─
││A (5)
│├─
│││B (6)
││├─
│││││●
││││├─
5 QED │││││A 4
││││
│││││●
││││├─
6 QED │││││B 4
│││├─
4 Cnj ││││A ∧ B 3
││├─
3 CR │││⊥ 2
│├─
2 RAA ││¬ B 1
├─
1 PE │¬ A ∨ ¬ B
 
│¬ A ∨ ¬ B 3
├─
││A ∧ B 2
│├─
2 Ext ││A (4)
2 Ext ││B (5)
││
│││¬ A (4)
││├─
│││●
││├─
4 Nc │││⊥ 3
││
│││¬ B (5)
││├─
│││●
││├─
5 Nc │││⊥ 3
│├─
3 PC ││⊥ 1
├─
1 RAA │¬ (A ∧ B)
3. a.
│A ∨ B 2
│A
├─
││B
│├─
│││A
││├─
│││○ A, B ⊭ ⊥
││├─
│││⊥ 2
││
│││B
││├─
│││○ A, B ⊭ ⊥
││├─
│││⊥ 2
│├─
2 PC ││⊥ 1
├─
1 RAA │¬ B
ABA∨B,A/¬B
TTⓉⓉⒻ
  b.
│A ∨ (B ∧ C) 3,8
├─
│││¬ A (5)
││├─
││││A (5)
│││├─
│││││¬ B
││││├─
│││││●
││││├─
5 Nc │││││⊥ 4
│││├─
4 IP ││││B 3
│││
││││B ∧ C
│││├─
6 Ext ││││B 7
6 Ext ││││C
││││●
│││├─
7 QED ││││B 3
││├─
3 PC │││B 2
│├─
2 PE ││A ∨ B 1
│
│││A
││├─
││││¬ C
│││├─
││││○ A, ¬ C ⊭ ⊥
│││├─
││││⊥ 9
││├─
9 IP │││C 8
││
│││B ∧ C 10
││├─
10 Ext │││B
10 Ext │││C 11
│││●
││├─
11 QED │││C 8
│├─
8 PC ││C 1
├─
1 Cnj │(A ∨ B) ∧ C
 

Since entailment fails in one direction, equivalence must fail, so a second derivation for entailment in the other direction need not be pursued; but that entailment does hold, as is shown below.

│(A ∨ B) ∧ C 1
├─
1 Ext │A ∨ B 2
1 Ext │C (8)
│
││A (4)
│├─
│││¬ (B ∧ C)
││├─
│││●
││├─
4 QED │││A 3
│├─
3 PE ││A ∨ (B ∧ C) 2
│
││B (7)
│├─
│││¬ A
││├─
││││●
│││├─
7 QED ││││B 6
│││
││││●
│││├─
8 QED ││││C 6
││├─
6 Cnj │││B ∧ C 5
│├─
5 PE ││A ∨ (B ∧ C) 2
├─
2 PC │A ∨ (B ∧ C)

Each of the following divides the one open gap:
ABCA∨(B∧C)/(A∨B)∧C
TTFⓉFTⒻ
TFFⓉFTⒻ
  c.
│¬ (A ∨ B) 3
├─
││A (5)
│├─
│││B
││├─
│││││¬ B
││││├─
│││││●
││││├─
5 QED │││││A 4
│││├─
4 PE ││││A ∨ B 3
││├─
3 CR │││⊥ 2
│├─
2 RAA ││¬ B 1
├─
1 PE │¬ A ∨ ¬ B


The following divide the first and second open gap, respectively:
AB¬A∨¬B/¬(A∨B)
FTTⓉFⒻT
TFFⓉTⒻT
 
│¬ A ∨ ¬ B 2
├─
││A ∨ B 3,5
│├─
│││¬ A (4)
││├─
││││A (4)
│││├─
││││●
│││├─
4 Nc ││││⊥ 3
│││
││││B
│││├─
││││○ ¬ A, B ⊭ ⊥
│││├─
││││⊥ 3
││├─
3 PC │││⊥ 2
││
│││¬ B (6)
││├─
││││A
│││├─
││││○ A, ¬ B ⊭ ⊥
│││├─
││││⊥ 5
│││
││││B (6)
│││├─
││││●
│││├─
6 Nc ││││⊥ 5
││├─
5 PC │││⊥ 2
│├─
2 PC ││⊥ 1
├─
1 RAA │¬ (A ∨ B)
Glen Helman 10 Sep 2011