Go up to A Defining New Notions
Go forward to A.2 Explicit Predicate Definitions
In mathematics, a formal description is called a definition; a definition constructs a new theory from a given one.
The axioms of a theory express those propositions that are stipulated to be true; from these propositions other true propositions can be derived.
0 (zero), ' (successor)and the axioms that are stated in Section Natural Numbers.
in (is element of)and the Axioms of Zermelo and Fraenkel.
0, 1, +, *, <=and the axioms that are stated in Section Real Numbers.
nil, cons, isnil, head, tailand axioms like (forall e, l: head(cons(e, l))=e).
A definition just introduces syntactic abbreviations for entities that are already implicitly given (but not explicitly named) by a theory; they do not add any conceptual power to a theory (nor do they remove some).
In the following, we will discuss various techniques to write definitions.