Proofs in Polyadic QL
Solution 5
5. (x)(y)(Fxy ≡ (Gx & ~Gy)), (∃x)(∃y)(Fxy & Fyx) // (∃x)(Gx & ~Gx)
| 1. | (x)(y)(Fxy ≡ (Gx & ~Gy)) | Prem. | ||
| 2. | (∃x)(∃y)(Fxy & Fyx) | Prem. | ||
| 3. | (∃y)(Fay & Fya) | E.I., 2 flag a | ||
| 4. | Fab & Fba | E.I. 3, flag b | ||
| 5. | (y)(Fay ≡ (Ga & ~Gy)) | U.I., 1 | ||
| 6. | Fab ≡ (Ga & ~Gb) | U.I. 5 | ||
| 7. | [Fab ⊃ (Ga & ~Gb)] & [(Ga & ~Gb) ⊃ Fab] | B.E. 6 | ||
| 8. | [Fab ⊃ (Ga & ~Gb)] | Simp. 7 | ||
| 9. | Fab | Simp. 4 | ||
| 10. | (Ga & ~Gb) | M.P. 8, 9 | ||
| 11. | Ga | Simp. 10 | ||
| 12. | (y)(Fby ≡ (Gb & ~Gy)) | U.I. 1 | ||
| 13. | (Fba ≡ (Gb & ~Ga)) | U.I. 12 | ||
| 14. | [Fba ⊃ (Gb & ~Ga)] & [(Gb & ~Ga) ⊃ Fba] | B.E. 13 | ||
| 15. | [Fba ⊃ (Gb & ~Ga)] | Simp. 14 | ||
| 16. | Fba | Simp. 4 | ||
| 17. | (Gb & ~Ga) | M.P. 15, 16 | ||
| 18. | ~Ga | Simp. 17 | ||
| 19 | Ga & ~Ga | Conj. 11, 18 | ||
| 20. | (∃x)(Gx & ~Gx) | E.G. 19 | ||
| . |
| table of contents | List of Exercises |