# 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 Mar 4, 2014 at 8:48
• @user103088 Yes, you are right. Mar 4, 2014 at 8:53