# Extension by definitions

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 $\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 $\emptyset$ and the new axiom $\forall x(x\notin \emptyset )$, meaning "for all x, x is not a member of $\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.

## Definition of relation symbols

Let $T$ be a first-order theory and $\phi (x_{1},\dots ,x_{n})$ a formula of $T$ such that $x_{1}$, ..., $x_{n}$ are distinct and include the variables free in $\phi (x_{1},\dots ,x_{n})$. Form a new first-order theory $T'$ from $T$ by adding a new $n$-ary relation symbol $R$, the logical axioms featuring the symbol $R$ and the new axiom
    $\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 $R$.
If $\psi$ is a formula of $T'$, let $\psi ^{\ast }$ be the formula of $T$ obtained from $\psi$ by replacing any occurrence of $R(t_{1},\dots ,t_{n})$ by $\phi (t_{1},\dots ,t_{n})$ (changing the bound variables in $\phi$ if necessary so that the variables occurring in the $t_{i}$ are not bound in $\phi (t_{1},\dots ,t_{n})$). Then the following hold:
* $\psi \leftrightarrow \psi ^{\ast }$ is provable in $T'$, and
* $T'$ is a conservative extension of $T$.
The fact that $T'$ is a conservative extension of $T$ shows that the defining axiom of $R$ cannot be used to prove new theorems. The formula $\psi ^{\ast }$ is called a translation of $\psi$ into $T$. Semantically, the formula $\psi ^{\ast }$ has the same meaning as $\psi$, but the defined symbol $R$ has been eliminated.

## Definition of function symbols

Let $T$ be a first-order theory (with equality) and $\phi (y,x_{1},\dots ,x_{n})$ a formula of $T$ such that $y$, $x_{1}$, ..., $x_{n}$ are distinct and include the variables free in $\phi (y,x_{1},\dots ,x_{n})$. Assume that we can prove
    $\forall x_{1}\dots \forall x_{n}\exists !y\phi (y,x_{1},\dots ,x_{n})$
in $T$, i.e. for all $x_{1}$, ..., $x_{n}$, there exists a unique y such that $\phi (y,x_{1},\dots ,x_{n})$. Form a new first-order theory $T'$ from $T$ by adding a new $n$-ary function symbol $f$, the logical axioms featuring the symbol $f$ and the new axiom
    $\forall x_{1}\dots \forall x_{n}\phi (f(x_{1},\dots ,x_{n}),x_{1},\dots ,x_{n})$,
called the defining axiom of $f$.
Let $\psi$ be any atomic formula of $T'$. We define formula $\psi ^{\ast }$ of $T$ recursively as follows. If the new symbol $f$ does not occur in $\psi$, let $\psi ^{\ast }$ be $\psi$. Otherwise, choose an occurrence of $f(t_{1},\dots ,t_{n})$ in $\psi$ such that $f$ does not occur in the terms $t_{i}$, and let $\chi$ be obtained from $\psi$ by replacing that occurrence by a new variable $z$. Then since $f$ occurs in $\chi$ one less time than in $\psi$, the formula $\chi ^{\ast }$ has already been defined, and we let $\psi ^{\ast }$ be
    $\forall z(\phi (z,t_{1},\dots ,t_{n})\rightarrow \chi ^{\ast })$
(changing the bound variables in $\phi$ if necessary so that the variables occurring in the $t_{i}$ are not bound in $\phi (z,t_{1},\dots ,t_{n})$). For a general formula $\psi$, the formula $\psi ^{\ast }$ is formed by replacing every occurrence of an atomic subformula $\chi$ by $\chi ^{\ast }$. Then the following hold:
* $\psi \leftrightarrow \psi ^{\ast }$ is provable in $T'$, and
* $T'$ is a conservative extension of $T$.
The formula $\psi ^{\ast }$ is called a translation of $\psi$ into $T$. As in the case of relation symbols, the formula $\psi ^{\ast }$ has the same meaning as $\psi$, but the new symbol $f$ has been eliminated.
The construction of this paragraph also works for constants, which can be viewed as 0-ary function symbols.

## Extensions by definitions

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

## Examples

* Traditionally, the first-order set theory ZF has $=$ (equality) and $\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 $\subseteq$, the constant $\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 $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
       $\forall x(x\times e=x{\text{ and }}e\times x=x)$,
    and what we obtain is an extension by definitions $T'$ of $T$. Then in $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 $T''$ obtained from $T'$ by adding a unary function symbol $f$ and the axiom
       $\forall x(x\times f(x)=e{\text{ and }}f(x)\times x=e)$
    is an extension by definitions of $T$. Usually, $f(x)$ is denoted $x^{-1}$.