Extension by definitions

Let ${\displaystyle T}$  be a first-order theory and ${\displaystyle \phi (x_{1},\dots ,x_{n})}$ aformulaof${\displaystyle T}$  such that ${\displaystyle x_{1}}$ , ..., ${\displaystyle x_{n}}$  are distinct and include the variables freein${\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 axiomof${\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 variablesin${\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 extensionof${\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 translationof${\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 axiomof${\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 extensionof${\displaystyle T}$ .

The formula ${\displaystyle \psi ^{\ast }}$  is called a translationof${\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 definitionsof${\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 translationof${\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'}$ ofT 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{\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}}$ .

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