= Solution
Choose a fresh parameter $a$. The <universal quantifier elimination rule> supplies both the implication and its premise at that same parameter:
``
1 ∀x. (P(x) → Q(x)) premise
2 | ∀x. P(x) assumption
3 | P(a) ∀-elim 2
4 | P(a) → Q(a) ∀-elim 1
5 | Q(a) →-elim 4,3
6 | ∀x. Q(x) ∀-intro 5, a fresh
7 (∀x. P(x)) → (∀x. Q(x)) →-intro 2–6
``
The <eigenvariable condition> holds because $a$ is absent from both undischarged assumptions at line 6. Hence \b[the universally quantified implication is proved].
The proposed version with merely $P(x)$ in the antecedent is \b[not derivable]. For a <counterexample>, take a two-element domain $\{0,1\}$ with $P$ and $Q$ both true precisely at zero. The universal premise holds. Under the assignment $x=0$, $P(x)$ is true but $\forall x\,Q(x)$ is false. By <soundness>, a formal proof cannot exist. Attempting the previous derivation would fail exactly at <universal quantifier introduction rule>: the parameter would occur in the undischarged assumption $P(x)$, so it would not be fresh.
Back to article page
