| |
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 to exploit the conditional introduced at stage 9, and the derivation could then proceed along the lines of stages 13-21 above.
|