Inmathematical logic, more specifically in theproof theory offirst-order theories, anextension by definition formalizes the introduction of a new symbol by means of adefinition. For example, it is common in naiveset theory to introduce a symbol${\displaystyle \mathrm{\varnothing }}$ for theset 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 \mathrm{\varnothing }}$ and the newaxiom${\displaystyle \mathrm{\forall }x(x\notin \mathrm{\varnothing })}$, meaning "for allx,x is not a member of${\displaystyle \mathrm{\varnothing }}$". 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 aconservative extension of the old one.

Let${\displaystyle T}$ be afirst-order theory and${\displaystyle \varphi (x_1,\dots ,x_n)}$ aformula of${\displaystyle T}$ such that${\displaystyle x_1}$, ...,${\displaystyle x_n}$ are distinct and include the variablesfree in${\displaystyle \varphi (x_1,\dots ,x_n)}$. Form a new first-order theory${\displaystyle T^{\prime }}$ from${\displaystyle T}$ by adding a new${\displaystyle n}$-ary relation symbol${\displaystyle R}$, thelogical axioms featuring the symbol${\displaystyle R}$ and the new axiom

${\displaystyle \mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_n(R(x_1,\dots ,x_n)\leftrightarrow \varphi (x_1,\dots ,x_n))}$,

called thedefining axiom of${\displaystyle R}$.

If${\displaystyle \psi }$ is a formula of${\displaystyle T^{\prime }}$, 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 \varphi (t_1,\dots ,t_n)}$ (changing thebound variables in${\displaystyle \varphi }$ if necessary so that the variables occurring in the${\displaystyle t_i}$ are not bound in${\displaystyle \varphi (t_1,\dots ,t_n)}$). Then the following hold:

1. ${\displaystyle \psi \leftrightarrow {\psi }^{\ast }}$ is provable in${\displaystyle T^{\prime }}$, and
2. ${\displaystyle T^{\prime }}$ is aconservative extension of${\displaystyle T}$.

The fact that${\displaystyle T^{\prime }}$ 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 atranslation 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 \varphi (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 \varphi (y,x_1,\dots ,x_n)}$. Assume that we can prove

${\displaystyle \mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_n\mathrm{\exists }!y\varphi (y,x_1,\dots ,x_n)}$

in${\displaystyle T}$, i.e. for all${\displaystyle x_1}$, ...,${\displaystyle x_n}$, there exists a uniquey such that${\displaystyle \varphi (y,x_1,\dots ,x_n)}$. Form a new first-order theory${\displaystyle T^{\prime }}$ from${\displaystyle T}$ by adding a new${\displaystyle n}$-aryfunction symbol${\displaystyle f}$, the logical axioms featuring the symbol${\displaystyle f}$ and the new axiom

${\displaystyle \mathrm{\forall }{x}_1\dots \mathrm{\forall }{x}_n\varphi (f(x_1,\dots ,x_n),x_1,\dots ,x_n)}$,

called thedefining axiom of${\displaystyle f}$.

Let${\displaystyle \psi }$ be any atomic formula of${\displaystyle T^{\prime }}$. 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 \mathrm{\forall }z(\varphi (z,t_1,\dots ,t_n)\to {\chi }^{\ast })}$

(changing the bound variables in${\displaystyle \varphi }$ if necessary so that the variables occurring in the${\displaystyle t_i}$ are not bound in${\displaystyle \varphi (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^{\prime }}$, and
2. ${\displaystyle T^{\prime }}$ is aconservative extension of${\displaystyle T}$.

The formula${\displaystyle {\psi }^{\ast }}$ is called atranslation 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^{\prime }}$ obtained from${\displaystyle T}$ by successive introductions of relation symbols and function symbols as above is called anextension by definitions of${\displaystyle T}$. Then${\displaystyle T^{\prime }}$ is a conservative extension of${\displaystyle T}$, and for any formula${\displaystyle \psi }$ of${\displaystyle T^{\prime }}$ we can form a formula${\displaystyle {\psi }^{\ast }}$ of${\displaystyle T}$, called atranslation of${\displaystyle \psi }$ into${\displaystyle T}$, such that${\displaystyle \psi \leftrightarrow {\psi }^{\ast }}$ is provable in${\displaystyle T^{\prime }}$. Such a formula is not unique, but any two of them can be proved to be equivalent inT.

In practice, an extension by definitions${\displaystyle T^{\prime }}$ ofT is not distinguished from the original theoryT. In fact, the formulas of${\displaystyle T^{\prime }}$ can be thought of asabbreviating their translations intoT. 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 theoryZF 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 \mathrm{\varnothing }}$, the unary function symbolP (thepower set operation), etc. All of these symbols belong in fact to extensions by definitions of ZF.
• Let${\displaystyle T}$ be a first-order theory forgroups in which the only primitive symbol is the binary product ×. InT, we can prove that there exists a unique elementy such thatx × y =y × x =x for everyx. Therefore we can add toT a new constante and the axiom

${\displaystyle \mathrm{\forall }x(x\times e=x\wedge e\times x=x)}$,

and what we obtain is an extension by definitions${\displaystyle T^{\prime }}$ of${\displaystyle T}$. Then in${\displaystyle T^{\prime }}$ we can prove that for everyx, there exists a uniquey such thatx × y =y × x =e. Consequently, the first-order theory${\displaystyle T^{″}}$ obtained from${\displaystyle T^{\prime }}$ by adding a unary function symbol${\displaystyle f}$ and the axiom

${\displaystyle \mathrm{\forall }x(x\times f(x)=e\wedge f(x)\times x=e)}$

is an extension by definitions of${\displaystyle T}$. Usually,${\displaystyle f(x)}$ is denoted${\displaystyle x^{-1}}$.

• Conservative extension
• Definite description
• Epsilon calculus
• 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)

• Mathematical logic
• Proof theory

• Articles with short description
• Short description matches Wikidata