previous up next
Go up to A Defining New Notions
Go forward to A.2 Explicit Predicate Definitions
RISC-Linz logo

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.


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

previous up next