How to disjunct $\forall x.(P(x) \lor Q(x))$

I really don't understand how to disjunct this. The whole argument is:

$$\forall x.[P(x) \lor Q(x)] \rightarrow \neg[\exists x.P(x)] \rightarrow \forall x. Q(x)$$

Am I supposed to use the deduction method to get

$$\forall x.[P(x) \lor Q(x)] \land \neg[\exists x.P(x)]$$

Which would allow me to then use de Morgan

$$\neg[\exists x.P(x)] \rightarrow \forall x. \neg[P(x)]$$

But then how would I obtain

$$\exists x. P(x) \land \forall x. Q(x)$$

Or am I just missing something here.

Before give a hint, I rewrite your attempt. As I see, you try to prove $$\vdash ∀x.[P(x)∨Q(x)]→[¬∃x.P(x)→∀x.Q(x)].$$ You try to use deduction theorem so you try to prove $$∀x.[P(x)∨Q(x)]\,;\,\lnot [\exists P(x)]\vdash \forall x.Q(x)$$ by De Morgan's theorem you get $\vdash\lnot\exists x.P(x) \leftrightarrow \forall x.\lnot P(x)$.

I give a way how to preceed the proof :

1. Use universal instantiation so you get $P(c)\lor Q(c)$.

2. Eliminate $P(c)$. (How?)

3. Use universal generalization.

Note. $\sigma;\tau\vdash\varphi$ means "you can deduce $\varphi$ from $\sigma$, $\tau$ and logical axioms."

• Ah okay I think I get it. So negate P(c) by using universal instantiation from De Morgan's and then get Q(c) from disjunctive syllogism and finally get forall x. Q(x) by universal generalization – user103088 Mar 4 '14 at 8:48
• @user103088 Yes, you are right. – Hanul Jeon Mar 4 '14 at 8:53