Proofs in Polyadic QL - Solutions
1. (∃x)(Ax & ~(∃y)(By & Lxy)), (x)(Ex ⊃ Bx) // (∃x)(Ax & (y)(Ey ⊃ ~Lxy))
Proof:
| 1. | (∃x)(Ax & ~(∃y)(By & Lxy)) | premise | |
| 2. | (x)(Ex ⊃ Bx) | premise | |
| 3. | Aa & ~(∃y)(By & Lay) | E.I., flag a | |
| 4. | ~(∃y)(By & Lay) | simp, 3 | |
| 5. | (y)~(By & Lay) | Q.N.R., 4 | |
| 6. | Aa | Simp, 3 | |
| 7. | flag b | flagged subproof for U.G. | sp1 |
| 8. | Eb ⊃ Bb | U. I., 2 | sp1 |
| 9. | ~(Bb & Lab) | U.I. 5 | sp1 |
| 10. | ~Bb v ~Lab | DeM., 9 | sp1 |
| 11. | Bb ⊃ ~Lab | C.E., 10 | sp1 |
| 12. | Eb ⊃ ~Lab | H.S., 8, 11 | sp1 |
| 13. | (y)(Ey ⊃ ~Lay) | U.G., 7-12 | |
| 14. | Aa & (y)(Ey ⊃ ~Lay) | Conj., 6,13 | |
| 15. | (∃x)(Ax & (y)(Ey ⊃ ~Lxy)) | E.G., 14 |