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 $T_1$ 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 $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

\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

T_1

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

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.

This article is issued from Wikipedia - version of the 11/6/2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.