## 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
nil, cons, isnil, head, tail

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