Proofs in Polyadic QL - Solutions
7. (x)((Tx & Sx) ⊃ Lax), (∃x)~(~Tx v ~Sx) // (∃x)Lax
Proof:
| 1. | (x)((Tx & Sx) ⊃ Lax) | premise | |
| 2. | (∃x)~(~Tx v ~Sx) | premise | |
| 3. | ~(~Tb v ~Sb) | E.I., 2, flag b | |
| 4. | (Tb & Sb) ⊃ Lab) | U.I., 1 | |
| 5. | ~~Tb & ~~Sb | DEM, 3 | |
| 6. | Tb & ~~Sb | D.N., 5 | |
| 7. | Tb & Sb | D.N. 6 | |
| 8. | Lab | M.P., 4, 7 | |
| 9. | (∃x)Lax | E.G., 8 |