Conservativity theorem

Conservativity theorem

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 T1 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 T1 is a conservative extension of T, which means that the theory T1 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 T1 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 T1 is a conservative extension of T, i.e. the theories T and T1 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.
Stub icon This logic-related article is a stub. You can help Wikipedia by expanding it. This mathematical logic-related article is a stub. You can help Wikipedia by expanding it.