# Theorem on Constants (and Substitution Theorem?)

"Let $$T'$$ be obtained from $$T$$ by adding new constants $$e_1,e_2,...,e_n$$ (but no new nonlogical axioms). For every formula $$A$$ of $$T$$, and every sequence of constants $$e_1,e_2,...,e_n$$, $$\vdash _TA$$ iff $$\vdash_{T'}A[e_1,e_2,...,e_n]$$."

It sounds like the theorem asserts that if an instance of a formula $$A$$ is provable for certain constants, then it must be provable for in general form, when those constants are replaced by free variables. This doesn't make much intuitive sense to me, and I'm not entirely sure I see how it follows from the substitution theorem, so for clarity's sake, I'd appreciate it if someone could correct me.

Edit: so it is the only if side that confuses me

• You have to write it correctly... The theorem does not assert that "$A$ is provable for certain constants". – Mauro ALLEGRANZA Dec 16 '19 at 12:30
• It says that if we can prove in theory $T$ the formula $A$ (with e.g. $x$ free), we can prove in theory $T'$ the formula $A[x/e]$ where the theory $T'$ has an "enlarged" language (the new constant symbol $e$) but no new axioms. – Mauro ALLEGRANZA Dec 16 '19 at 12:33
• If there are no new axioms, there is no axiom involving $e$; thus, we have no restriction on it. To prove a formula $A(x)$ with $x$ free amounts sematically to assert that $A$ holds for every object of the domain of every model of $T$. Thus, it holds also for object named $e$, whatever it is. – Mauro ALLEGRANZA Dec 16 '19 at 12:35
• @mauro-allegranza First off, thank you for replying to me. I'm alright with that side of the implication, that $A$ being provable implies $A[x/e]$ I understand. That $A[x/e]$ implies $A$ is what seems counterintuitive to me. – Caroline.T Dec 16 '19 at 12:41
• The issue is that an "unspecified" constant (this is the gist of : $e$ new but no new axioms) behaves exactly as a free variable. – Mauro ALLEGRANZA Dec 16 '19 at 15:39

The Substitution Rule part: once you have the proof of $$A[e_1, ..., e_n]$$ in $$T'$$ you may be tempted to prove $$A$$ in $$T$$ by simply replacing $$e_1, ..., e_n$$ by the appropriate $$x_1, ..., x_n$$ throughout the first proof. However, some of these variables may have been used in that proof, so they may interfere with the ones you've just inserted and ruin everything. The solution is to replace $$e_1, ..., e_n$$ by some $$y_1, ..., y_n$$ that weren't used in the proof. Now you have $$\vdash_TA[y_1, ..., y_n]$$ and by the substitution rule $$\vdash_TA[x_1, ..., x_n]$$ which is the same as $$\vdash_TA$$.