Notations and preliminaries

In the following we shall use the following symbols and abbreviations: $\omega$ denotes the set of natural numbers. $=_{def}$ is the symbol for a definition. $Pow$ is the power set function: if $X$ is any set then $Pow(X)$ is the powerset of $X$. 'wrt' abbreviates 'with respect to', and 'iff' stands for 'if and only if'.

Let $X$ be any set and $R\subseteq X\times X$ a binary relation on $X$. Then $R^+$ denotes the transitive closure and $R^*$ the reflexive, transitive closure of $R$. If $R$ and $S$ are two relations on $X$ then $R;S$ denotes the composition of the two relations, i.e., $(s,t)\in R;S$ iff there exists a $u$ such that $(s,u)\in R$ and $(u,t)\in S$.

Let $R\subseteq X\times X$ a binary relation on a set $X$. We will be considering relations having certain algebraic properties:

• $R$ is reflexive iff for all $x\in X$, $xRx$.

• $R$ is transitive iff for all $x,y,z\in X$, if $xRy$ and $yRz$ then $xRz$.

• $R$ is symmetric iff for all $x,y\in X$, if $xRy$ then $yRz$.

• $R$ is serial iff for all $x\in X$ there is a $y\in X$ such that $xRy$.

• $R$ is Euclidean iff for all $x,y,z\in X$, if $xRy$ and $xRz$ then $yRz$.

• $R$ is directed iff for all $x,y,z\in X$, if $xRy$ and $xRz$ then there is some $t\in X$ such that $yRt$ and $zRt$.

The relation $R$ 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 ($\lnot$), conjunction ($\land$), disjunction ($\lor$), implication ($\to$), and material equivalence ( $\leftrightarrow$), possibly together with additional (non-extensional) connectives, to form more complex formulae.^1.4 Atomic formulae will be denoted by $\phi, \phi_0, \phi_1, \ldots$. To denote arbitrary formulae we use $\alpha, \beta, \gamma, \ldots$, possibly with indexes. We take negation and implication as basic connectives. Disjunction, conjunction, and material equivalence are introduced as abbreviations:

$$(\alpha \lor \beta) =_{def} \lnot \alpha \to \beta$$

$$(\alpha \land \beta) =_{def} \lnot (\lnot \alpha \lor \lnot \beta)$$

$$(\alpha \leftrightarrow \beta) =_{def} ((\alpha \to \beta) \land (\beta \to \alpha))$$

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 $\mathcal{L}$ be a formal language which contains the above-mentioned Boolean connectives. A logic $\Lambda$ 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 $\vdash_{\Lambda}\alpha$ to indicate that $\alpha$ is a $\Lambda$-theorem. If $\Gamma\subseteq \mathcal{L}$ and $\alpha\in \mathcal{L}$ then we say that $\alpha$ is $\Lambda$-deducible from $\Gamma$, denoted $\Gamma \vdash_{\Lambda} \alpha$, if there exist $\avec{\beta}{,}{n} \in \Gamma$ such that $\vdash_{\Lambda} \avec{\beta}{\land}{n} \to \alpha$. (In the case $n=0$, this means that $\vdash_{\Lambda}\alpha$.) We write $\Gamma\not\vdash_{\Lambda}\alpha$ if $\alpha$ is not $\Lambda$-deducible from $\Gamma$. A set $\Gamma\subseteq \mathcal{L}$ is $\Lambda$-consistent if there is no formula $\alpha$ such that $\Gamma\not\vdash_{\Lambda} (\alpha \land \lnot \alpha)$. The deductive closure of a set $\Gamma\subseteq \mathcal{L}$ with respect to the logic $\Lambda$ is defined as:

$$Cn_{\Lambda}(\Gamma) =_{def} \{ \alpha \in \mathcal{L}: \Gamma \vdash_{\Lambda} \alpha \}$$

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 $\alpha\in \mathcal{L}$ is valid in some model $M$ (for the language $\mathcal{L}$), in symbol $M\models \alpha$. A formula $\alpha$ is called valid with respect to some class $\mathcal{C}$ of models, denoted $\models_{\mathcal{C}}\alpha$, 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 $\Lambda$ is determined by a class $\mathcal{C}$ of models just in case it is sound and complete wrt $\mathcal{C}$, i.e., $\vdash_{\Lambda}\alpha$ iff $\models_{\mathcal{C}}\alpha$.