1

I need to complete the following proof using only primitive rules (the introduction and elimination rules for each connective and quantifier).

(∃x)(∀y)(Py ∨ Qx) ⊢ (∀y)Py ∨ (∃x)Qx

I've only been able to get this far:

1| (∃x)(∀y)(Py ∨ Qx)        | Premise

2| a | (∀y)(Py ∨ Qa)        | Assumption

3|   | Pc ∨ Qa              | ∀ elimination, 2

4|   | (∃x)(Pc ∨ Qx)        | ∃ introduction, 3

5|   | e | Pc ∨ Qe          | Assumption

6|   |   | ???              | ???

I can't figure out how to split the disjunction into its respective parts using only primitive rules.

2 Answers 2

1

You cannot that way; after step 3), you need -Elimination (i.e. Proof by Caes).

You have to start two subproofs: one from assumption Pc and the second one from Qa and in both cases derive (∀y)Py ∨ (∃x)Qx.

1

This is a tricky proof, but given as your goal is a disjunction, a proof by contradiction is typically a good bet. Here is a proof following that strategy one done using the Fitch software: enter image description here

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .