Fitch natural deduction proof of $\forall x (P(x) \to Q(x)) \to (\forall x (P(x)) \to \forall x (Q(x))$

My logic exam is coming up and I'm pretty happy with my natural deductions, but I found this 'gem' in an old exam paper and for the life of me I cannot figure it out.

You need to prove $$\forall x (P(x) \to Q(x)) \to (\forall x (P(x)) \to \forall x (Q(x))$$ from no premises. The fact that there are no conjunctions or disjunctions makes this quite a tricky one, especially since there are 3 conditionals in there as well. I am trying to work backwards, ie. starting with the conclusion and working my way back up but even then I get stuck.

Any assistance would be greatly appreciated, thanks!

I assume there is a final ")" at the end of the formula you are trying to prove.

Here is a result using a proof checker: If you have a series of conditionals like you do, start by making subproofs assuming the antecedents of the conditionals. Then attempt to show the consequent for the innermost conditional. If you can do that then you can use conditional introduction (→I) to discharge the assumptions of the subproofs in reverse order.

The rules associated with this proof checker are given in the forallx book linked below.

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

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

• Thanks so much for your help - I eventually figured it out and checked my result against yours - it isn't 100% the same but boils down to the same thing. – Gerhardus Carinus May 12 at 15:16

Hint

Assume $$∀x(P(x)→Q(x))$$ and assume $$∀xP(x)$$.

Then use suitable applications of $$(\forall \text E)$$ to get $$Q(x)$$.

• Thank you - that hint actually got me over the line! – Gerhardus Carinus May 12 at 15:15