= Solution
A <variable> $v$ is fresh for the surrounding context $\Gamma$ when it does not occur free in any undischarged assumption in $\Gamma$. Choose it also distinct from bound variables that would cause <variable capture> in the intended substitution. The <universal quantifier introduction rule> is
$$
\boxed{\frac{\Gamma\vdash\phi(v)}{\Gamma\vdash\forall x\,\phi(x)}\quad(v\text{ fresh for }\Gamma).}
$$
Its justification is that the <logical derivation> of $\phi(v)$ used no special information about $v$, so it establishes the property of an arbitrary object. Semantically, changing the assignment of $v$ preserves the truth of $\Gamma$; therefore $\phi(v)$ holds for every possible assigned object. Without the <eigenvariable condition>, the assumption $R(v)$ could incorrectly be generalized to $\forall x\,R(x)$ in an interpretation where only one of two objects satisfies $R$.
Back to article page
