\renewcommand\cfile{madint.tex}

Following related work by Wadge \cite{Wadge},
Hennessy \cite{Hennessy} and Sch\"onfeld \cite{Schonfeld},
Maddux \cite{seqra} deals with relation algebras in terms of the relations
and, in a sense, of the elements of the set $U$.
He gives a sequent calculus in which variables
({\bfseries point variables})\index{point variable|textbf}
appear in the place of elements of $U$.
Thus, for example, his rules for introducing the conjunction operator
(which we write ``$\land$") are
$$ \frac {\Gamma, x[R]y, x[S]y \vdash \Delta} {\Gamma, x[R \land S]y \vdash \Delta}
(\land \vdash )
\quad \textrm{ and } \quad 
\frac {\Gamma \vdash \Delta, x[R]y \qquad \Gamma \vdash \Delta, x[S]y}
{\Gamma \vdash \Delta, x[R \land S]y}
(\vdash \land )$$
If the $x$ and $y$ are removed from these rules, they look like
rules of the Gentzen sequent calculus for propositional logic,
which are themselves
easily derivable in the Display Logic system \dRA.
However the rules for introducing the relation composition operator
(which we write $\circ$) are
$$ \frac {\Gamma, x[R]y, y[S]z \vdash \Delta} {\Gamma, x[R \circ S]z \vdash \Delta}
(\circ \vdash )
\quad \textrm{ and } \quad 
\frac {\Gamma \vdash \Delta, x[R]y \qquad \Gamma \vdash \Delta, y[S]z}
{\Gamma \vdash \Delta, x[R \circ S]z}
(\vdash \circ ) $$ 
with the restriction that $y$ cannot appear in the conclusion of
($\circ \vdash $).
We examine how to represent these rules, and proofs using them, in \dRA.

In \cite{seqra}, Maddux defines
{\bfseries \boldmath $n$-sequents}\index{n-sequent@$n$-sequent|textbf},
which are sequents containing at most $n$ distinct point variables, and
{\bfseries \boldmath $n$-proofs}\index{n-proof@$n$-proof|textbf},
which contain only $n$-sequents.
He shows that the set of 4-provable sequents characterises the class of
relation algebras,
that is, the theorems of a relation algebra are exactly the 
4-provable sequents.
Likewise he shows that the set of $\omega$-provable sequents (ie, results
which are $n$-provable for some integer $n$) characterise the representable
relation algebras.

In this chapter we show how to translate a 4-proof in
Maddux's point variable calculus,
which we call \M\index{M@\M|textbf},
into a proof in \dRA.
Since proofs in the point variable calculus are often easier than
in \dRA, this will provide a means of constructing proofs in \dRA.
It will also provide an alternative proof that 
4-provable sequents in \M\ are theorems of \RA.

The axiom and rules of inference of \M\ are listed in \fig{M}.
It should be noted that the terms to the left and right of $\vdash$ are
\emph{sets}, so, for example, 
``$\Gamma, x[R]y$'' stands for ``$\Gamma \cup \{ x[R]y \}$''.
This means that, in \M, the ordering within
``$\Gamma, x[R]y$'' is not significant, and that a repetition of a formula
may be deleted.

\begin{figure}[htbp]
\label{fig:M}
\begin{center}
Axioms

\vspace{1.0ex} 
\hfill
$\displaystyle {\Gamma, x[R]y \vdash \Delta, x[R]y} $ \hfill
$\displaystyle {\Gamma, x[\bot] y \vdash \Delta} $ \hfill
$\displaystyle {\Gamma \vdash \Delta, x[\top] y} $ \hfill
$\displaystyle {\Gamma \vdash \Delta, x[\1]x} $ \hfill \mbox{}
\vspace{2.0ex} 

Rules of Inference

\begin{tabular}{c@{\hspace{15mm}}c}
 & \\
$\displaystyle
\frac {\Gamma \vdash \Delta}
{\Gamma, \Gamma' \vdash \Delta} 
(M \vdash)
$ & $\displaystyle
\frac {\Gamma \vdash \Delta}
{\Gamma \vdash \Delta, \Delta'} 
(\vdash M)
$\\ & \\ $\displaystyle
\frac {\Gamma \vdash \Delta, \delta \qquad \Gamma', \delta \vdash \Delta'}
{\Gamma, \Gamma' \vdash \Delta, \Delta'} 
$(cut) & $\displaystyle
\frac {\Gamma, x[R]y\vdash \Delta } {\Gamma, x[R]z, z[\1]y \vdash \Delta}
$(Id) \\ & \\ $\displaystyle
\frac {\Gamma \vdash \Delta, x[R]y } {\Gamma, x [\lnot R]y \vdash \Delta} 
(\lnot \vdash)
$ & $\displaystyle
\frac {\Gamma, x[R]y \vdash \Delta } {\Gamma \vdash \Delta, x [\lnot R]y} 
(\vdash \lnot )
$\\ & \\ $\displaystyle
\frac {\Gamma, x[R]y \vdash \Delta } {\Gamma, y [\smile R]x \vdash \Delta} 
(\smile \vdash)
$ & $\displaystyle
\frac {\Gamma \vdash \Delta, x[R]y } {\Gamma \vdash \Delta, y [\smile R]x} 
(\vdash \smile )
$\\ & \\ $\displaystyle
\frac {\Gamma, x[R]y \vdash \Delta \qquad \Gamma, x[S]y \vdash \Delta}
{\Gamma, x[R \lor S]y \vdash \Delta} 
(\lor \vdash)
$ & $\displaystyle
\frac {\Gamma\vdash \Delta, x[R]y, x[S]y } {\Gamma \vdash \Delta, x[R \lor S]y}
(\vdash \lor)
$\\ & \\ $\displaystyle
\frac {\Gamma, x[R]y, x[S]y \vdash \Delta} {\Gamma, x[R \land S]y \vdash \Delta}
(\land \vdash)
$ & $\displaystyle
\frac {\Gamma \vdash \Delta, x[R]y \qquad \Gamma \vdash \Delta, x[S]y}
{\Gamma \vdash \Delta, x[R \land S]y} 
(\vdash \land)
$\\ & \\ $\displaystyle
\frac {\Gamma, x[R]y, y[S]z \vdash \Delta} {\Gamma, x[R \circ S]z \vdash \Delta}
(\circ \vdash )
$ & $\displaystyle
\frac {\Gamma \vdash \Delta, x[R]y \qquad \Gamma \vdash \Delta, y[S]z}
{\Gamma \vdash \Delta, x[R \circ S]z} 
(\vdash \circ )
$ \\ ($y$ cannot appear in $\Gamma$ or $\Delta$) &
\end{tabular}
\end{center}
\caption{The system \M\ of Maddux}
\end{figure}

We provide an intuitive explanation of the 
($\circ \vdash $) rule and the restriction on it.
The sequent $ {\Gamma, x[R]y, y[S]z \vdash \Delta} $ stands for
$$\forall x,y,z,\ldots 
  (\Gamma \:\&\: x[R]y \:\&\: y[S]z \Rightarrow \Delta) $$
Provided that 
$y$ does not appear in $\Gamma$ or $\Delta$,
this is equivalent to
$$\forall x,z,\ldots 
(\Gamma \:\&\: \exists y ((x,y) \in R \:\&\: (y,z) \in S) \Rightarrow \Delta) $$
When $\circ$ denotes the composition of concrete relations, 
%$ \exists y (x[R]y \:\&\: y[S]z) $
$ \exists y ((x,y) \in R \:\&\: (y,z) \in S) $
is exactly the meaning of 
$ (x,z) \in R \circ S $.

\renewcommand\cfile{}