# 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}}$

and adding a new axiom

${\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}$.

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 ${\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 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\,\!}$).

## References

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