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 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 and the new axiom , meaning "for all x, x is not a member of ". 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 symbolsEdit

Let   be a first-order theory and   a formula of   such that  , ...,   are distinct and include the variables free in  . Form a new first-order theory   from   by adding a new  -ary relation symbol  , the logical axioms featuring the symbol   and the new axiom

 ,

called the defining axiom of  .

If   is a formula of  , let   be the formula of   obtained from   by replacing any occurrence of   by   (changing the bound variables in   if necessary so that the variables occurring in the   are not bound in  ). Then the following hold:

  1.   is provable in  , and
  2.   is a conservative extension of  .

The fact that   is a conservative extension of   shows that the defining axiom of   cannot be used to prove new theorems. The formula   is called a translation of   into  . Semantically, the formula   has the same meaning as  , but the defined symbol   has been eliminated.

Definition of function symbolsEdit

Let   be a first-order theory (with equality) and   a formula of   such that  ,  , ...,   are distinct and include the variables free in  . Assume that we can prove

 

in  , i.e. for all  , ...,  , there exists a unique y such that  . Form a new first-order theory   from   by adding a new  -ary function symbol  , the logical axioms featuring the symbol   and the new axiom

 ,

called the defining axiom of  .

Let   be any formula of  . We define formula   of   recursively as follows. If the new symbol   does not occur in  , let   be  . Otherwise, choose an occurrence of   in   such that   does not occur in the terms  , and let   be obtained from   by replacing that occurrence by a new variable  . Then since   occurs in   one less time than in  , the formula   has already been defined, and we let   be

 

(changing the bound variables in   if necessary so that the variables occurring in the   are not bound in  ). For a general formula  , the formula   is formed by replacing every occurrence of an atomic subformula   by  . Then the following hold:

  1.   is provable in  , and
  2.   is a conservative extension of  .

The formula   is called a translation of   into  . As in the case of relation symbols, the formula   has the same meaning as  , but the new symbol   has been eliminated.

The construction of this paragraph also works for constants, which can be viewed as 0-ary function symbols.

Extensions by definitionsEdit

A first-order theory   obtained from   by successive introductions of relation symbols and function symbols as above is called an extension by definitions of  . Then   is a conservative extension of  , and for any formula   of   we can form a formula   of  , called a translation of   into  , such that   is provable in  . 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   of T is not distinguished from the original theory T. In fact, the formulas of   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.

ExamplesEdit

  • Traditionally, the first-order set theory ZF has   (equality) and   (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  , the constant  , the unary function symbol P (the power set operation), etc. All of these symbols belong in fact to extensions by definitions of ZF.
  • Let   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
 ,
and what we obtain is an extension by definitions   of  . Then in   we can prove that for every x, there exists a unique y such that x×y=y×x=e. Consequently, the first-order theory   obtained from   by adding a unary function symbol   and the axiom
 
is an extension by definitions of  . Usually,   is denoted  .

BibliographyEdit

  • 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)