Conservativity theorem

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

$\mathrm{\exists }{x}_1\dots \mathrm{\exists }{x}_m\phi (x_1,\dots ,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,\dots ,a_m$

and adding a new axiom

$\phi (a_1,\dots ,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 $\mathrm{\forall }\overrightarrow{y}\mathrm{\exists }x\phi (x,\overrightarrow{y})$ is a theorem of a first-order theory $T$, where we denote $\overrightarrow{y}:=(y_1,\dots ,y_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 $\mathrm{\forall }\overrightarrow{y}\phi (f(\overrightarrow{y}),\overrightarrow{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.