2.
|
| │∀x ¬ ∀y Rxy | a:2, b:8 |
| ├─ | |
| ││∀x Rxa | a:3, b:9 |
| │├─ | |
2 UI | ││¬ ∀y Ray | 4 |
3 UI | ││Raa | (6) |
| ││ | |
| ││││● | |
| │││├─ | |
6 QED | ││││Raa | 5 |
| │││ | |
| │││ⓑ | |
| │││││¬ Rab | |
| ││││├─ | |
8 UI | │││││¬ ∀y Rby | 10 |
9 UI | │││││Rba | (12) |
| │││││ | |
| │││││││● | |
| ││││││├─ | |
12 QED | │││││││Rba | 11 |
| ││││││ | |
| ││││││││¬ Rbb | |
| │││││││├─ | |
| ││││││││○ | Raa,¬ Rab,Rba,¬ Rbb ⊭ ⊥ |
| │││││││├─ | |
| ││││││││⊥ | 13 |
| ││││││├─ | |
13 IP | │││││││Rbb | 11 |
| ││││││ | |
| ││││││ⓒ | |
| │││││││(unfinished) | |
| ││││││├─ | |
| │││││││Rbc | 11 |
| │││││├─ | |
11 UG+ | ││││││∀y Rby | 10 |
| ││││├─ | |
10 CR | │││││⊥ | 7 |
| │││├─ | |
7 IP | ││││Rab | 5 |
| ││├─ | |
5 UG+ | │││∀y Ray | 4 |
| │├─ | |
4 CR | ││⊥ | 1 |
| ├─ | |
1 RAA | │¬ ∀x Rxa | |
|