In mathematical logic, the conservativity theorem states the following: Suppose that a closed formula
∃
x
1
…
∃
x
m
φ
(
x
1
,
…
,
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
,
…
,
a
m
and adding a new axiom
φ
(
a
1
,
…
,
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
∀
y
→
∃
x
φ
(
x
,
y
→
)
is a theorem of a first-order theory
T
, where we denote
y
→
:=
(
y
1
,
…
,
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
∀
y
→
φ
(
f
(
y
→
)
,
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
).
