Proofs in Polyadic QL - Solutions
(∃x)(∃y)(∃z)((Axy &Ayz) ⊃ Axz)
Proof:
| 1. | ~(∃x)(∃y)(∃z)((Axy &Ayz) ⊃ Axz) | assump., I.P | sp1 |
| 2. | (x)~(∃y)(∃z)((Axy &Ayz) ⊃ Axz) | Q.N. 1 | sp1 |
| 3. | (x)(y)~(∃z)((Axy &Ayz) ⊃ Axz) | Q.N. 2 | sp1 |
| 4. | (x)(y)(z)~((Axy &Ayz) ⊃ Axz) | Q.N. 3 | sp1 |
| 5. | (y)(z)~((Aay &Ayz) ⊃ Aaz) | U.I. 4 | sp1 |
| 6. | (z)~((Aaa &Aaz) ⊃ Aaz) | U.I. 5 | sp1 |
| 7. | ~((Aaa &Aaa) ⊃ Aaa) | U.I. 6 | sp1 |
| 8. | ~(~(Aaa &Aaa) v Aaa) | C.E. 7 | sp1 |
| 9. | (~~(Aaa &Aaa) & ~Aaa) | DEM, 8 | sp1 |
| 10. | (Aaa &Aaa) & ~Aaa) | D.N. 9 | sp1 |
| 11. | Aaa & ~Aaa | REP, 10 | sp1 |
| 12. | (∃x)(∃y)(∃z)((Axy &Ayz) ⊃ Axz) | I.P. 1-11 |