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