Solutions to Proving Theorems in QL
Proof 1
| 1. | (x)(Ax ⊃ Bx) | assump., CP | sp1 |
| 2. | (∃x)~Bx | assump., CP | sp1, sp2 |
| 3. | ~Ba | E.I., 2, flag a | sp1, sp2 |
| 4. | Aa ⊃ Ba | U.I., 1 | sp1, sp2 |
| 5. | ~Aa | M.T. 3, 4 | sp1, sp2 |
| 6. | (∃x)~Ax | E.G. 5 | sp1, sp2 |
| 7. | (∃x)~Bx ⊃ (∃x)~Ax | C.P., 2 -6 | sp1 |
| 8. | (x)(Ax ⊃ Bx) ⊃ ((∃x)~Bx ⊃ (∃x)~Ax) | C.P., 1-7 |