# Extension by definitions

(Redirected from Extension by definition)

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 $\phi$, 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$.

If $\psi$ is an atomic formula of $T'\,$, define a 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$, and let $\chi$ be obtained from $\psi$ be 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 $\cdot$. 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\cdot e=x\text{ and }e\cdot 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\cdot f(x)=e\text{ and }f(x)\cdot 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)