Proofs in Polyadic QL - Solutions
3. (x)(y)(Rxy ⊃ ~Ryx) /// (x)~Rxx
Proof:
| 1. | (x)(y)(Rxy ⊃ ~Ryx) | premise | |
| 2. | flag a | flagging assump., U.G. | sp1 |
| 3. | (y)(Ray ⊃ ~Rya) | U.I., 1 | sp1 |
| 4. | (Raa ⊃ ~Raa) | U.I. 3 | sp1 |
| 5. | ~Raa v ~Raa | C.E., 4 | sp1 |
| 6. | ~Raa | rep, 5 | sp1 |
| 7. | (x)~Rxx | U.G. 2-6 |