8.6.xa. Exercise answers

1.
│∃x ((Wx ∧ ∀y (¬ y = x → ¬ Wy)) ∧ Ax) 1
├─
│ⓐ
││(Wa ∧ ∀y (¬ y = a → ¬ Wy)) ∧ Aa 2
│├─
2 Ext ││Wa ∧ ∀y (¬ y = a → ¬ Wy) 3
2 Ext ││Aa (4)
3 Ext ││Wa (4)
3 Ext ││∀y (¬ y = a → ¬ Wy)
4 Adj ││Aa ∧ Wa X, (5)
5 EG ││∃x (Ax ∧ Wx) X, (6)
││●
│├─
6 QED ││∃x (Ax ∧ Wx) 1
├─
1 PCh │∃x (Ax ∧ Wx)
 

Ix Wx: 3

│A(Ix Wx) (3)
├─
││∀x ¬ (Ax ∧ Wx) Ix Wx:2
│├─
2 UI ││¬ (A(Ix Wx) ∧ W(Ix Wx)) 3
3 MPT ││¬ W(Ix Wx) (5)
││
││ⓐ
│││Wa (5)
│││∀x (Wx → a = x)
│││Ix Wx = a IxWx—a, ∗
││├─
│││●
││├─
5 Nc= │││⊥ 4
││
│││∀x (Wx → ∃y (Wy ∧ ¬ x = y)) ∗:6
│││Ix Wx = ∗ IxWx—∗
││├─
6 UI │││W∗ → ∃y (Wy ∧ ¬ ∗ = y)) 7
│││
│││││¬ W∗
││││├─
│││││○ A(Ix Wx),¬ W(Ix Wx),
││││├─     ¬ W∗,(IxWx)=∗ ⊭ ⊥
│││││⊥ 8
│││├─
8 IP ││││W∗ 7
│││
││││∃y (Wy ∧ ¬ ∗ = y)
│││├─
││││(unfinished)
│││├─
││││⊥ 7
││├─
7 RC │││⊥ 4
│├─
4 SD ││⊥ 1
├─
1 NcP │∃x (Ax ∧ Wx)
 
2.
│∃x (Ax ∧ Wx) 1
│¬ ∃x ∃y (¬ y = x ∧ (Wx ∧ Wy)) (15)
├─
│ⓐ
││Aa ∧ Wa 2
│├─
2 Ext ││Aa (5)
2 Ext ││Wa (6), (11)
││
│││∀x ¬ ((Wx ∧ ∀y (¬ y = x → ¬ Wy)) ∧ Ax) a:4
││├─
4 UI │││¬ ((Wa ∧ ∀y (¬ y = a → ¬ Wy)) ∧ Aa) 5
5 MPT │││¬ (Wa ∧ ∀y (¬ y = a → ¬ Wy)) 6
6 MPT │││¬ ∀y (¬ y = a → ¬ Wy) 7
│││
││││ⓑ
││││││¬ b = a (12)
│││││├─
│││││││Wb (11)
││││││├─
11 Adj │││││││Wa ∧ Wb X, (12)
12 Adj │││││││¬ b = a ∧ (Wa ∧ Wb) X, (13)
13 EG │││││││∃y (¬ y = a ∧ (Wa ∧ Wy)) X, (14)
14 EG │││││││∃x ∃y (¬ y = x ∧ (Wx ∧ Wy)) X, (15)
│││││││●
││││││├─
15 Nc │││││││⊥ 10
│││││├─
10 RAA ││││││¬ Wb 9
││││├─
9 CP │││││¬ b = a → ¬ Wb 8
│││├─
8 UG ││││∀y (¬ y = a → ¬ Wy) 7
││├─
7 CR │││⊥ 3
│├─
3 NcP ││∃x ((Wx ∧ ∀y (¬ y = x → ¬ Wy)) ∧ Ax) 1
├─
1 PCh │∃x ((Wx ∧ ∀y (¬ y = x → ¬ Wy)) ∧ Ax)
 

Ix Wx: 2

│∃x (Ax ∧ Wx) 1
│¬ ∃x ∃y (¬ y = x ∧ (Wx ∧ Wy)) (16)
├─
│ⓐ
││Aa ∧ Wa 2
│├─
2 Ext ││Aa (6)
2 Ext ││Wa (5), (8), (12)
││
││ⓑ
│││Wb
│││∀y (Wy → b = y) a:4
│││Ix Wx = b a, b—IxWx, ∗
││├─
4 UI │││Wa → b = a 5
5 MPP │││b = a a—b—IxWx, ∗
│││●
││├─
6 QED= │││A(Ix Wx) 3
││
│││∀x (Wx → ∃y (Wy ∧ ¬ x = y)) a:7
│││Ix Wx = ∗ a, c, IxWx—∗
││├─
7 UI │││Wa → ∃y (Wy ∧ ¬ a = y) 8
8 MPP │││∃y (Wy ∧ ¬ a = y) 9
│││
│││ⓒ
││││Wc ∧ ¬ a = c 10
│││├─
10 Ext ││││Wc (12)
10 Ext ││││¬ a = c (13)
││││
│││││¬ A(Ix Wx)
││││├─
12 Adj │││││Wc ∧ Wa X, (13)
13 Adj │││││¬ a = c ∧ (Wc ∧ Wa) X, (14)
14 EG │││││∃y (¬ y = c ∧ (Wc ∧ Wy)) X, (15)
15 EG │││││∃x ∃y (¬ y = x ∧ (Wx ∧ Wy)) X, (16)
│││││●
││││├─
16 Nc │││││⊥ 11
│││├─
11 IP ││││A(Ix Wx) 9
││├─
9 PCh │││A(Ix Wx) 3
│├─
3 SD ││A(Ix Wx) 1
├─
1 PCh │A(Ix Wx)
Glen Helman 20 Jul 2012