I am pretty confused by this. We know that $\phi : = \exists x Px \land \exists x Qx $ does not imply $\psi : = \exists x (P x \land Q x)$, as for the model $M$ with domain $\{0,1\}$ with $P := \{0\}$ and $Q := \{1\}$, we have that $M \models \phi$, $M \not \models \psi$. But, seemingly:

\begin{eqnarray} \exists x Px \land \exists x Qx \implies & \lnot ( \lnot ( \exists x Px \land \exists x Qx))\\ \implies & \lnot ( \lnot \exists x Px \lor \lnot \exists x Qx)\\ \implies & \lnot (\forall x \lnot Px \lor \forall x \lnot Qx))\\ \implies & \lnot (\forall x (\lnot Px \lor \lnot Qx ))\\ \implies & \exists x \lnot ( \lnot P x \lor \lnot Q x) \\ \implies & \exists x (P x \land Q x) , \end{eqnarray}

where $(3) \implies (4)$ by the schema $\forall x A x \lor \forall x B x \implies \forall x (A x \lor B x)$; (2) $\implies (3), (4) \implies (5)$ by quantifier/negation relations; and $(1) \implies (2), (5) \implies (6)$ by De Morgan's laws. What went wrong here? Thanks!


1 Answer 1


$$ \lnot (\forall x \lnot Px \lor \forall x \lnot Qx)) \Rightarrow \lnot (\forall x (\lnot Px \lor \lnot Qx ))\\$$

is not correct.

It is equivalent to

$$ \varphi ~ =: ~\forall x \lnot Px \lor \forall x \lnot Qx \Leftarrow \forall x (\lnot Px \lor \lnot Qx ) ~ := \psi\\$$

Consider your examplary $\{P,Q\}$-structure $A$ over the universe $\{0,1\}$ with $P=\{0\}$ and $Q=\{1\}$.

Now $A \models \psi$ but $A \not \models \varphi$.

This the schema $\forall x A x \lor \forall x B x \Rightarrow \forall x (A x \lor B x)$ is correct but you have been using it the otherway around which is generally not a correct implication.

  • $\begingroup$ Great thank you! This answer also explains why moving from the last statement to the first is indeed valid. I made the error that I can substitute implications of logical expressions for those expressions e.g. P $\land$ Q implies P does not entail $\lnot(P \land Q)$ implies $\lnot(P)$ $\endgroup$
    – user40919
    Nov 21, 2013 at 22:35
  • $\begingroup$ Results such as these are easy (and fun!) to check using the method of analytic tableaux. [I drew one up for you in an answer but my phone's not letting me share it for some reason.] I recommend learning how to use them :) $\endgroup$
    – Shaun
    Nov 21, 2013 at 23:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .