Is $ \forall x(P(x) \lor Q(x)) \vdash \forall x P(x) \lor \exists xQ(x) $ provable? I know I should be able to determine whether the following holds, but I am not able to either find a model to show that this is false nor can I prove its correctness by using natural deduction.

$ \forall x(P(x) \lor Q(x))  \vdash \forall x P(x) \lor \exists xQ(x) $

Could anybody help me here?
 A: The entailment is true, as you can easily check using a tableaux. To construct a natural deduction proof, I would use the deduction theorem to transform the syntactic entailment into a material conditional, then proceed to construct the conditional statement by reductio ad absurdum. I don't know which natural deduction system you're using, but a sketch of a proof would look something like this. Hopefully you can translate my proof into whatever system you're using.
$$
\begin{align}
   (1)  & \quad \forall x (P(x) \vee Q(x)) && [\text{HYP}] \\
   (2)  & \quad \neg (\forall x (P(x)) \vee \exists x (Q(x))) && [\text{HYP}] \\ 
   (3)  & \quad \neg \forall x(P(x)) \wedge \neg \exists x(Q(x)) && [\text{DM} (2)] \\
   (4)  & \quad \neg \forall x(P(x)) && [\wedge\text{-elim}(3)] \\
   (5)  & \quad \neg \exists x(Q(x)) && [\wedge\text{-elim}(3)] \\
   (6)  & \quad \exists x (\neg P(x)) && [\neg\forall\text{-elim}(4)] \\
   (7)  & \quad \forall x (\neg Q(x)) && [\neg\exists\text{-elim}(5)] \\
   (8)  & \quad \neg P(a) && [\exists\text{-elim}(6)] \\
   (9)  & \quad \neg Q(a) && [\forall\text{-elim}(7)] \\
   (10) & \quad \neg P(a) \wedge \neg Q(a) && [\wedge\text{-intro}(8,9)] \\
   (11) & \quad P(a) \vee Q(a) && [\forall\text{-elim}(1)] \\
   (12) & \quad \neg (\neg P(a) \wedge \neg Q(a)) && [\text{DM}(11)] \\
   (13) & \quad \forall x(P(x) \vee \exists x(Q(x)) && [\text{RAA}(2,10,12)] \\
   (14) & \quad \forall x (P(x) \vee Q(x)) \rightarrow (\forall x(P(x) \vee \exists x(Q(x)) && [\rightarrow\text{-intro}(1,13)]
\end{align}
$$
Since you don't have De Morgan's Laws, I will sketch a proof that $\neg (P \wedge Q)$ implies $\neg P \vee \neg Q$ using the primitive rules of natural deduction, leaving the proof that $\neg (P \vee Q)$ implies $\neg P \wedge \neg Q$ as an exercise. The proofs are similar, so hopefully the following will be useful.
$$
\begin{align}
 (1) & \quad \neg (P \wedge Q) && [\text{HYP}] \\
 (2) & \quad \neg (\neg P \vee \neg Q) && [\text{HYP}] \\
 (3) & \quad \neg P && [\text{HYP}] \\
 (4) & \quad \neg P \vee \neg Q && [\vee\text{-intro}(3)] \\
 (5) & \quad P && [\text{RAA}(3,4)] \\
 (6) & \quad \neg Q && [\text{HYP}] \\
 (7) & \quad \neg P \vee \neg Q && [\vee\text{-intro}(6)] \\
 (8) & \quad Q && [\text{RAA}(3,7)] \\
 (9) & \quad P \wedge Q && [\wedge\text{-intro}(5,8)] \\
 (10) & \quad \neg P \vee \neg Q && [\text{RAA}(1,9)] \\
 (11) & \quad \neg (P \wedge Q) \rightarrow \neg P \vee \neg Q && [\rightarrow\text{-intro}(1,10)]
\end{align}
$$
A: Assume the antecedent is true and the conclusion is false.  If the conclusion is false, then $\forall{x}P(x)$ and $\exists{x}Q(x)$ are both false.  If $\forall{x}P(x)$ is false, then $P(x_0)$ is false for some $x_0$.  We know that $P(x_0)\vee Q(x_0)$ (from the antecedent).  Since $P(x_0)$ is false, $Q(x_0)$ must be true.  Therefore $\exists{x}Q(x)$ is true.  This contradicts our assumption that the conclusion was false.  Therefore the conclusion is true.
