In mathematical logic, more specifically in the proof theory of first-order theories, an extension by definition formalizes the introduction of a new symbol by means of a definition. For example, it is common in naive set theory to introduce a symbol 👁 {\displaystyle \emptyset }
for the set that has no member. In the formal setting of first-order theories, this can be done by adding to the theory a new constant 👁 {\displaystyle \emptyset }
and the new axiom 👁 {\displaystyle \forall x(x\notin \emptyset )}
, meaning "for all x, x is not a member of 👁 {\displaystyle \emptyset }
". 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.

Let 👁 {\displaystyle T}
be a first-order theory and 👁 {\displaystyle \phi (x_{1},\dots ,x_{n})}
a formula of 👁 {\displaystyle T}
such that 👁 {\displaystyle x_{1}}
, ..., 👁 {\displaystyle x_{n}}
are distinct and include the variables free in 👁 {\displaystyle \phi (x_{1},\dots ,x_{n})}
. Form a new first-order theory 👁 {\displaystyle T'}
from 👁 {\displaystyle T}
by adding a new 👁 {\displaystyle n}
-ary relation symbol 👁 {\displaystyle R}
, the logical axioms featuring the symbol 👁 {\displaystyle R}
and the new axiom

👁 {\displaystyle \forall x_{1}\dots \forall x_{n}(R(x_{1},\dots ,x_{n})\leftrightarrow \phi (x_{1},\dots ,x_{n}))}
,

called the defining axiom of 👁 {\displaystyle R}
.

If 👁 {\displaystyle \psi }
is a formula of 👁 {\displaystyle T'}
, let 👁 {\displaystyle \psi ^{\ast }}
be the formula of 👁 {\displaystyle T}
obtained from 👁 {\displaystyle \psi }
by replacing any occurrence of 👁 {\displaystyle R(t_{1},\dots ,t_{n})}
by 👁 {\displaystyle \phi (t_{1},\dots ,t_{n})}
(changing the bound variables in 👁 {\displaystyle \phi }
if necessary so that the variables occurring in the 👁 {\displaystyle t_{i}}
are not bound in 👁 {\displaystyle \phi (t_{1},\dots ,t_{n})}
). Then the following hold:

1. 👁 {\displaystyle \psi \leftrightarrow \psi ^{\ast }}
   is provable in 👁 {\displaystyle T'}
   , and
2. 👁 {\displaystyle T'}
   is a conservative extension of 👁 {\displaystyle T}
   .

The fact that 👁 {\displaystyle T'}
is a conservative extension of 👁 {\displaystyle T}
shows that the defining axiom of 👁 {\displaystyle R}
cannot be used to prove new theorems. The formula 👁 {\displaystyle \psi ^{\ast }}
is called a translation of 👁 {\displaystyle \psi }
into 👁 {\displaystyle T}
. Semantically, the formula 👁 {\displaystyle \psi ^{\ast }}
has the same meaning as 👁 {\displaystyle \psi }
, but the defined symbol 👁 {\displaystyle R}
has been eliminated.

Let 👁 {\displaystyle T}
be a first-order theory (with equality) and 👁 {\displaystyle \phi (y,x_{1},\dots ,x_{n})}
a formula of 👁 {\displaystyle T}
such that 👁 {\displaystyle y}
, 👁 {\displaystyle x_{1}}
, ..., 👁 {\displaystyle x_{n}}
are distinct and include the variables free in 👁 {\displaystyle \phi (y,x_{1},\dots ,x_{n})}
. Assume that we can prove

👁 {\displaystyle \forall x_{1}\dots \forall x_{n}\exists !y\phi (y,x_{1},\dots ,x_{n})}

in 👁 {\displaystyle T}
, i.e. for all 👁 {\displaystyle x_{1}}
, ..., 👁 {\displaystyle x_{n}}
, there exists a unique y such that 👁 {\displaystyle \phi (y,x_{1},\dots ,x_{n})}
. Form a new first-order theory 👁 {\displaystyle T'}
from 👁 {\displaystyle T}
by adding a new 👁 {\displaystyle n}
-ary function symbol 👁 {\displaystyle f}
, the logical axioms featuring the symbol 👁 {\displaystyle f}
and the new axiom

👁 {\displaystyle \forall x_{1}\dots \forall x_{n}\phi (f(x_{1},\dots ,x_{n}),x_{1},\dots ,x_{n})}
,

called the defining axiom of 👁 {\displaystyle f}
.

Let 👁 {\displaystyle \psi }
be any atomic formula of 👁 {\displaystyle T'}
. We define formula 👁 {\displaystyle \psi ^{\ast }}
of 👁 {\displaystyle T}
recursively as follows. If the new symbol 👁 {\displaystyle f}
does not occur in 👁 {\displaystyle \psi }
, let 👁 {\displaystyle \psi ^{\ast }}
be 👁 {\displaystyle \psi }
. Otherwise, choose an occurrence of 👁 {\displaystyle f(t_{1},\dots ,t_{n})}
in 👁 {\displaystyle \psi }
such that 👁 {\displaystyle f}
does not occur in the terms 👁 {\displaystyle t_{i}}
, and let 👁 {\displaystyle \chi }
be obtained from 👁 {\displaystyle \psi }
by replacing that occurrence by a new variable 👁 {\displaystyle z}
. Then since 👁 {\displaystyle f}
occurs in 👁 {\displaystyle \chi }
one less time than in 👁 {\displaystyle \psi }
, the formula 👁 {\displaystyle \chi ^{\ast }}
has already been defined, and we let 👁 {\displaystyle \psi ^{\ast }}
be

👁 {\displaystyle \forall z(\phi (z,t_{1},\dots ,t_{n})\rightarrow \chi ^{\ast })}

(changing the bound variables in 👁 {\displaystyle \phi }
if necessary so that the variables occurring in the 👁 {\displaystyle t_{i}}
are not bound in 👁 {\displaystyle \phi (z,t_{1},\dots ,t_{n})}
). For a general formula 👁 {\displaystyle \psi }
, the formula 👁 {\displaystyle \psi ^{\ast }}
is formed by replacing every occurrence of an atomic subformula 👁 {\displaystyle \chi }
by 👁 {\displaystyle \chi ^{\ast }}
. Then the following hold:

1. 👁 {\displaystyle \psi \leftrightarrow \psi ^{\ast }}
   is provable in 👁 {\displaystyle T'}
   , and
2. 👁 {\displaystyle T'}
   is a conservative extension of 👁 {\displaystyle T}
   .

The formula 👁 {\displaystyle \psi ^{\ast }}
is called a translation of 👁 {\displaystyle \psi }
into 👁 {\displaystyle T}
. As in the case of relation symbols, the formula 👁 {\displaystyle \psi ^{\ast }}
has the same meaning as 👁 {\displaystyle \psi }
, but the new symbol 👁 {\displaystyle f}
has been eliminated.

The construction of this paragraph also works for constants, which can be viewed as 0-ary function symbols.

A first-order theory 👁 {\displaystyle T'}
obtained from 👁 {\displaystyle T}
by successive introductions of relation symbols and function symbols as above is called an extension by definitions of 👁 {\displaystyle T}
. Then 👁 {\displaystyle T'}
is a conservative extension of 👁 {\displaystyle T}
, and for any formula 👁 {\displaystyle \psi }
of 👁 {\displaystyle T'}
we can form a formula 👁 {\displaystyle \psi ^{\ast }}
of 👁 {\displaystyle T}
, called a translation of 👁 {\displaystyle \psi }
into 👁 {\displaystyle T}
, such that 👁 {\displaystyle \psi \leftrightarrow \psi ^{\ast }}
is provable in 👁 {\displaystyle T'}
. 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 👁 {\displaystyle T'}
of T is not distinguished from the original theory T. In fact, the formulas of 👁 {\displaystyle T'}
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.

• Traditionally, the first-order set theory ZF has 👁 {\displaystyle =}
  (equality) and 👁 {\displaystyle \in }
  (membership) as its only primitive relation symbols, and no function symbols. In everyday mathematics, however, many other symbols are used such as the binary relation symbol 👁 {\displaystyle \subseteq }
  , the constant 👁 {\displaystyle \emptyset }
  , the unary function symbol P (the power set operation), etc. All of these symbols belong in fact to extensions by definitions of ZF.
• Let 👁 {\displaystyle T}
  be a first-order theory for groups in which the only primitive symbol is the binary product ×. In T, we can prove that there exists a unique element y such that x × y = y × x = x for every x. Therefore, we can add to T a new constant e and the axiom

👁 {\displaystyle \forall x(x\times e=x\land e\times x=x)}
,

and what we obtain is an extension by definitions 👁 {\displaystyle T'}
of 👁 {\displaystyle T}
. Then in 👁 {\displaystyle T'}
we can prove that for every x, there exists a unique y such that x × y = y × x = e. Consequently, the first-order theory 👁 {\displaystyle T''}
obtained from 👁 {\displaystyle T'}
by adding a unary function symbol 👁 {\displaystyle f}
and the axiom

👁 {\displaystyle \forall x(x\times f(x)=e\land f(x)\times x=e)}

is an extension by definitions of 👁 {\displaystyle T}
. Usually, 👁 {\displaystyle f(x)}
is denoted 👁 {\displaystyle x^{-1}}
.

• Conservative extension
• Definite description
• Epsilon calculus
• Extension by new constant and function names

• S. C. Kleene (1952), Introduction to Metamathematics, D. Van Nostrand
• E. Mendelson (1997). Introduction to Mathematical Logic (4th ed.), Chapman & Hall.
• J. R. Shoenfield (1967). Mathematical Logic, Addison-Wesley Publishing Company (reprinted in 2001 by AK Peters)