The Lemma on Constants is an elementary result, which says something like the following:

Lemma: Suppose {\displaystyle T\vdash \phi (c)}, where {\displaystyle T} is a theory, {\displaystyle \phi (x)} is a formula, x is a tuple of variables, and c is a tuple of constant symbols not appearing in T. Then {\displaystyle T\vdash \forall x:\phi (x)}.

Proof: If one interprets {\displaystyle T\vdash \psi } to mean that {\displaystyle \psi } holds in all models of T, then this follows from unwinding the definitions: {\displaystyle T\vdash \phi (c)} means that whenever M is a model of T and c is a tuple from M, {\displaystyle M\models \phi (c)}. Then clearly {\displaystyle M\models \forall x:\phi (x)}!

On the other hand, if one interprets {\displaystyle T\vdash \psi } to mean that {\displaystyle \psi } can be proven from T, then this follows from the other version by Gödel's Completeness Theorem, which says that these two interpretations of {\displaystyle \vdash } are the same. QED.

The Lemma on Constants is practically obvious. However, it is handy to have a name for this lemma when making technical arguments. ::: ::: :::