Proofs in Polyadic QL
Like truth-trees, proofs in Polyadic QL introduce no new rules. Here too, care must be taken in applying the rules involving quantifiers.
Let's prove the following theorem:
| (x)(y)Lxy ⊃ (∃x)(∃y)Lxy |
Since this is a theorem, we don't have premises. We must use Conditional Proof or Indirect Proof. Conditional Proof is the natural choice, since the wff is a conditional. Here's the whole proof:
| 1. | (x)(y)Lxy | Assump., CP | SP1 |
| 2. | (y)Lay | U.I., 1 | SP1 |
| 3. | Laa | U.I., 2 | SP1 |
| 4. | (∃y)Lay | E.G. 3 | SP1 |
| 5. | (∃x)(∃y)Lxy | E.G. 4 | SP1 |
| 6. | (x)(y)Lxy ⊃ (∃x)(∃y)Lxy | CP, 1-5 |
Lines 2 and 3 instantiate the universal quantifiers, one
at a time. Lines 4 and 5 existentially generalize, one at a time. Line 6 allows
the inference to the conditional. Easy!
Let's look at another example. We will prove:
| (x)(Sx ⊃ ~(∃y)(Py v Txy)) |
| (∃x)(Tax & Px) |
| ~Sa |
In thinking through our strategy for this proof, we note that the conclusion is the negation of some instantiated version of the antecedent of the conditional in the first premise. So if we can derive the negation of the consequent of that conditional, we can use Modus Tollens to get the conclusion.
| 1. | (x)(Sx ⊃ ~(∃y)(Py v Txy)) | premise | |
| 2. | (∃x)(Tax & Px) | premise | |
| 3. | Sa ⊃ ~(∃y)(Py v Tay) | U.I., 1 | |
| 4. | Tab & Pb | E.I., 2, flag b | |
| 5. | Pb | Simp, 4 | |
| 6. | Pb v Tab | Disj., 5 | |
| 7. | (∃y)(Py v Tay) | E.G., 6 | |
| 8. | ~~(∃y)(Py v Tay) | D.N. 7 | |
| 9. | ~Sa | M.T., 3,8 |
Have we run out of exercises? No!
 |
 |