Conservativity theorem

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

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

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

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

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