Extension by new constant and function names

In mathematical logic, the conservativity theorem states the following: Suppose that a closed formula

$\exists x_{1}\ldots \exists x_{m}\,\varphi (x_{1},\ldots ,x_{m})$

is a theorem of a first-order theory $T$. Let $T_{1}$ be a theory obtained from $T$ by extending its language with new constants

$a_{1},\ldots ,a_{m}$

and adding a new axiom

$\varphi (a_{1},\ldots ,a_{m})$.

Then $T_{1}$ is a conservative extension of $T$, which means that the theory $T_{1}$ has the same set of theorems in the original language (i.e., without constants $a_{i}$) as the theory $T$.

In a more general setting, the conservativity theorem is formulated for extensions of a first-order theory by introducing a new functional symbol:

Suppose that a closed formula $\forall {\vec {y}}\,\exists x\,\!\,\varphi (x,{\vec {y}})$ is a theorem of a first-order theory $T$, where we denote ${\vec {y}}:=(y_{1},\ldots ,y_{n})$. Let $T_{1}$ be a theory obtained from $T$ by extending its language with new functional symbol $f$ (of arity $n$) and adding a new axiom $\forall {\vec {y}}\,\varphi (f({\vec {y}}),{\vec {y}})$. Then $T_{1}$ is a conservative extension of $T$, i.e. the theories $T$ and $T_{1}$ prove the same theorems not involving the functional symbol $f$).

References

• Elliott Mendelson (1997). Introduction to Mathematical Logic (4th ed.) Chapman & Hall.
• J.R. Shoenfield (1967). Mathematical Logic. Addison-Wesley Publishing Company.