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:
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
.