Go up to A Defining New NotionsGo forward to A.2 Explicit Predicate Definitions

## A.1 Preliminaries

In mathematics, a formal description is called a definition; a definition constructs a new theory from a given one.

Definition 135 (Theory) A  theory (Theorie) consists of a set of constants and a set of formulas that only use constants from the given set. We call these formulas the  axioms (Axiome) of the theory.

The axioms of a theory express those propositions that are stipulated to be true; from these propositions other true propositions can be derived.

Example
• The theory of Peano Arithmetic consists of constants
0 (zero), ' (successor)
and the axioms that are stated in Section Natural Numbers.
• The theory of sets has a single binary predicate constant
in  (is element of)
and the Axioms of Zermelo and Fraenkel.
• The theory of real numbers has constants
0, 1, +, *, <=
and the axioms that are stated in Section Real Numbers.
• The theory of lists has the constants
and axioms like (forall e, l: head(cons(e, l))=e).

Definition 136 (Definition) A  definition (Definition) is a statement that introduces into a theory a new constant and new axioms such that from the extended set of axioms no formula can be derived that could not be derived from the original axioms (provided that this formula only uses constants from the original theory).

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

Example  The axioms of the set theory demand the existence of a set that does not contain any elements. We introduce the constant 0 to denote this set. We may conclude (forall x: x not  in 0).

In the following, we will discuss various techniques to write definitions.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999