Go backward to 7 More on Relations Go up to Top Go forward to B Proving Propositions

A Defining New Notions

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.