\renewcommand\cfile{mad.tex}

From \M\ we construct an equivalent alternative system 
\Mp\index{M@\Mp|textbf}.
\Mp\ has fewer inference rules than \M\ (although more axioms);
this will make reasoning about rearranging proof trees easier
in \Mp\ than in \M.

First, we omit the axioms of \M\ (which are shown on the left),
and replace them by the new axioms shown.
\begin{center}
\begin{tabular}{c@{\hspace{15mm}}c}
{\bfseries Axiom of \M} & {\bfseries Axiom of \Mp} \\[1.0ex]
$ {\Gamma, x[R]y \vdash \Delta, x[R]y} $ & $ {x[R]y \vdash x[R]y} $ \\
$ {\Gamma, x[\bot] y \vdash \Delta} $ & $ {x[\bot] y \vdash } $ \\
$ {\Gamma \vdash \Delta, x[\top] y} $ & $ {\vdash x[\top] y} $ \\
$ {\Gamma \vdash \Delta, x[\1]x} $ & $ {\vdash x[\1]x} $ 
\end{tabular}
\end{center}

Secondly, we omit the following inference rules,
replacing them by the new axioms shown.

\begin{center}
\begin{tabular}{c@{\hspace{15mm}}c}
{\bfseries Rule of \M} & {\bfseries Axiom of \Mp} \\[1.0ex]
(Id) & $ x[R]z, z[\1]y \vdash x[R]y $ \\ 
($\lnot \vdash$) & $ x [\lnot R]y, x[R]y \vdash$ \\ 
($\vdash\lnot $) & $ \vdash x[R]y, x [\lnot R]y$ \\ 
($\smile \vdash$) & $ y [\smile R]x \vdash x[R]y$ \\ 
($\vdash\smile $) & $ x[R]y \vdash y [\smile R]x$ \\ 
($\lor \vdash $) & $ x[R \lor S]y \vdash x[R]y, x[S]y$ \\ 
($\vdash \lor $) &
$ x[R]y \vdash x[R \lor S]y$ \quad and \quad $ x[S]y \vdash x[R \lor S]y$ \\
($\land \vdash $) &
$ x[R \land S]y\vdash x[R]y $ \quad and \quad $ x[R \land S]y\vdash x[S]y $ \\ 
($\vdash \land $) & $ x[R]y, x[S]y\vdash x[R \land S]y $ \\ 
($\vdash \circ $) & $ x[R]y, y[S]z\vdash x[R \circ S]z $ 
\end{tabular}
\end{center}

This gives the system \Mp, as shown in \fig{Mp}.

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

\vspace{2mm} 
\hfill
$\displaystyle {x[R]y \vdash x[R]y} $ \hfill
$\displaystyle {x[\bot] y \vdash } $ \hfill
$\displaystyle {\vdash x[\top] y} $ \hfill
$\displaystyle {\vdash x[\1]x} $ \hfill \mbox{}

\begin{tabular}{c@{\hspace{0mm}}c}
 & \\
 & { $ x[R]z, z[\1]y \vdash x[R]y $ } \\ 
 & \\
$ x [\lnot R]y, x[R]y \vdash$ & 
$ \vdash x[R]y, x [\lnot R]y$ \\ 
 & \\
$ y [\smile R]x \vdash x[R]y$ & 
$ x[R]y \vdash y [\smile R]x$  \\
 & \\
$ x[R \lor S]y \vdash x[R]y, x[S]y$ & 
$ \begin{array}{c}  x[R]y \vdash x[R \lor S]y \\
 x[S]y \vdash x[R \lor S]y  \end{array}$  \\
 & \\
$ \begin{array}{c} x[R \land S]y\vdash x[R]y \\
 x[R \land S]y\vdash x[S]y \end{array} $ & 
$ x[R]y, x[S]y\vdash x[R \land S]y $  \\ 
& \\
 & { $ x[R]y, y[S]z\vdash x[R \circ S]z $ } 
 \\ &
\end{tabular}

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
%$\\ & \\ $\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, \delta \qquad \Gamma', \delta \vdash \Delta'}
{\Gamma, \Gamma' \vdash \Delta, \Delta'} 
$(cut) \\ ($y$ cannot appear in $\Gamma$ or $\Delta$) &

\end{tabular}
\end{center}
\caption{The system \Mp}
\end{figure}

\begin{thm} \label{mmp}
The systems \M\ and \Mp\ are equivalent
(ie, any sequent provable in \M\ is provable in \Mp, and vice versa).
Further, if we define 
{$\mathcal M_n$} and {$\mathcal M'_n$}
to be the systems \M\ and \Mp\, limited to
$n$-sequents and $n$-proofs, then, for $n \geq 3$, 
{$\mathcal M_n$} and {$\mathcal M'_n$} are equivalent.
\end{thm}

{\bfseries Proof.} 
The first four axioms of \Mp\ are special cases of the axioms of \M;
conversely, the four axioms of 
\M\ can be deduced (in \Mp)
from these four axioms of \Mp\ using the monotonicity rules,
$(M \vdash )$ and $(\vdash M )$, which are part of \Mp.

The remaining new axioms of \Mp\ can easily be deduced 
in \M\ using the corresponding rules of inference shown.
Conversely,
in each case, the inference rule of \M\ may
be derived in \Mp\ by using the corresponding axiom(s) of \Mp\ shown,
with one or two applications of the (cut) inference rule.
Some examples of this follow.

%For example, to derive the ($\vdash \circ $) rule in \Mp,
\vpf
\begin{center}
\bpf
\A "$ \Gamma \vdash \Delta, y[S]z$"
\A "$ \Gamma \vdash \Delta, x[R]y $"
\A "axiom of \Mp"
\U [:] "$ x[R]y, y[S]z\vdash x[R \circ S]z $"
\B "$ {\Gamma, y[S]z \vdash \Delta, x[R \circ S]z} $" "(cut)"
\B "$ {\Gamma \vdash \Delta, x[R \circ S]z} $" "(cut)"
\epf
\\[1.0ex]
{\small Derivation  in \Mp\ of the ($\vdash \circ $) rule of \M}
\end{center}

\up 4
\begin{center}
\bpf
\A "axiom of \Mp"
\U [:] "$ x[R \land S]y\vdash x[S]y $"
\A "axiom of \Mp"
\U [:] "$ x[R \land S]y\vdash x[R]y $"
\A "$ \Gamma, x[R]y, x[S]y \vdash \Delta $"
\B "$ \Gamma, x[R \land S]y, x[S]y \vdash \Delta $" "(cut)"
\B "$ \Gamma, x[R \land S]y \vdash \Delta$" "(cut)"
\epf
\\[1.0ex]
{\small Derivation  in \Mp\ of the ($\land \vdash $) rule of \M}
\end{center}

\up 4
\begin{center}
\bpf
\A "axiom of \Mp"
\U [:] "$ \vdash x[R]y, y [\lnot R]x$"
\A "$ \Gamma, x[R]y \vdash \Delta $"
\B "$ \Gamma \vdash \Delta, x[\lnot R]y$" "(cut)"
\epf
\\[1.0ex]
{\small Derivation  in \Mp\ of the ($\vdash \lnot $) rule of \M}
\end{center}

Note that, in all these derivations, if the premises and conclusion use
at most $n$ point variables, then so do the intermediate sequents.
$\Box$

We now look at re-ordering the steps in a derivation in \Mp. 
This will help us to produce a correpsonding derivation in \dRA.
Consider first the monotonicity rules, 
$(M \vdash )$ and $(\vdash M )$.
These rules simply add an extra formula to a sequent.
We try to move any use of a monotonicity rule to as near as possible 
to the bottom of a proof.

\begin{thm} \label{pw} Any $n$-proof in \Mp\ can be replaced by an
$n$-proof in which any monotonicity step 
(use of the rules $(M \vdash )$ or $(\vdash M )$)
\begin{itemize} \shrinklist{0.5}
\item[--]
is immediately above a step using the $(\circ \vdash) $ rule,
\item[--]
is immediately above another monotonicity step, or
\item[--]
is at the bottom of the proof.
\end{itemize}
\end{thm}

{\bfseries Proof.} 
Following the terminology of Belnap \cite{Bel}, we define
a \bfi{parameter} of an inference rule of \Mp\ as 
one of the formulae in the sets 
$\Gamma$, $\Delta$, $\Gamma'$ or $\Delta'$ of the rule as shown.
The other formula in the conclusion of a rule is called
the {\bfseries principal}\index{principal formula|textbf} formula, and 
the other formula(e) in the premises of a rule are called
the {\bfseries side\index{side formula|textbf}} formula(e).

Consider the proof step immediately below a monotonicity step.
To simplify the discussion, assume that the monotonicity step adds only a single
formula.

If the formula added by the monotonicity step is 
a parameter of the next lower proof step, then 
clearly that lower proof step could be done without the extra formula,
and the extra formula could be added, by monotonicity, to the conclusion of
the lower proof step.
(Note the difference between \M\ and \Mp\ here.
This reasoning does not apply to \M, in which some inference rules
contain two premises, each containing an occurrence of $\Gamma$, where
the two occurrences of
$\Gamma$ need to be the same, for those rules, in the form given, to apply).

Suppose, on the other hand,
that the formula added by the monotonicity step is not a parameter
(ie, is a side formula) of the next lower proof step.
Then, where the lower proof step is an instance of the rule (cut),
the sequent which is the \emph{premise} of the monotonicity step must be
${\Gamma \vdash \Delta} $ or
$\Gamma' \vdash \Delta' $ as in the statement of the (cut) rule.
(This is because each premise of (cut) contains only one side formula).
Then the use of (cut) is unnecessary;
the conclusion of the lower step could be 
obtained directly from the premise of the upper step,
by monotonicity.
An example of this is shown below: the proof fragment on the left can be
replaced by that on the right.

\vpf
\begin{center}
\hfill
\bpf
\A "$ \Gamma \vdash \Delta $"
\U "$ \Gamma \vdash \Delta, \delta $" "($\vdash M$)"
\A "$ \Gamma', \delta \vdash \Delta' $"
\B "$ \Gamma, \Gamma' \vdash \Delta, \Delta'$" "(cut)"
\epf
\hfill
\bpf
\A "$ \Gamma \vdash \Delta $"
\U "$ \Gamma \vdash \Delta, \Delta' $" "($\vdash M$)"
\U "$ \Gamma, \Gamma' \vdash \Delta, \Delta'$" "($M \vdash $)"
\epf
\hfill \mbox{}
\\[1.0ex]
{\small Removal of (cut) following monotonicity step }
\end{center}

%Note that, in all these derivations, if the premises and conclusion use
%at most $n$ point variables, then so do the intermediate sequents.

There remains the case of the $(\circ \vdash) $ rule;
a monotonicity step immediately above this rule may not be able to be
moved lower.

If we continue re-ordering the proof, by moving monotonicity steps lower
in this way, we reach the situation where each monotonicity step 
\begin{itemize}
\item[--]
is immediately above a step using the $(\circ \vdash) $ rule,
\item[--]
is immediately above another monotonicity step, or
\item[--]
is at the bottom of the proof.
\end{itemize}

Finally, it can be seen that these modifications to the proof change 
an $n$-proof into another $n$-proof.
$\Box$

\renewcommand\cfile{}