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.

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^{\prime }}$Zdroj:https://en.wikipedia.org?pojem=Extension_by_definitions
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.