What proof strategy can we use to prove this? $$\forall x [P(x) \rightarrow Q(x)] \Rightarrow [\forall x P(x) \rightarrow \forall x Q(x)]$$
I tried to do a proof by case, but it doesn't work because of the quantifiers. So I was wondering what are the proof strategies I can use for this.
 A: You are given that 
$$\tag1\forall x[P(x)\to Q(x).$$
Assume that 
$$\tag2\forall x P(x).$$
Let $x$ be arbitrary.
Then by specialization from $(2)$, you have$P(x)$ and by specialization from $(1)$ you have $P(x)\to Q(x)$, hence by modus ponens $(Q(x)$.
By generalization (i.e. because $x$ was arbitrary)
$$\tag 3 \forall x Q(x).$$
Since you derived $(3)$ by assuming $(2)$, you have
$$\forall x P(x)\to \forall x Q(x).$$
A: Assuming that you’re allowed to argue informally, I’d assume that $\forall xP(x)\to\forall xQ(x)$ is false. Then $\forall xP(x)$ must be true, and $\forall xQ(x)$ must be false. Thus, every $x$ (in the universe of discourse) has property $P$, but there is at least one $-$ call it $a$ $-$ that does not have property $Q$.
You should now be able to show quite easily that $\forall x [P(x) \rightarrow Q(x)]$ cannot be true, thereby showing the contrapositive of 
$$\forall x [P(x) \rightarrow Q(x)] \Rightarrow [\forall x P(x) \rightarrow \forall x Q(x)]\;.$$
A: Or you can argue directly. What do you need in order to establish a conditional (as on the RHS)?
You assume the antecedent and aim to prove the consequent.
So you are given the LHS i.e. $\forall x [P(x) \rightarrow Q(x)]$, are assuming $\forall x P(x)$ for the sake of argument, and need to show $\forall x Q(x)$.
Do you see how to do that? (If you don't immediately see it, you need to (re)read a decent introduction to predicate logic, as this really is ABC.)
A: There are two proof strategies presented in the answers. I will use a proof checker to show each one and then provide a third strategy.  Both start out assuming $∀xP(x)$, but approach the proof differently.


*

*Brian M. Scott then assumed $∀xQ(x)$ was false to derive a contradiction as this proof does:





*Hagen von Eitzen derived $Q(x)$ directly.





*This proof starts with assuming the negation of the material implication of the goal.



It is useful having multiple strategies one can use to approach a problem.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
