In mathematical logic, more specifically in the proof theory of firstorder 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 that has no member. In the formal setting of firstorder 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.
YouTube Encyclopedic

1/5Views:219 86741 504602275 897100 812

Field Definition (expanded)  Abstract Algebra

MATHEMATICAL SYSTEM  UNDEFINED AND DEFINED TERMS  GRADE 8 MATHEMATICS Q3

CICM2021: The Design of Mathematical Language  Jeremy Avigad

Intro to LaTeX : Learn to write beautiful math equations

Functions  Types of Mapping  Don't Memorise
Transcription
Definition of relation symbols
Let be a firstorder theory and a formula of such that , ..., are distinct and include the variables free in . Form a new firstorder 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:
 is provable in , and
 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 symbols
Let be a firstorder 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 firstorder 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 atomic 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:
 is provable in , and
 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 0ary function symbols.
Extensions by definitions
A firstorder 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.
Examples
 Traditionally, the firstorder 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 firstorder 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 firstorder theory obtained from by adding a unary function symbol and the axiom
 is an extension by definitions of . Usually, is denoted .
See also
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, AddisonWesley Publishing Company (reprinted in 2001 by AK Peters)