\renewcommand\cfile{gord.tex}

Gordeev \cite{Gor} has proposed a system of rules for rewriting equations
of the form $F = \top$ (where $F$ is a formula and
$\top$ is the unique largest element).
These are a mixture of some rules which may rewrite an arbitrary part of the 
formula $F$, and others which may be applied to rewrite
only the whole of $F$, or,
when $F$ is a conjunction, one of the conjuncts of $F$.
It is therefore a system which only allows for proving equations of the form
$F = \top$.
However it is known that every Boolean combination of equations is
equivalent to an equation of the form
$F = \top$ (see \cite{Mad}, pp.~435--6, pp.~439--440).

%
%What I obtained from your calculus is a following rewriting system \NRA
%in the original (positive) language of \RA. I write
%
%$ \land    \lor     \lnot     \bot    \top    \0    \1    \circ     +    \smile $
%
%for boolean times, plus, minus, 0, 1, relation-0, relation-1
%(identity), relation-product, relation-sum and conversity,
%respectively.
The system,
which we call \NRA\index{NRA@\textbf{NRA}|textbf},
uses ``literals'' ($L$) and ``positive terms'' ($A, B, C, D$).
Literals are of the shape 
$P$, $\lnot P$, $\smile P$, $\lnot \smile P$, $\0$ or $\1$,
for any given primitive relation symbol $P$
(as stated by Gordeev; presumably $\top$ and/or
$\bot$ should also be included).
Positive terms are
built up from literals using the binary operators.
Any \RA\ term is reducible to a positive term by the standard
rules which show how the unary operators distribute over the binary operators.
(These rules are not listed below.)
Corresponding \dRA\ structural rules for most of them are found in 
\fig{sdr}.

In \NRA\ there are 12 rewriting rules (NRA1)-(NRA12),
which are listed in Figure \ref{G}.
In these rules, $L$ denotes a literal; $A,B,C,D$ denote positive terms.
The rules are used in forming ``reductions'', as described below.

\newcommand\tabtwo[2]{ % similar to \frac, except no line, and
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ $ #2 $
  \end{tabular}}

\begin{figure}[htbp]
\label{G}
\begin{center}
\begin{tabular}{l@{\hspace{15mm}}c}
(NRA1) & \tabtwo {   A\lor B \longrightarrow B\lor A			}
  { A\land B \longrightarrow B\land A } \\[-1.0ex] & \\

(NRA2) & \tabtwo {   A\lor (B\lor C) \longrightarrow (A\lor B)\lor C	}
  { A\land (B\land C) \longrightarrow (A\land B)\land C } \\[-1.0ex] & \\

(NRA3) & $   A\lor (B\land C) \longrightarrow (A\lor B)\land (A\lor C) $ 
\\[-1.0ex] & \\

(NRA4) & $   A \longrightarrow A\lor A $ \\[-1.0ex] & \\

(NRA5) & $   A\lor B \longrightarrow A $ \\[-1.0ex] & \\

(NRA6) & $   \top\lor A \longrightarrow \top$ \qquad
   $ \top\land A \longrightarrow A $ \\[-1.0ex] & \\

(NRA7) & $   L\lor (\lnot L) \longrightarrow \top $ \\[-1.0ex] & \\

(NRA8) & \tabtwo {   A+(B+C) \longrightarrow (A+B)+C}
  { (A+B)+C \longrightarrow A+(B+C) } \\[-1.0ex] & \\

(NRA9) & $(A+B)\lor (C\circ D) \longrightarrow (A\lor C)\land (B\lor D)$
\\[-1.0ex] & \\

(NRA10) & \tabtwo { (A+B)\lor C \longrightarrow (\smile A+C)\lor B	}
  { (A+B)\lor C \longrightarrow (C+\smile B)\lor A } \\[-1.0ex] & \\

(NRA11) & $ A \longrightarrow \0+A$ \qquad
   $ A \longrightarrow A+\0 $ \\[-1.0ex] & \\

(NRA12) & $ \0+A \longrightarrow A$ \qquad
   $ A+\0 \longrightarrow A $
\\ & \\[0.0ex]
\multicolumn 2 c { \hspace{5em} $A,B,C,D$ denote positive terms} \\
\multicolumn 2 c { \hspace{5em} $L$ denotes a literal}
\\ & \\[1.0ex]
\multicolumn 2 c {\hspace{5em} $F[G'] \longrightarrow F[G'']$ } \\
\multicolumn 2 c { \hspace{5em}
where $G' \longrightarrow G''$ is any rule except (NRA9) and (NRA10)}
\\ & \\[1.0ex]
\multicolumn 2 c {
\hspace{5em} $G_1 \land G_2 \land \ldots \land G_j' \land \ldots \land G_k
\longrightarrow 
G_1 \land G_2 \land \ldots \land G_j'' \land \ldots \land G_k$} \\
\multicolumn 2 c {
\hspace{5em} where $G_j' \longrightarrow G_j''$ is (NRA9) or (NRA10) }
\end{tabular}
\end{center}

\caption{The rules of \NRA}
\end{figure}

A ``reduction" in \NRA\ is defined as one of
\begin{itemize}
\item
$F[G'] \longrightarrow F[G'']$,
% $F \longrightarrow F[G' \gets G'']$
where $G' \longrightarrow G''$ is 
an instance of any rule (NRA$i$) except for (NRA9) and (NRA10)
%or $F[G_j'] \longrightarrow F[G_j'']$
% or $F \longrightarrow F[G_j' := G_j'']$
% where $F[G_j'] = G_1 \land  G_2 \land  \ldots \land  G_k$,
%$1 \leq j\leq k$ and 
\item $G_1 \land G_2 \land \ldots \land G_j' \land \ldots \land G_k
\longrightarrow 
G_1 \land G_2 \land \ldots \land G_j'' \land \ldots \land G_k$
where $1 \leq j\leq k$ and 
$G_j' \longrightarrow G_j''$ is an instance of (NRA9) or (NRA10)
\end{itemize}
We take it that $F[\cdot]$ must be such that 
$G$ is a `sub-positive-term' of $F[G]$, ie, that $G$ is not a literal properly
contained in a larger literal within $F[G]$
(for example, $F[G]$ may not be $\lnot G \lor H$).

That is, the rules, except for (NRA9) and (NRA10), can be applied to 
rewrite any sub-positive-term of $F$.
However, (NRA9) and (NRA10) can be applied to rewrite only a conjunct of $F$.

A ``reduction chain" $F_0 \stackrel * \longrightarrow  F_n$
in \NRA\ is a finite sequence of reductions 
$F_0 \longrightarrow F_1 \longrightarrow \ldots \longrightarrow F_n$
(ie,  each $F_i \longrightarrow F_{i+1}$ is a ``reduction").
A derivation of $F$ in \NRA\ is a reduction chain 
$F \stackrel * \longrightarrow  \top$.

Gordeev states that
$F$ is derivable in \NRA\ iff $F=\top$ is derivable in \RA.
%(It is known that any Boolean combination of relational equations 
%is equivalent to an equation of the form $F=\top$,
%see \cite{Mad}, pp.~435-6.) 
He notes that
proofs in \NRA\ are shorter than in \dRA.

We now justify the soundness of this system in terms of \dRA.
Firstly, we explain the \NRA\ reduction step in terms of \dRA.

\begin{lemma} \label{gordlem}
Whenever $F' \longrightarrow F''$ in \NRA, 
then $\top \vdash F'' \Longrightarrow \top \vdash F'$ in \dRA.
\end{lemma}

\proof\ First we show that if $F' \longrightarrow F''$ in \NRA,
by virtue of rules other than (NRA9) and (NRA10), 
then $F'' \vdash F'$ in \dRA.

For rules (NRA1) to (NRA12), except (NRA9) and (NRA10), 
where \mbox{$F' \longrightarrow F''$} 
is the \NRA\ rule $G' \longrightarrow G''$,
the \dRA\ theorem $G'' \vdash G'$ is proved in Isabelle,
as \ttdef{G1a},\ttdef{G1b},\ldots,
\insrc{Gord.ML}.
Note that we have no way, in Isabelle, to encode the requirement that
$A,B,C,D$ denote positive terms rather than arbitrary formulae;
in fact the \dRA\ results hold for arbitrary formulae $A,B,C,D$,
and the Isabelle results
\texttt{G1a},\texttt{G1b},\ldots, are for arbitrary formulae.
Likewise, for (NRA7), we have no way to encode the requirement
that $L$ is a literal, but in fact (NRA7) holds for an arbitrary formula $L$.

Recall that, for rules other than (NRA9) and (NRA10),
$F[G'] \longrightarrow F[G'']$ is
a ``reduction" in \NRA\ where
% $F'' = F[G' := G'']$ and
$G' \longrightarrow G''$ is an instance of one of the rules.
So, assume $F' \longrightarrow F''$ is 
$F[G'] \longrightarrow F[G'']$, where 
$G' \longrightarrow G''$ is an instance of a rule other than (NRA9) and (NRA10).
Thus we have $G'' \vdash G'$, and we need to show $F[G''] \vdash F[G']$.
This is shown by induction on the structure of $F[\cdot]$;
recalling that $F[\cdot]$ uses only literals and the binary operators,
the inductive steps rely on the four \dRA-theorems
\texttt{cong\_or}, \texttt{cong\_and}, \texttt{cong\_comp} and \texttt{cong\_rs}
(see \S\ref{congs}), and the identity rule \texttt{idf}.

Since $F'' \vdash F'$, if we assume 
$\top \vdash F''$, then the (cut) rule gives $ \top \vdash F'$.

We now look at rules (NRA9) and (NRA10).
Where the \NRA\ rule is \mbox{$G' \longrightarrow G''$,}
we have proved the \dRA\ derived rule
$\top \vdash G'' \Longrightarrow \top \vdash G'$ in Isabelle,
as \ttdef{G9}, \ttdef{G10a} and \ttdef{G10b}, 
\insrc{Gord.ML}.

Now for rules (NRA9) and (NRA10),
$F[G'] \longrightarrow F[G'']$ is
a ``reduction" in \NRA\ where
% $F'' = F[G' := G'']$,
$G'$ is a conjunct of $F[G']$, 
and $G' \longrightarrow G''$ is an instance of one of the rules.
So we have 
$\top \vdash G'' \Longrightarrow \top \vdash G'$,
and we need to show 
$\top \vdash F[G''] \Longrightarrow \top \vdash F[G']$.
This is shown by induction on the number of conjuncts in $F[\cdot]$;
the inductive step uses the following \dRA-theorem,
proved in \texttt{Gord.ML}.
\begin{center}
\slrule {  \top \vdash G1'' \Longrightarrow \top \vdash G1' \qquad
      \top \vdash G2'' \Longrightarrow \top \vdash G2' }
       { \top \vdash G1'' \land G2'' \Longrightarrow \top \vdash G1' \land G2'}
(\ttdef{G910meth})
\end{center}
$\Box$

\label{G910meth}\texttt{G910meth} is
an Isabelle theorem whose use of the metalogic is
more complex than others seen so far.
It has nested occurrences of the
metalogical operator $\Longrightarrow$;
the premises and conclusion are all of the form
``$Y$ follows from $X$'', or
``$Y \Longrightarrow X$ can be derived as a rule''.

We can now demonstrate the soundness of \NRA\ with respect to \RA,
giving a constructive method of turning 
an \NRA-derivation of $F$ into a  
\dRA-derivation of $F = \top$.
 
\begin{thm} [Soundness of \NRA\ with respect to \dRA]
For every \NRA-derivation of $F$ there is a
\dRA-derivation of $\top \vdash F$.
\end{thm}

\proof\
Consider an \NRA-derivation of $F$, 
$F \stackrel * \longrightarrow  \top$, i.e.
$F=F_0 \longrightarrow F_1 \longrightarrow \ldots \longrightarrow F_n=\top$,
where each $F_i \longrightarrow F_{i+1}$ is a ``reduction".
Then Lemma~\ref{gordlem} gives us successively
$\top \vdash F_n$ (trivially), 
$\top \vdash F_{n-1}, \ldots,$ and $\top \vdash F_0$,
ie $\top \vdash F$.
$\Box$

Note that if we define `=' as in \S\ref{provRA},
then since, trivially, $F \vdash \top $,
we obtain $F = \top$ in the above theorem.

We have thus shown that 
if $F$ is derivable in \NRA\, then $\top \vdash F$
is derivable in \dRA, and so that $F=\top$ in \RA.
This demonstrates the soundness of \NRA\ with respect to \RA.

The converse of this, that \NRA\ is also complete with respect to \RA,
is shown by Gordeev \cite{Gor}.
He transforms derivability in \dRA\ into \NRA;
since \dRA\ is complete (ie, with respect to \RA), so is \NRA.

\renewcommand\cfile{}