# Extension by new constant and function names

In mathematical logic, a theory can be extended with new constants or function names under certain conditions with assurance that the extension will introduce no contradiction. Extension by definitions is perhaps the best-known approach, but it requires unique existence of an object with the desired property. Addition of new names can also be done safely without uniqueness.

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}$ $\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$ .
Suppose that a closed formula $\forall {\vec {x}}\,\exists y\,\!\,\varphi (y,{\vec {x}})$ is a theorem of a first-order theory $T$ , where we denote ${\vec {x}}:=(x_{1},\ldots ,x_{n})$ . Let $T_{1}$ be a theory obtained from $T$ by extending its language with a new functional symbol $f$ (of arity $n$ ) and adding a new axiom $\forall {\vec {x}}\,\varphi (f({\vec {x}}),{\vec {x}})$ . 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$ ).