In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition.
For example, it is common in naive set theory to introduce a symbol
In the formal setting of first-order theories, this can be done by adding to the theory a new constant
It can then be proved that doing so adds essentially nothing to the old theory, as should be expected from a definition.
More precisely, the new theory is a conservative extension of the old one.
be a first-order theory and
are distinct and include the variables free in
Form a new first-order theory
-ary relation symbol
, the logical axioms featuring the symbol
(changing the bound variables in
is a conservative extension of
shows that the defining axiom of
, but the defined symbol
be a first-order theory (with equality) and
are distinct and include the variables free in
Form a new first-order theory
-ary function symbol
, the logical axioms featuring the symbol
by replacing that occurrence by a new variable
be (changing the bound variables in
is formed by replacing every occurrence of an atomic subformula
As in the case of relation symbols, the formula
The construction of this paragraph also works for constants, which can be viewed as 0-ary function symbols.
A first-order theory
by successive introductions of relation symbols and function symbols as above is called an extension by definitions of
is a conservative extension of
Such a formula is not unique, but any two of them can be proved to be equivalent in T. In practice, an extension by definitions
of T is not distinguished from the original theory T. In fact, the formulas of
can be thought of as abbreviating their translations into T. The manipulation of these abbreviations as actual formulas is then justified by the fact that extensions by definitions are conservative.