|
5.
|
(∀x: Wx) ¬ Gx ≃ ¬ (∀x: Wx) Gx
| │∀x (Wx → ¬ Gx) | a:2 |
| ├─ | |
| ││∀x (Wx → Gx) | a:3 |
| │├─ | |
| 2 UI | ││Wa → ¬ Ga | 4 |
| 3 UI | ││Wa → Ga | 6, 8 |
| ││ | |
| ││││¬ Wa | |
| │││├─ | |
| ││││││¬ Wa | |
| │││││├─ | |
| ││││││○ | ¬ Wa ⊭ ⊥ |
| │││││├─ | |
| ││││││⊥ | 7 |
| ││││├─ | |
| 7 IP | │││││Wa | 6 |
| ││││ | |
| │││││Ga | |
| ││││├─ | |
| │││││○ | ¬ Wa,Ga ⊭ ⊥ |
| ││││├─ | |
| │││││⊥ | 6 |
| │││├─ | |
| 6 RC | ││││⊥ | 5 |
| ││├─ | |
| 5 IP | │││Wa | 4 |
| ││ | |
| │││¬ Ga | (8) |
| ││├─ | |
| 8 MTT | │││¬ Wa | |
| │││○ | ¬ Wa,¬ Ga ⊭ ⊥ |
| ││├─ | |
| │││⊥ | 4 |
| │├─ | |
| 4 RC | ││⊥ | 1 |
| ├─ | |
| 1 RAA | │¬ ∀x (Wx → Gx) | |
|
|
lurks in the 1st and 3rd gaps
lurks in the 1st and 2nd gaps
|