|
d.
|
(∀x: Px) (∀y: Py) (∀z: Pz ∧ Lzx) Lyz
(∀x:Px) (∀y:Py) (Lxy → (∀z:Pz) (∀w:Pw) Lzw)
| │∀x (Px → ∀y (Py → ∀z ((Pz ∧ Lzx) → Lyz))) | b:10, a:17 |
| ├─ | |
| │ⓐ | |
| │││Pa | (15), (18) |
| ││├─ | |
| │││ⓑ | |
| │││││Pb | (11) |
| ││││├─ | |
| ││││││Lab | (15) |
| │││││├─ | |
| ││││││ⓒ | |
| ││││││││Pc | (20) |
| │││││││├─ | |
| ││││││││ⓓ | |
| ││││││││││Pd | (13), (22) |
| │││││││││├─ | |
10 UI | ││││││││││Pb → ∀y (Py → ∀z ((Pz ∧ Lzb) → Lyz)) | 10 |
11 MPP | ││││││││││∀y (Py → ∀z ((Pz ∧ Lzb) → Lyz)) | d:12 |
12 UI | ││││││││││Pd → ∀z ((Pz ∧ Lzb) → Ldz) | 13 |
13 MPP | ││││││││││∀z ((Pz ∧ Lzb) → Ldz) | a:14 |
14 UI | ││││││││││(Pa ∧ Lab) → Lda | 16 |
15 Adj | ││││││││││Pa ∧ Lab | X, (16) |
16 MPP | ││││││││││Lda | (22) |
17 UI | ││││││││││Pa → ∀y (Py → ∀z ((Pz ∧ Lza) → Lyz)) | 18 |
18 MPP | ││││││││││∀y (Py → ∀z ((Pz ∧ Lza) → Lyz)) | c:19 |
19 UI | ││││││││││Pc → ∀z ((Pz ∧ Lza) → Lcz) | 20 |
20 MPP | ││││││││││∀z ((Pz ∧ Lza) → Lcz) | d:21 |
21 UI | ││││││││││(Pd ∧ Lda) → Lcd) | 23 |
22 Adj | ││││││││││Pd ∧ Lda | X, (23) |
23 MPP | ││││││││││Lcd | (24) |
| ││││││││││● | |
| │││││││││├─ | |
24 QED | ││││││││││Lcd | 9 |
| ││││││││├─ | |
9 CP | │││││││││Pd → Lcd | 8 |
| │││││││├─ | |
8 UG | ││││││││∀w (Pw → Lcw) | 7 |
| ││││││├─ | |
7 CP | │││││││Pc → ∀w (Pw → Lcw)) | 6 |
| │││││├─ | |
6 UG | ││││││∀z (Pz → ∀w (Pw → Lzw)) | 5 |
| ││││├─ | |
5 CP | │││││Lab → ∀z (Pz → ∀w (Pw → Lzw)) | 4 |
| │││├─ | |
4 CP | ││││Pb → (Lab → ∀z (Pz → ∀w (Pw → Lzw))) | 3 |
| ││├─ | |
3 UG | │││∀y (Py → (Lay → ∀z (Pz → ∀w (Pw → Lzw)))) | 2 |
| │├─ | |
2 CP | ││Pa → ∀y (Py → (Lay → ∀z (Pz → ∀w (Pw → Lzw)))) | 1 |
| ├─ | |
1 UG | │∀x (Px → ∀y (Py → (Lxy → ∀z (Pz → ∀w (Pw → Lzw))))) | |
It would be easy to get lost in this argument, but the basic structure has just three parts: planning what must be shown (stages 1-9) and then applying the premise twice (stages 10-16 and 17-23) to take us first from Lab to Lda and then from Lda to Lcd. After stage 9, we have Lcd as the goal and Lab among the resources, and we also know that a, b, c, and d are all people. The premise tells us that anyone who loves is loved by everyone. It will then follow from Lab that the predicate [L _ a] is true of everyone, and it will follow from any predication of [Ld _ ] of a person that Lcd. Since Lda is both [L _ a]d and [Ld _ ]a, it can link the two applications of the premise.
|