Inference in Predicate Logic

Question

I have stumbled upon the following reasoning, but I'm not sure if it's correct. Here it goes: Domain X

1. $\forall x :\phi(x)⟹\gamma(x)$
2. Let $E\subseteq X⟹[\forall x\in E :\phi(x)⟹\gamma(x)]$
3. Suppose I know, by some property of $E$, that $\forall x\in E :\phi(x)$, that is for every $x\in E$, $\phi(x)$ is true.
4. [$\forall x\in E :\phi(x)] ⟹ \phi(x)$ (by universal instantation)
5. ⟹ $\gamma(x)$ (by universal instantation of 2. and by 4.)
6. ⟹ $\forall x\in E :\gamma(x)$ (by universal generalization)
7. Therefore: [$\forall x\in E :\phi(x)⟹\gamma(x)]\wedge [\forall x\in E :\phi(x)] ⟹ \forall x\in E :\gamma(x)$

It's like I have distributed the quantifier over the implication. Is this correct?

Answer 1

1. $\forall x : \phi(x) \implies \gamma(x)$ (premise)
2. $E\subset X$ (premise)
3. $\forall x \in E :\phi(x) \implies \gamma(x)$ (by 2)
4. $\forall x \in E : \phi(x)$ (premise)
5. $\phi(x)$ (U.I, 4)
6. $\phi(x) \implies \gamma(x)$ (U.I, 3)
7. $\gamma(x)$ (M.P, 5, 6)
8. $\forall x \in E : \gamma(x)$ (U.G, 7)
9. $\forall x \in E : \phi(x)\implies \forall x \in E : \gamma(x)$ (conditional proof, 4 - 8)

10. $\forall x \in E (\phi(x) \implies \gamma(x)) \land (\forall x \in E : \phi(x))\implies \forall x \in E : \gamma(x))$

11. $\forall x \in E (\phi(x) \implies \gamma(x)) \implies [(\forall x \in E : \phi(x))\implies (\forall x \in E : \gamma(x))]$

Answer 2

This is correct. Note that you can go a little bit further: $\forall x(\varphi(x)\implies\psi(x))$ implies $\forall x(\varphi(x))\implies\forall x(\psi(x))$. This is one direction of distributivity of $\forall$ over $\implies$.

As a cautionary note, let me point out that similar-looking principles may not hold, e.g.: it is not the case that $$[(\forall x\varphi(x))\implies (\forall x\psi(x))\quad \color{red}{\implies}\quad \forall x(\varphi(x)\implies\psi(x))].$$ That is, distributivity doesn't go in both directions.

---

Note that distributivity does work both ways for $\forall$ over $\wedge$, but (again) works only one way for $\forall$ over $\vee$. Similar but dual results hold for distribution of $\exists$ over Boolean operations.