= Solution
The dot after $\forall x$ gives it scope over the following implication: read the premise as $H=\forall x\,(P(x)\to Q(x))$. Choose a fresh arbitrary <eigenvariable> $u$. A <natural deduction> proof is
$$
\begin{array}{rll}
1&H&\text{premise}\\
2&[\forall x\,P(x)]^a&\text{assumption}\\
3&\quad P(u)\to Q(u)&\forall E\ 1\\
4&\quad P(u)&\forall E\ 2\\
5&\quad Q(u)&\to E\ 4,3\\
6&\quad\forall x\,Q(x)&\forall I\ 5\\
7&(\forall x\,P(x))\to(\forall x\,Q(x))&\to I\ (2\text{--}6).
\end{array}
$$
At line 6, $u$ is free in no undischarged assumption, so the <universal quantifier introduction rule> is valid.
The proposed variant is not derivable in a sound <first-order logic>. For a <countermodel>, use the two-element domain $\{0,1\}$, interpret both <predicates> $P,Q$ as $\{0\}$, and assign the free variable $x$ the value 0. Then $\forall x(P(x)\to Q(x))$ is true, as is $P(x)$ under the assignment, but $\forall x\,Q(x)$ is false at element 1. The premise's bound $x$ and the conclusion's free $x$ have different scopes.
$$
\boxed{H\vdash(\forall x\,P(x))\to(\forall x\,Q(x)),\qquad
H\not\vdash P(x)\to(\forall x\,Q(x)).}
$$
Attempting to generalize from $Q(x)$ in the variant would violate the <eigenvariable condition>, because $x$ remains free in the undischarged assumption $P(x)$.
Back to article page
