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.


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

  • $\begingroup$ 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 $\endgroup$
    – user103088
    Mar 4, 2014 at 8:48
  • $\begingroup$ @user103088 Yes, you are right. $\endgroup$
    – Hanul Jeon
    Mar 4, 2014 at 8:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.