Extension by definition

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: • \psi\leftrightarrow\psi^\ast is provable in T', and • 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 \psi, 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. Let \psi be any atomic formula of T'. We define 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 such that f does not occur in the terms t_i, and let \chi be obtained from \psi by 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: • \psi\leftrightarrow\psi^\ast is provable in T', and • 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 ×. 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 \times e = x \land e \times 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 \times f(x)=e \land f(x) \times x=e) :is an extension by definitions of T. Usually, f(x) is denoted x^{-1}. ==See also==