Proofs in Polyadic QL - Solutions
4. (x)~Rxx, (x)(y)(z)((Rxy & Ryz)
⊃
Rxz) // (x)(y)(Rxy
⊃
~Ryx)
| 1. |
(x)~Rxx |
Premise |
|
|
| 2. |
(x)(y)(z)((Rxy & Ryz)
⊃
Rxz) |
Premise |
|
|
| 3. |
flag a |
flag assump, UG |
SP1 |
|
| 4. |
flag b |
flag assump, UG |
SP1 |
SP2 |
| 5. |
~Raa |
U.I. 1 |
SP1 |
SP2 |
| 6. |
(y)(z)((Ray & Ryz)
⊃
Raz) |
U.I. 2 |
SP1 |
SP2 |
| 7. |
(z)((Rab & Rbz)
⊃
Raz) |
U.I. 6 |
SP1 |
SP2 |
| 8. |
((Rab & Rba)
⊃
Raa) |
U.I. 7 |
SP1 |
SP2 |
| 9. |
~(Rab & Rba) |
M.T. 5, 8 |
SP1 |
SP2 |
| 10. |
(~Rab v ~Rba) |
DEM., 9 |
SP1 |
SP2 |
| 11. |
(Rab
⊃
~Rba) |
C.E., 10 |
SP1 |
SP2 |
| 12. |
(y)(Ray
⊃ ~Rya) |
U.G. 4-11 |
SP1 |
|
| 13. |
(x)(y)(Rxy
⊃ ~Ryx) |
U.G. 3-12 |
|
|
|