# 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 which 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:

1. $\psi \leftrightarrow \psi ^{\ast }$  is provable in $T'$ , and
2. $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 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:

1. $\psi \leftrightarrow \psi ^{\ast }$  is provable in $T'$ , and
2. $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}$ .

## Bibliography

• 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)