$\varphi$ is quantifier free sentence, $T$ a theory, $\vec{c} \not\in T$. $T \vdash \varphi(\vec{c})$ implies $T \vdash \forall x \varphi(\vec{x})$?

Question

Let $\varphi$ be a quantifier free sentence and $T$ is a theory such that $\vec{c} \not\in T$. I am trying to see why the following is true: $T \vdash \varphi(\vec{c})$ implies $T \vdash \forall x \varphi(\vec{x})$. I am looking for a purely syntatical proof, i.e. whether the fact that there is some deduction of $\varphi(\vec{c})$ from $T$ implies that there is some deduction of $\forall x \varphi(\vec{x})$. If this is true, how can I qualify my statement so that it does become true? You can pick any deduction system and I would be grateful for your help.

Answer 1

The result is known as Generalization on constant.

The "trick" is simple: if you have a proof of $\varphi(c)$ and $c$ is not used in the set $T$ of assumptions (axioms), you can replace everywhere in the proof $c$ with a new variable $w$, where new means: nowhere occurring in the proof (the proof is a finite object and we have an unlimited supply of variables).

The result will be $T \vdash \varphi [w/c]$. The proof is by induction on the length of the derivation.

Due to the fact that $c$ does not occur in $T$, also the variable $w$ will not, and thus you can apply Generaliztion to conclude with $T \vdash \forall x \varphi$.