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 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{\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)