Predicate logic proofs - how to split a disjunction bound by two quantifiers

Question

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.

Answer 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.

Answer 2

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: