8.5.xa. Exercise answers

1. Some of the derivations below are given in two forms, one that does not use EG and another that does.
  a.
│∃x Fx 1
│∀x (Fx → Gx) a:2
├─
│ⓐ
││Fa (3)
│├─
2 UI ││Fa → Ga 3
3 MPP ││Ga
│││∀x ¬ Gx a:5
││├─
5 UI │││¬ Ga (6)
│││●
││├─
6 Nc │││⊥
│├─
4 NcP ││∃x Gx 1
├─
1 PCh │∃x Gx
│∃x Fx 1
│∀x (Fx → Gx) a:2
├─
│ⓐ
││Fa (3)
│├─
2 UI ││Fa → Ga 3
3 MPP ││Ga (4)
4 EG ││∃x Gx X, (5)
││●
│├─
5 QED ││∃x Gx 1
├─
1 PCh │∃x Gx
  b.
│∃x (Fx ∧ Gx) 1
│∀x (Gx → Hx) a:3
├─
│ⓐ
││Fa ∧ Ga 2
│├─
2 Ext ││Fa (7)
2 Ext ││Ga (4)
3 UI ││Ga → Ha 4
4 MPP ││Ha (8)
││
│││∀x ¬ (Fx ∧ Hx) a:6
││├─
6 UI │││¬ (Fa ∧ Ha) 7
7 MPT │││¬ Ha (8)
│││●
││├─
8 Nc │││⊥ 5
│├─
5 NcP ││∃x (Fx ∧ Hx) 1
├─
1 PCh │∃x (Fx ∧ Hx)
 
│∃x (Fx ∧ Gx) 1
│∀x (Gx → Hx) a:3
├─
│ⓐ
││Fa ∧ Ga 2
│├─
2 Ext ││Fa (5)
2 Ext ││Ga (4)
3 UI ││Ga → Ha 4
4 MPP ││Ha (5)
5 Adj ││Fa ∧ Ha X, (6)
6 EG ││∃x (Fx ∧ Hx) X, (7)
││●
│├─
7 QED ││∃x (Fx ∧ Hx) 1
├─
1 PCh │∃x (Fx ∧ Hx)
  c.
│∀x (Fx → Ga) b:3
├─
││∃x Fx 2
│├─
││ⓑ
│││Fb (4)
││├─
3 UI │││Fb → Ga 4
4 MPP │││Ga (5)
│││●
││├─
5 QED │││Ga 2
│├─
2 PCh ││Ga 1
├─
1 CP │∃x Fx → Ga
   
│∃x Fx → Ga 4
├─
│ⓑ
│││Fb (8)
││├─
││││¬ Ga (4)
│││├─
4 MTT ││││¬ ∃x Fx 5
││││
││││││∀x ¬ Fx b:7
│││││├─
7 UI ││││││¬ Fb (8)
││││││●
│││││├─
8 Nc ││││││⊥ 6
││││├─
6 NcP │││││∃x Fx 5
│││├─
5 CR ││││⊥ 3
││├─
3 IP │││Ga 2
│├─
2 CP ││Fb→Ga 1
├─
1 UG │∀x (Fx → Ga)
│∃x Fx → Ga 4
├─
│ⓑ
│││Fb (3)
││├─
3 EG │││∃x Fx X, (4)
4 MPP │││Ga (5)
│││●
││├─
5 QED │││Ga 2
│├─
2 CP ││Fb → Ga 1
├─
1 UG │∀x (Fx → Ga)
  d.
│Fa (3)
├─
││∀x ¬ (x = a ∧ Fx) a:2
│├─
2 UI ││¬ (a = a ∧ Fa) 3
3 MPT ││¬ a = a (4)
││●
│├─
4 DC ││⊥ 1
├─
1 NcP │∃x (x = a ∧ Fx)
 
│Fa (2)
├─
1 EC │a = a X, (2)
2 Adj │a = a ∧ Fa X, (3)
3 EG │∃x (x = a ∧ Fx) X, (4)
│●
├─
4 QED │∃x (x = a ∧ Fx)
   
│∃x (x = a ∧ Fx) 1
├─
│ⓑ
││b = a ∧ Fb 2
│├─
2 Ext ││b = a a—b
2 Ext ││Fb (3)
││●
│├─
3 QED= ││Fa 1
├─
1 PCh │Fa
  e.
│∃x (Fx ∧ ∀y Rxy) 2
├─
│ⓐ
││ⓑ
│││Fb ∧ ∀y Rby 3
││├─
3 Ext │││Fb (6)
3 Ext │││∀y Rby a:7
│││
││││∀y ¬ (Fy ∧ Rya) b:5
│││├─
5 UI ││││¬ (Fb ∧ Rba) 6
6 MPT ││││¬ Rba (8)
7 UI ││││Rba (8)
││││●
│││├─
8 Nc ││││⊥ 4
││├─
4 NcP │││∃y (Fy ∧ Rya) 2
│├─
2 PCh ││∃y (Fy ∧ Rya) 1
├─
1 UG │∀x ∃y (Fy ∧ Ryx)
 
│∃x (Fx ∧ ∀y Rxy) 2
├─
│ⓐ
││ⓑ
│││Fb ∧ ∀y Rby 3
││├─
3 Ext │││Fb (5)
3 Ext │││∀y Rby a:4
4 UI │││Rba (5)
5 Adj │││Fb ∧ Rba X, (6)
6 EG │││∃y (Fy ∧ Rya) X, (7)
│││●
││├─
7 QED │││∃y (Fy ∧ Rya) 2
│├─
2 PCh ││∃y (Fy ∧ Rya) 1
├─
1 UG │∀x ∃y (Fy ∧ Ryx)
  f.
│∃x (Gx ∧ Fx) 1
│¬ Fa (6)
├─
│ⓑ
││Gb ∧ Fb 2
│├─
2 Ext ││Gb (5)
2 Ext ││Fb (6)
││
│││∀x ¬ (¬ x = a ∧ Gx) b:4
││├─
4 UI │││¬ (¬ b = a ∧ Gb) 5
5 MPT │││b = a a—b
│││●
││├─
6 Nc= │││⊥ 3
│├─
3 NcP ││∃x (¬ x = a ∧ Gx) 1
├─
1 PCh │∃x (¬ x = a ∧ Gx)
  g.
│∀x (Fx → Ga) c:3
│∀x (Ga → Fx) b:5
│∃x Fx 2
├─
│ⓑ
││ⓒ
│││Fc (4)
││├─
3 UI │││Fc → Ga 4
4 MPP │││Ga (6)
5 UI │││Ga → Fb 6
6 MPP │││Fb (7)
│││●
││├─
7 QED │││Fb 2
│├─
2 PCh ││Fb 1
├─
1 UG │∀x Fx
  h.
(∀x: Px) (∀y: Py ∧ (∃z: Pz) Lyz) Lxy
(∃x: Px) (∃y: Py) Lxy
(∀x: Px) (∀y: Py) Lxy
│∀x (Px → ∀y ((Py ∧ ∃z (Pz ∧ Lyz)) → Lxy)) b:7, a:14
│∃x (Px ∧ ∃y (Py ∧ Lxy)) 5
├─
│ⓐ
│││Pa (15)
││├─
│││ⓑ
│││││Pb (8), (19)
││││├─
│││││ⓒ
││││││Pc ∧ ∃y (Py ∧ Lcy) 6
│││││├─
6 Ext ││││││Pc (12), (17)
6 Ext ││││││∃y (Py ∧ Lcy) 10
7 UI ││││││Pb → ∀y ((Py ∧ ∃z (Pz ∧ Lyz)) → Lby) 8
8 MPP ││││││∀y ((Py ∧ ∃z (Pz ∧ Lyz)) → Lby) c:9
9 UI ││││││(Pc ∧ ∃z (Pz ∧ Lcz)) → Lbc 13
││││││
││││││ⓓ
│││││││Pd ∧ Lcd (11)
││││││├─
11 EG │││││││∃z (Pz ∧ Lcz) X, (12)
12 Adj │││││││Pc ∧ ∃z (Pz ∧ Lcz) X, (13)
13 MPP │││││││Lbc (17)
14 UI │││││││Pa → ∀y ((Py ∧ ∃z (Pz ∧ Lyz)) → Lay) 15
15 MPP │││││││∀y ((Py ∧ ∃z (Pz ∧ Lyz)) → Lay) b:16
16 UI │││││││(Pb ∧ ∃z (Pz ∧ Lyz)) → Lab 20
17 Adj │││││││Pc ∧ Lbc X, (18)
18 EG │││││││∃z (Pz ∧ Lbz) X, (19)
19 Adj │││││││Pb ∧ ∃z (Pz ∧ Lbz) X, (20)
20 MPP │││││││Lab (21)
│││││││●
││││││├─
21 QED │││││││Lab 10
│││││├─
10 PCh ││││││Lab 5
││││├─
5 PCh │││││Lab 4
│││├─
4 CP ││││Pb → Lab 3
││├─
3 UG │││∀y (Py → Lay) 2
│├─
2 CP ││Pa → ∀y (Py → Lay) 1
├─
1 UG │∀x (Px → ∀y (Py → Lxy))

Note that stages 10 and 11 serve only to move us from ∃y (Py ∧ Lcy) to ∃z (Pz ∧ Lcz)—i.e., to change a bound variable. If sentences that differ only in the choice of a letter for a bound variable are regarded as the same (or if a different variable had been chosen when analyzing the second premise), the assumption Pc ∧ ∃y (Py ∧ Lcy) could be used as a premise for MPP and stages 10-12 would not be needed.

  i. ∃x ¬ (∃y: ¬ y = x) Dy ≃ ¬ ∃x (∃y: ¬ y = x) (Dx ∧ Dy)
│∃x ¬ ∃y (¬ y = x ∧ Dy) 2
├─
││∃x ∃y (¬ y = x ∧ (Dx ∧ Dy)) 3
│├─
││ⓐ
│││¬ ∃y (¬ y = a ∧ Dy) 7
││├─
│││ⓑ
││││∃y (¬ y = b ∧ (Db ∧ Dy)) 4
│││├─
││││ⓒ
│││││¬ c = b ∧ (Db ∧ Dc) 5
││││├─
5 Ext │││││¬ c = b (13)
5 Ext │││││Db ∧ Dc 6
6 Ext │││││Db (10)
6 Ext │││││Dc (12)
│││││
│││││││∀y ¬ (¬ y = a ∧ Dy) b:9, c:11
││││││├─
9 UI │││││││¬ (¬ b = a ∧ Db) 10
10 MPT │││││││b = a a—b, c
11 UI │││││││¬ (¬ c = a ∧ Dc) 12
12 MPT │││││││c = a a—b—c
│││││││●
││││││├─
13 DC │││││││⊥ 8
│││││├─
8 NcP ││││││∃y (¬ y = a ∧ Dy) 7
││││├─
7 CR │││││⊥ 4
│││├─
4 PCh ││││⊥ 3
││├─
3 PCh │││⊥ 2
│├─
2 PCh ││⊥ 1
├─
1 RAA │¬ ∃x ∃y (¬ y = x ∧ (Dx ∧ Dy))
   
│¬ ∃x ∃y (¬ y = x ∧ (Dx ∧ Dy)) (12)
├─
││∀x ∃y (¬ y = x ∧ Dy) a:2, b:5
│├─
2 UI ││∃y (¬ y = a ∧ Dy) 3
││
││ⓑ
│││¬ b = a ∧ Db 4
││├─
4 Ext │││¬ b = a
4 Ext │││Db (8)
5 UI │││∃y (¬ y = b ∧ Dy) 6
│││
│││ⓒ
││││¬ c = b ∧ Dc 7
│││├─
7 Ext ││││¬ c = b (9)
7 Ext ││││Dc (8)
8 Adj ││││Db ∧ Dc X, (9)
9 Adj ││││¬ c = b ∧ (Db ∧ Dc) X, (10)
10 EG ││││∃y (¬ y = b ∧ (Db ∧ Dy)) X, (11)
11 EG ││││∃x ∃y (¬ y = x ∧ (Dx ∧ Dy)) X, (12)
││││●
│││├─
12 Nc ││││⊥ 6
││├─
6 PCh │││⊥ 3
│├─
3 PCh ││⊥ 1
├─
1 NcP │∃x ¬ ∃y (¬ y = x ∧ Dy)
2. a.
│∃x Fx 1
│∃x Gx 2
├─
│ⓐ
││Fa (5)
│├─
││ⓑ
│││Gb (7)
││├─
││││∀x ¬ (Fx ∧ Gx) a:4, b:6
│││├─
4 UI ││││¬ (Fa ∧ Ga) 5
5 MPT ││││¬ Ga
6 UI ││││¬ (Fb ∧ Gb) 7
7 MPT ││││¬ Fb
││││○ Fa,¬ Fb,¬ Ga,Gb ⊭ ⊥
│││├─
││││⊥ 3
││├─
3 NcP │││∃x (Fx ∧ Gx) 2
│├─
2 PCh ││∃x (Fx ∧ Gx) 1
├─
1 PCh │∃x (Fx ∧ Gx)
  b.
│∃x (Fx ∧ Gx) 1
│∃x (Fx ∧ Hx) 3
│∀x (Fx → ∀y (Fy → x = y)) a:3
├─
│ⓐ
││Fa ∧ Ga 2
│├─
2 Ext ││Fa (6)
2 Ext ││Ga (11)
││
││ⓑ
│││Fb ∧ Hb 4
││├─
4 Ext │││Fb (8)
4 Ext │││Hb (12)
5 UI │││Fa → ∀y (Fy → a = y) 6
6 MPP │││∀y (Fy → a = y) b:7
7 UI │││Fb → a = b 8
8 MPP │││a = b a—b
│││
││││∀x ¬ (Gx ∧ Hx) a:10
│││├─
10 UI ││││¬ (Ga ∧ Ha) 11
11 MPT ││││¬ Ha (12)
││││●
│││├─
12 Nc= ││││⊥ 9
││├─
9 NcP │││∃x (Gx ∧ Hx) 3
│├─
3 PCh ││∃x (Gx ∧ Hx) 1
├─
1 PCh │∃x (Gx ∧ Hx)
3. a.
(∃x: Sx) Cx, (∀x: Sx) Tx, ∀x (Cx → Px) / (∃x: Tx) Px
│∃x (Sx ∧ Cx) 1
│∀x (Sx → Tx) a:3
│∀x (Cx → Px) a:5
├─
│ⓐ
││Sa ∧ Ca 2
│├─
2 Ext ││Sa (4)
2 Ext ││Ca (6)
3 UI ││Sa → Ta 4
4 MPP ││Ta (7)
5 UI ││Ca → Pa 6
6 MPP ││Pa (7)
7 Adj ││Ta ∧ Pa X, (8)
8 EG ││∃x (Tx ∧ Px) X, (9)
││●
│├─
9 QED ││∃x (Tx ∧ Px) 1
├─
1 PCh │∃x (Tx ∧ Px)
  b.
(∃x: Px ∧ (∃y: Sy) Oxy) Dx
(∀x: Sx) Rx
(∃x: Px ∧ (∃y: Ry) Oxy) Dx
│∃x ((Px ∧ ∃y (Sy ∧ Oxy)) ∧ Dx) 1
│∀x (Sx → Rx) b:6
├─
│ⓐ
││(Pa ∧ ∃y (Sy ∧ Oay)) ∧ Da 2
│├─
2 Ext ││Pa ∧ ∃y (Sy ∧ Oay) 3
2 Ext ││Da (11)
3 Ext ││Pa (10)
3 Ext ││∃y (Sy ∧ Oay) 3
││
││ⓑ
│││Sb ∧ Oab 5
││├─
5 Ext │││Sb (7)
5 Ext │││Oab (8)
6 UI │││Sb → Rb 7
7 MPP │││Rb (8)
8 Adj │││Rb ∧ Oab X, (9)
9 EG │││∃y (Ry ∧ Oay) X, (10)
10 Adj │││Pa ∧ ∃y (Ry ∧ Oay) X, (11)
11 Adj │││(Pa ∧ ∃y (Ry ∧ Oay)) ∧ Da X, (12)
12 EG │││∃x ((Px ∧ ∃y (Ry ∧ Oxy)) ∧ Dx) X, (13)
│││●
││├─
13 QED │││∃x ((Px ∧ ∃y (Ry ∧ Oxy)) ∧ Dx) 4
│├─
4 PCh ││∃x ((Px ∧ ∃y (Ry ∧ Oxy)) ∧ Dx) 1
├─
1 PCh │∃x ((Px ∧ ∃y (Ry ∧ Oxy)) ∧ Dx)
Glen Helman 20 Jul 2012