Distribution of universal quantifiers over implication I want to prove that $∀x(φ(x)⟹ψ(x))$ implies $∀x(φ(x))⟹∀x(ψ(x))$. I read they are not equivalent, but I am not sure why. I tried the following:


*

*$∀x(φ(x)⟹ψ(x))$

*$⟹[φ(a)⟹ψ(a)]$ is true.

*$⟹φ(a)$ is true.

*$⟹∀x(φ(x))$ (by universal generalization of 3.)

*$⟹φ(a)$ (by universal instantation of 4. and 3.)

*$⟹ψ(a)$ (by 2.)

*$⟹∀x(φ(x))$

*Finally $[∀x(φ(x)⟹ψ(x))]⟹[∀x(φ(x))⟹∀x(φ(x))]$


I can't think of a counterexpample to show that they are not equivalent. Any hints would be greatly appreciated.
 A: For a counterexample to show that the two forms are not equivalent, you can let $\varphi(x)$ mean "$x$ is even" and $\psi(x)$ mean "$x$ is odd" (say, in an universe where the quantifiers range over $\mathbb N$).
A: The argument you give is broken, for reasons stated in the comments.
Here is a hint for how to approach the problem:
Suppose we assume both $$(*)\quad\forall x(\varphi(x)\implies \psi(x))$$ and $$(**)\quad \forall x(\varphi(x)).$$ What do we know if $\forall x(\psi(x))$ happens to fail? Well, by definition this would mean $\exists x(\neg\psi(x))$. Let $a$ be such an $x$; what does $(*)$ tell us about $a$? Why does this contradict $(**)$? 
A: Proof in the forward direction $\forall x \; (\phi(x) \implies \psi(x)) \implies(\forall x \, \phi(x) \implies \forall x \,\psi(x))$.


*

*$\forall x \; (\phi(x) \implies \psi(x))$

*$\forall x \, \phi(x)$

*$\phi(a)$ (U.I. 2, a\x)

*$\phi(a) \implies \psi(a)$ (U.I. 1, a\x)

*$\psi(a)$ (M.P. 3, 4)

*$\forall x \, \psi(x)$ (U.G. 5)

*$\forall x \, \phi(x) \implies \forall x \, \psi(x)$ (conditional proof, 2 - 6)

*$\forall x \; (\phi(x) \implies \psi(x)) \implies(\forall x \, \phi(x) \implies \forall x \,\psi(x))$ (conditional proof, 1-7)


Please note that we are only able to preform step 6 because both the Universal instantation and its generalization occur within the same conditional proof.
An improper use use of Universal Generalization would be


*

*$\forall x \; \phi(x)$(premise)

*$\phi(a)$ 

*$\phi(a) \implies \varphi(a)$ (assumption, begin conditional proof)

*$\varphi(a)$

*$\forall x \; \varphi(x)$


This is incorrect because 4. is only true because 3 is true. i.e. we should have discharged the assumption and then we could have generalized. So it would properly look like 


*

*$\forall x \; \phi(x)$(premise)

*$\phi(a)$ 

*$\phi(a) \implies \varphi(a)$ (assumption, begin conditional proof)

*$\varphi(a)$

*$(\phi(a) \implies \varphi(a))\implies \varphi(a) $

*$\forall x \; (\phi(x) \implies \varphi(x))\implies \varphi(x))$


Now a counter example for the converse:


*

*$\phi(a) \land \lnot \phi(b) \land \lnot \psi(a) \land \lnot \psi(b)$ (premise)

*$\phi(a) \land \lnot \psi(a)$ (Simp., 2)

*$\lnot(\psi(a) \implies \psi(a))$ (M.I./D.M., 3)

*$\exists x\, \lnot(\psi(x) \implies \psi(x))$ (E.G. 4)

*$\lnot \forall x \, (\psi(x) \implies \psi(x))$ (D.M. for Quantifiers, 5)

*$\lnot \phi(b)$ (Simp., 2)

*$\exists x \, \lnot \phi(x)$ (E.G, 7)

*$ \lnot \forall x \, \phi(x)$ (D.M. for Quantifiers, 8)

*$ \lnot \forall x \, \phi(x) \lor \forall x \, \psi(x)$ (Add., 9)

*$\forall x \, \phi(x) \implies \forall x \, \psi(x)$ (M.I., 10)

*$(\forall x \, \phi(x) \implies \forall x \, \psi(x))\land \lnot \forall x \, (\psi(x) \implies \psi(x)) $ (Conj., 11, 6)

*$\lnot [(\forall x \, \phi(x) \implies \forall x \, \psi(x))\implies \forall x \, (\psi(x) \implies \psi(x))]$ (M.I., D.M., 12)

*(1) is a counter example


Of course a counter example doesn't need to be shown in this way, but I'm not sure how else to show that it is in fact a counter example.
