\renewcommand\cfile{thms.tex}

\subsection{A Decision Procedure for Classical Propositional Calculus}
\label{decproc}
In most systems for propositional calculus it is straightforward to
describe a decision procedure, and this is so for the subset of
\dRA\ involving purely Boolean expressions.
We now describe how such a decision procedure was implemented
in Isabelle.

For the Boolean logical operators, the logical introduction rules
will always enable a displayed formula
to be broken down (in a backwards proof).
That is, for every binary operator \emph{op}, there are rules
whose conclusions are
$A \ op\  B \vdash X$ and $X \vdash A \ op\  B $, and
similarly for every unary or constant formula operator.
Note that it is the variant forms \verb:andS: and \verb:orA: of the rules
($\land \vdash$) and ($\vdash \lor$) that have this property.

Therefore, all the Boolean formula operators can be replaced
by structural operators.  
Typically, this will result in several subgoals, not just one.
Then the display postulates could be used to remove all instances of
$*$ (which will move structures from one side of the turnstile to the other),
to give sequents of the form 
$A,B,\ldots \vdash C,D,\ldots$.
If $A,B,C,D,\ldots$ are assumed to stand for primitive propositions,
then there are two cases.
Firstly,
if any such variable appears on both sides of the turnstile in some subgoal,
then that subgoal is a classical tautology.

Otherwise, in a subgoal $X \vdash Y$ in which no 
variable appears on both sides of the turnstile,
all the antecedent variables could be assigned $\top$,
and all the succedent ones $\bot$. 
This would falsify the formula
$\tau(X \vdash Y)$ 
(see \cite{dRA}, \S4,
for the definition of $\tau$\index{tau@$\tau$|textbf}, which
gives the correspondence between structural operators and formula
operators).
Since it can be checked that the logical introduction rules
for the Boolean operators
(again, using \verb:andS: and \verb:orA: in place of
($\land \vdash$) and ($\vdash \lor$))
have the property
that $\tau$(conclusion) is true if and only if every $\tau$(premise) is
true (and the display postulates also have this property),
this assignment also falsifies the sequent originally given.

The procedure implemented works a little differently from this.
Firstly, all logical operators are removed.
Secondly, all subgoals are scanned for a repeated simple formula variable $A$,
appearing both in an antecedent position and in a succedent position.
When such a pair is found, the monotonicity rules
are used to remove extraneous variables.
The result may be 
$A \vdash A$, which is proved using \verb:idf:,
or it may be more complex, like
$*(A, *A) \vdash I$.
Various rules
such as the display postulates,
distributive and identity rules,
are used to reduce the more complex cases to 
$A \vdash A$.

This is implemented as \ttdef{weak\_tac} \insrc{weak.tac}.
The implementation also handles terms containing the
(structural) converse operator $\bullet$, so it can prove,
automatically, a sequent like
$*(\bullet A, \bullet *A) \vdash I$.

\subsection{Theorems proved using Isabelle}
We give some examples of theorems and derived rules
that have been proved in \dRA, using Isabelle.

Chin \& Tarski \cite{CT} give a number of results whose proof is
far from simple.  For example, their Theorem 2.7 is
$$ (a \circ b) \land c \vdash a \circ ((\smile a \circ c) \land b) $$
This is proved \insrc{CT.ML} as \ttdef{CT27}.
It is also possible to state a purely structural version 
of this theorem (as a structural rule)
\begin{center}
\slrule
{X; ((\bullet X; Z), Y) \vdash W}
{(X; Y), Z \vdash W}
\end{center}
This is derived as \ttdef{CT27sr}.
The manner of proving these results was to copy the proof in \cite{CT};
this gave a proof containing a number of cuts, which were then 
eliminated using the procedure described in \ch{cut}.
(Later the \dRA\ proof was simplified substantially).

Chin \& Tarski \cite{CT} Theorem 2.11 is
$$(r \circ s) \land (t \circ u)
\vdash (r \circ ((\smile r \circ t) \land (s \circ \smile u))) \circ
u
$$
which is proved as \ttdef{CT211}.
Again, there is a structural rule version,
\begin{center}
\slrule
{(U; ((\bullet U; W), (V; \bullet X))); X \vdash Z}
{(U; V), (W; X) \vdash Z}
\end{center}
which is derived as \ttdef{CT211sr}.

The Dedekind rule (\cite{RALL}, \S5.3; \cite{RALF}, \S2.1) is
$$
(Q \circ R) \land S
\vdash (Q \land (S \circ \smile R)) \circ (R \land (\smile Q \circ S))
$$
It is proved as \ttdef{ded} \insrc{ded.ML}.
The structural rule version
\begin{center}
\slrule
{(X, (Z; \bullet Y)); (Y, (\bullet X; Z)) \vdash W}
{(X; Y), Z \vdash W}
\end{center}
is derived as \ttdef{dedsr}.

Some interesting theorems were proved in \texttt{peirce.ML},
which can in fact be used to prove
some of the theorems mentioned in \S\ref{Peirce}.
Again, they can be proved in the form of structural rules.
Firstly, we have
\begin{center} \hfill
\invrule {((X; Y), E); Z \vdash W } { ((X, \bullet Y); I), Z \vdash W}
(\ttdl{thab}) \hfill \mbox{}
\end{center}

Secondly we have two results related to it.

\begin{center} \hfill
\invrule { (X, E); (Y, Z) \vdash W } { ((X, E); Y), Z \vdash W }
(\ttdl{th78sr}) \hfill
\invrule { (X; I), (Y; Z) \vdash W } { ((X; I), Y); Z \vdash W }
(\ttdl{th56sr}) \hfill \mbox{}
\end{center}
These results show an interesting similarity between the 
Boolean and relational ``times'' operators, `,' and `;',
and their identities, $I$ and $E$.
We show an intuitive explanation of these results.
We have two simpler results (which can be derived by
setting $Y = I$ in \texttt{th78sr},
and $Y = E$ in \texttt{th56sr}).
\begin{center}
  \hfill
(s78\label{s78})
\invrule { (X, E); Z \vdash W } { ((X, E); I), Z \vdash W }
  \hfill
(s56\label{s56})
\invrule { (X; I), Z \vdash W } { ((X; I), E); Z \vdash W }
  \hfill \mbox{}
\end{center}
(Alternatively, we can derive these two results by setting
$Y = E$ and $Y = I$ in \texttt{thab}.)
That is (for (s78)), relational pre-multiplication of $Z$
by $(X,E)$ is the same as Boolean pre-multiplication of $Z$
by $((X, E);I)$. 
Viewed in this way, the main result \texttt{th78sr} 
follows from the associativity of Boolean multiplication.
Similarly, the main result \texttt{th56sr} 
follows from the associativity of relational multiplication.

These results have the following corollaries, which
give examples of cases where the
Boolean product and the relational product of two quantities are equal.
\begin{center}
  \hfill
\invrule { (X, E); (E, Z) \vdash W } { (X, E), (E, Z) \vdash W }
(\ttdl{cor78i}) \hfill
\invrule { (X; I), (I; Z) \vdash W } { (X; I); (I; Z) \vdash W }
(\ttdl{cor56i}) \hfill \mbox{}
\end{center}
These corollaries are obtained by
setting $Y = E$ in \texttt{th78sr},
and $Y = I$ in \texttt{th56sr}.

\subsection{Proving the RA axioms} \label{provRA}

We show, informally,
how any result provable in \RA\ can be proved in \dRA, in Isabelle.
(This shows the completeness of \dRA\ with respect to \RA,
which is Theorem 6 of Gor\'e \cite{dRA}).
Firstly, following \cite{dRA}, Theorem 6,
we let $A=B$ mean $A \vdash B$ and $B \vdash A$;
more formally, we introduce the following rules
\begin{center}
\slrule {A \vdash B \quad B \vdash A } { A = B}(\ttdef{eqI})
\qquad
\slrule {A = B } { A \vdash B}(\ttdef{eqD1})
\qquad
\slrule {A = B } { B \vdash A}(\ttdef{eqD2})
\end{center}
\seesrc{RA.thy}.
Note that this equality is reflexive, symmetric and transitive,
proved as \ttdef{eqrefl}, \ttdef{eqsym} and \ttdef{eqtrans} \insrc{RA.ML}.
We define $A \leq B$ as $(A \land B) = A$, as in \RA;
it is then proved, as the theorem \ttdef{lett}, that 
$A \leq B \iff A \vdash B$.

Then the \RA\ axioms can be proved; (RA2) to (RA8) are proved in
\src{RA.ML}\@.
Axiom (RA1), which says that the logical operators form a Boolean algebra,
can be seen to follow from the fact that \dRA\
%Gentzen sequent calculus
contains classical propositional logic (see \S\ref{decproc}).

In using the \RA\ axioms we would implicitly rely on the 
equality operator $=$ being symmetric and transitive,
which we proved, as indicated above.
We would also use the fact that equality in
\RA\ permits substitution of equals.
That is, suppose $C[A]$ and $C[B]$ are formulae
such that $C[B]$ is obtained from $C[A]$ by replacing some occurrences of $A$
by $B$. 
If we now prove in \RA\ that
$A = B$ and $C[A] = D$ then 
we could deduce $C[B] = D$ by substituting $B$ for $A$.
%from \RA\ equations $A = B$ and $C[A] = D$, 
%one deduces $C[B] = D$.

To show that this can be done in \dRA\
we have to use induction on the structure of $C[\cdot]$. 
Each induction step 
uses one of these derived results shown below, proved as \ttdef{eqcs}
in \src{RA.ML}.
\vspace{-2.0ex}
\begin{center} \small
\begin{tabular}{c@{\quad}c@{\quad}c}
\slrule {A_1 = A \quad B_1 = B} {A_1 \lor B_1 = A \lor B} (\ttdef{eqc\_or}) &
\slrule {A_1 = A \quad B_1 = B} {A_1 \land B_1 = A \land B}
(\ttdef{eqc\_and}) &
\slrule {A_1 = A } {\lnot A_1 = \lnot A } (\ttdef{eqc\_not}) 
\label{eqcs}
\\ & \\
\slrule {A_1 = A \quad B_1 = B} {A_1 + B_1 = A + B} (\ttdef{eqc\_rs}) &
\slrule {A_1 = A \quad B_1 = B} {A_1 \circ B_1 = A \circ B}
(\ttdef{eqc\_comp}) &
\slrule {A_1 = A } {\smile A_1 = \smile A } (\ttdef{eqc\_conv}) 
\end{tabular}
\end{center}

In a sense, this inductive proof could be demonstrated 
in any particular case
by use of the tactic \ttdef{idf\_tac}, described in \S\ref{otm}.
A proof would look like this, where `\ddag' denotes a number of sequents 
of the form $A \vdash A$, and where `=' denotes either
(\texttt{eqD1}) or (\texttt{eqD2}).
\vspace{-2.0ex}
\vpf
\begin{center}
\bpf
\A "$A = B $"
\U "$B \vdash A $" "="%"(\texttt{eqD2})" 
\A "\ddag"
\B "$C[B] \vdash C[A]$" "(\texttt{idf\_tac})"
\A "$C[A] = D$"
\U "$C[A] \vdash D$" "="%"(\texttt{eqD1})"
\B "$C[B] \vdash D$" "(cut)"

\A "$C[A] = D$"
\U "$D \vdash C[A] $" "="%"(\texttt{eqD2})" 
\A "$A = B $"
\U "$A \vdash B $" "="%"(\texttt{eqD1})" 
\A "\ddag"
\B "$C[A] \vdash C[B] $" "(\texttt{idf\_tac})"
\B "$D \vdash C[B]$" "(cut)"

\B "$C[B]=D$" "(\texttt{eqI})"
\epf
\end{center}

\subsection{Peirce algebras} \label{Peirce}

In \cite{BBS}, \S3.3, Brink, Britz \& Schmidt 
show the relationship between Peirce algebras and relation algebras.
A Peirce algebra consists of a relation algebra
$\mathcal R$ and a Boolean algebra $\mathcal B$, interacting in a
defined way.
It is shown that for any Peirce algebra, the 
Boolean algebra $\mathcal B$ is isomorphic to 
each of 
$$\mathcal I = \{R \in \mathcal R \;|\; R \leq \1 \} \qquad
\mathcal J = \{R \in \mathcal R \;|\; R = R \circ \top \}$$

We have proved a number of theorems in \dRA\ relevant 
to showing that 
$\mathcal I$ and $\mathcal J$
are isomorphic; they are found \insrc{peirce.ML}.

Firstly we redefine 
$\mathcal I$ and $\mathcal J$ as
$$\mathcal I' = \{A \land \1 \;|\; A \in \mathcal R \} \qquad
\mathcal J' = \{A \circ \top \;|\; A \in \mathcal R \}$$
That $\mathcal J = \mathcal J' $ is justified by theorems 
\ttdef{thj} and \ttdef{thjr}.
That $\mathcal I = \mathcal I' $ is similar, but simpler.

If we define mappings
$f : \mathcal I' \to \mathcal J'$
and $g : \mathcal J' \to \mathcal I'$ by
$f(R) = R \circ \top$ and \mbox{$g(R) = R \land \1$,}
then \ttdef{th1} and \ttdef{th2} give
$f(g(R)) = R$ for $R \in \mathcal J'$;
\ttdef{th3} and \ttdef{th4} give
$g(f(R)) = R$ for $R \in \mathcal I'$.
These are essentially Lemmas 3.5 and 3.7 of \cite{BBS}.

This shows that $f$ and $g$ are bijections.
To show that 
$\mathcal I$ and $\mathcal J$ are isomorphic as Boolean algebras,
it remains only to show that $g$ is a homomorphism of Boolean algebras.
This is straightforward once we define
$\lnot$ on ${\mathcal I}$ by
\mbox{$\lnot_{\mathcal I} (A \land \1) = 
\lnot_{\mathcal R} A \land \1$,}
ie, for $R \in \mathcal I$, 
$\lnot_{\mathcal I} R = 
\1 \setminus R$,
where $ \setminus $ denotes set difference.

\renewcommand\cfile{}