The Lemma on Constants is an elementary result, which says something like the following:
Lemma: Suppose , where is a theory, is a formula, x is a tuple of variables, and c is a tuple of constant symbols not appearing in T. Then .
Proof: If one interprets to mean that holds in all models of T, then this follows from unwinding the definitions: means that whenever M is a model of T and c is a tuple from M, . Then clearly !
On the other hand, if one interprets to mean that 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 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. ::: ::: :::