8.6.xa. Exercise answers

1.
│(∃x: Wx ∧ (∀y: ¬ y = x) ¬ Wy) Ax 1
├─
│ⓐ
││Wa ∧ (∀y: ¬ y = a) ¬ Wy 2
││Aa (3)
│├─
2 Ext ││Wa (3)
2 Ext ││(∀y: ¬ y = a) ¬ Wy
3 REG ││(∃x: Ax) Wx X, (4)
││●
│├─
4 QED ││(∃x: Ax) Wx 1
├─
1 PRCh │(∃x: Ax) Wx
  Ix Wx: 3
│A(Ix Wx) (2)
├─
││(∀x: Ax) ¬ Wx Ix Wx:2
│├─
2 SB ││¬ W(Ix Wx)
││
││ⓐ
│││Wa
│││(∀x: Wx) a = x
│││Ix Wx = a (IxWx)—a, ∗
││├─
│││●
││├─
3 Nc= │││⊥
││
│││(∀x: Wx) (∃y: Wy) ¬ x = y   ∗:4
│││Ix Wx = ∗
││├─
│││││¬ W∗
││││├─
│││││○ A(Ix Wx),¬ W(Ix Wx),
││││├─     ¬ W∗,(IxWx)=∗ ⇏ ⊥
│││││⊥ 5
│││├─
5 IP ││││W∗ 4
│││
││││(∃y: Wy) ¬ ∗ = y
│││├─
││││(unfinished)
│││├─
││││⊥ 4
││├─
4 MCR │││⊥
│├─
3 SD ││⊥ 1
├─
1 PRCh │(∃x: Ax) Wx



2.
│(∃x: Ax) Wx 1
│¬ ∃x (∃y: ¬ y = x) (Wx ∧ Wy) (11)
├─
│ⓐ
││Aa (3)
││Wa (4), (8)
│├─
│││(∀x: Wx ∧ (∀y: ¬ y = x) ¬ Wy) ¬ Ax a:3
││├─
3 SC │││¬ ((Wa ∧ (∀y: ¬ y = a) ¬ Wy)) 4
4 MPT │││¬ (∀y: ¬ y = a) ¬ Wy 5
│││
││││ⓑ
│││││¬ b = a (9)
││││├─
││││││Wb (8)
│││││├─ (9)
8 Adj ││││││Wa ∧ Wb X
9 REG ││││││(∃y: ¬ y = a) (Wa ∧ Wy) X, (10)
10 EG ││││││∃x (∃y: ¬ y = x) (Wx ∧ Wy) X, (11)
││││││●
│││││├─
11 Nc ││││││⊥ 7
││││├─
7 RAA │││││¬ Wb 6
│││├─
6 RUG ││││(∀y: ¬ y = a) ¬ Wy 5
││├─
5 CR │││⊥ 2
│├─
2 RNcP ││(∃x: Wx ∧ (∀y: ¬ y = x) ¬ Wy) Ax 1
├─
1 PRCh │(∃x: Wx ∧ (∀y: ¬ y = x) ¬ Wy) Ax
  Ix Wx: 2
│(∃x: Ax) Wx 1
│¬ ∃x (∃y: ¬ y = x) (Wx ∧ Wy) (11)
├─
│ⓐ
││Aa (4), (5)
││Wa (3), (8)
│├─
││ⓑ
│││Wb
│││(∀y: Wy) b = y a:3
│││Ix Wx = b a, b—IxWx, ∗
││├─
3 SB │││b = a a—b—(IxWx), ∗
│││●
││├─
4 QED= │││A(Ix Wx) 2
││
│││(∀x: Wx) (∃y: Wy) ¬ x = y a:5
│││Ix Wx = ∗ a, c, (IxWx)—∗
││├─
5 SB │││(∃y: Wy) ¬ a = y 6
│││
│││ⓒ
││││Wc (8)
││││¬ a = c (9)
│││├─
│││││¬ A(Ix Wx)
││││├─
8 Adj │││││Wc ∧ Wa X, (9)
9 REG │││││(∃y: ¬ y = c) (Wc ∧ Wy) X, (10)
10 EG │││││∃x (∃y: ¬ y = x) (Wx ∧ Wy) X, (11)
│││││●
││││├─
11 Nc │││││⊥
│││├─
7 UP ││││A(Ix Wx) 6
││├─
6 PRCh │││A(Ix Wx) 2
│├─
2 SD ││A(Ix Wx) 1
├─
1 PRCh │A(Ix Wx)
Glen Helman 03 Dec 2004