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

Question

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.

Answer 1

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