# 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 ${\displaystyle \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 ${\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.

## Definition of relation symbols

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.

## Definition of function symbols

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 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.

## Extensions by definitions

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.

## Examples

• 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{\text{ and }}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{\text{ and }}f(x)\times x=e)}$
is an extension by definitions of ${\displaystyle T}$ . Usually, ${\displaystyle f(x)}$  is denoted ${\displaystyle 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)