In the following we shall use the following symbols and abbreviations: denotes the set of natural numbers. is the symbol for a definition. is the power set function: if is any set then is the powerset of . 'wrt' abbreviates 'with respect to', and 'iff' stands for 'if and only if'.

Let be any set and a binary relation on . Then denotes the transitive closure and the reflexive, transitive closure of . If and are two relations on then denotes the composition of the two relations, i.e., iff there exists a such that and .

Let a binary relation on a set . We will be considering relations having certain algebraic properties:

- is reflexive iff for all , .
- is transitive iff for all , if and
then .
- is symmetric iff for all , if then .
- is serial iff for all there is a such that .
- is Euclidean iff for all , if and then
.
- is directed iff for all , if and
then there is some such that and .

The relation is said to be an equivalence relation if it is reflexive, transitive, and symmetric. It is easy to verify that every reflexive relation is also serial and every reflexive, transitive and Euclidean relation is an equivalence relation. Often the term ``confluent'' is used as a synonym for ``directed''.

To construct a formal language we will start with a countable set of
atomic formulae and use the usual Boolean connectives: negation
(), conjunction (), disjunction (), implication
(), and material equivalence (
), possibly
together with additional (non-extensional) connectives, to form more
complex formulae.^{1.4} Atomic formulae will be
denoted by
. To denote arbitrary
formulae we use
, possibly with
indexes. We take negation and implication as basic
connectives. Disjunction, conjunction, and material equivalence are
introduced as abbreviations:

To omit parentheses where possible we also adopt the convention that the binding powers of the connectives decrease in the following order: negation, conjunction, disjunction, implication, and material equivalence.

Let be a formal language which contains the above-mentioned Boolean connectives. A logic in this language will be defined by specifying a set of axiom schemata and rules of inference. Formulae derivable (or provable) from the axioms using the inference rules of the logic are called theorems. We often identify a logic with the set of its theorems. We write to indicate that is a -theorem. If and then we say that is -deducible from , denoted , if there exist such that . (In the case , this means that .) We write if is not -deducible from . A set is -consistent if there is no formula such that . The deductive closure of a set with respect to the logic is defined as:

The semantic counterpart of the provability concept is the concept of validity. We shall define precisely the notion of a model for a formal language and the concept of validity in a model, i.e., we shall specify when a formula is valid in some model (for the language ), in symbol . A formula is called valid with respect to some class of models, denoted , if it is valid in all models of that class. A logic is said to be sound with respect to a class of models if and only if all of its theorems are valid wrt that class of models. It is complete wrt a class of models iff all valid formulae of that class of models are theorems of the logic. We say that a logic is determined by a class of models just in case it is sound and complete wrt , i.e., iff .