Go backward to 7 More on RelationsGo up to TopGo forward to B Proving Propositions |

When formulating propositions for a particular domain, it becomes soon cumbersome to commit oneself to the predicates and functions provided by the domain. For instance, while set theory offers a single binary predicate ` in ' that in principle suffices to express all facts about sets, formulas become very large and difficult to understand if they are expressed only with the help of this predicate.

Therefore we need mechanisms that allow us to introduce new predicate and
function constants that capture under a single name properties respectively
objects whose description with the help of the basic notions is rather
large. By this *abstraction (Abstraktion)*, we can refer to a notion just
by its name without having to repeat its description in different contexts
over and over again. If descriptions are similar but not identical, we may
extract by *parameterization (Parameterisierung)* a common core or a more
general notion that is suitable for abstraction.

The new constants may be again used for the introduction of other constants,
thus we can build in an iterative *bottom up (von unten nach oben)*
process new layers of abstractions on top of previously constructed ones.

Actually when formalizing aspects of the real world or specifying problems,
this process typically proceeds *top down (von oben nach unten)*: we
introduce a name for the notion of interest and then construct a description
that reduces this notion to simpler notions. We may use these simpler notions
just as "black boxes" or again describe them in terms of simpler notions
until we reach a level where the notions are sufficiently well
understood. This is in particular the case, if these notions are the
elementary predicates and functions of a formally characterized domain (such
as set theory).

This method of constructing descriptions by *stepwise
refinement (schrittweise Verfeinerung)* is of particular importance in computer
science that has to deal with complex and often only vaguely understood
aspects of the real world.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999