Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 8 / a / ii / Solution

Choose a fresh parameter $a$. The universal quantifier elimination rule supplies both the implication and its premise at that same parameter:The eigenvariable condition holds because $a$ is absent from both undischarged assumptions at line 6. Hence the universally quantified implication is proved.

The proposed version with merely $P(x)$ in the antecedent is 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 xQ(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.