\documentstyle[proof]{article}
\def\imp{\to}
\def\ra{\Rightarrow}
%\def\land{\mathbin\&}
\newtheorem{definition}{DEFINITION}[section]
\newtheorem{lemma}[definition]{LEMMA}
\newtheorem{theorem}[definition]{THEOREM}
\newtheorem{corollary}[definition]{COROLLARY}
\newtheorem{proposition}[definition]{PROPOSITION}
\newtheorem{example}[definition]{EXAMPLE}
\newtheorem{remark}[definition]{REMARK}
\newtheorem{conjecture}[definition]{CONJECTURE}
%\setlength{\textwidth}{230pt}
\renewcommand{\baselinestretch}{2}
\title{Syntactical Investigations into $BI$ Logic and $BB'I$ Logic}
\author{ Yuichi Komori \\
%	Department of Mathematics,
%	Faculty of Science \\
%	Shizuoka University \\
%	Ohya Shizuoka 422 JAPAN \\
%	e-mail ykomori@tansei.cc.u-tokyo.ac.jp
}
\date{10 November, 1993}
\begin{document}
\maketitle
%
In this note, we will study four implicational logics $B, BI, BB' and BB'I$.
In \cite{Mar}, Martin and Meyer proved that a formula $\alpha$ is provable
in $BB'$ if and only if $\alpha$ is provable in $BB'I$ and $\alpha$ is not of
the form of
$\beta \to \beta$.  Though it gave a positive solution to the $P-W$ problem,
their method was semantical and not easy to grasp.  We shall give a
syntactical proof of the syntactical relation between $BB'$ and $BB'I$ logics.
It also includes a syntactical proof of Powers and Dwyer's theorem
that is proved
semantically in \cite{Mar}.  Moreover, we shall establish the same
relation between $B$ and $BI$ logics as $BB'$ and $BB'I$ logics.  This relation
seems to say that $B$ logic is meaningful, and so we think that $B$ logic
is the weakest among meaningful logics.  Therefore, by Theorem~\ref{mainB},
our Gentzen-type system
for $BI$ logic may be regarded as the most basic among all meaningful logics. 
It should be mentioned here that the first syntactical proof of $P-W$
problem is given by Misao Nagayama \cite{Nagayama}.
%
\section{Introduction}
\setcounter{definition}{0}
%
We will be concerned with four logics of pure implication, formulated in
a language constructed in the usual way from a set of propositional
variables, with a single binary connective $\to$.
We use $p, q,...,
p_1, q_1,...$, as variables ranging over propositional variables.
We use $\alpha, \beta,...,
\alpha_1, \beta_1,...$, as variables ranging over formulas.
By the symbol $\equiv$, we mean the equality as sequences of symbols.
Parentheses will be omitted following the convention that $\to$ associates
to the right. For example,
$\alpha_1 \to \alpha_2 \to \alpha_3 \to \alpha_4$ denotes 
$\alpha_1 \to (\alpha_2 \to (\alpha_3 \to \alpha_4))$.

The first logic, which we call $B$, has axioms all instances of
\[(B) \ (\beta \to \gamma) \to (\alpha \to \beta) \to \alpha \to \gamma, \]
and a rule
$$ 
\infer[\mbox{(modus ponens)}]{\beta}{\alpha \to \beta & \alpha}.
$$

The second logic, $BI$, has in addition to the axioms and rules of $B$
the axiom scheme
\[(I) \ \alpha \to \alpha. \]
The third logic, $BB'$, has in addition to the axioms and rules of $B$
the axiom scheme
\[(B') \ (\alpha \to \beta) \to (\beta \to \gamma) \to \alpha \to \gamma. \]
The fourth logic, $BB'I$, has in addition to the axioms and rules of $BB'$
the axiom scheme $I$.

Let $L$ be any one of logics $B, BI, BB'$ or $BB'I$.
We write $L \vdash \alpha \ \ 
( L \not\vdash \alpha )$ to mean that $\alpha$ is (resp. is not) provable in
the logic $L$.  Such systems as $B$, $BI$, $BB'$ and $BB'I$ are called
Hilbert-type systems , contrasting with Gentzen-type systems.
We say that a formula $\alpha$ is trivial (non-trivial) 
if $\alpha$ is (resp. is not) of the form $\beta \to \beta$.
We have the following three main theorems.

\begin{theorem} \label{mainB}
For any formula $\alpha$, $B \vdash \alpha$ \ \ if and only if \ \ 
$BI \vdash \alpha \ and \ \alpha$ is non-trivial.
\end{theorem}
\begin{theorem} \label{mainBB'}
For any formula $\alpha$, $BB' \vdash \alpha$ \ \ if and only if \ \ 
$BB'I \vdash \alpha$ \ and \ $\alpha$ is non-trivial.
\end{theorem}
\begin{theorem} \label{decidable}
The four logics $B$, $BI$, $BB'$ and $BB'I$ are decidable.
\end{theorem}

Anderson and Belnap asked in {\bf \S8.11} of \cite{Anderson}
whether $\alpha$ and $\beta$ are the same formula if both formulas
$\alpha \to \beta$ and $\beta \to \alpha$ are provable in $BB'I$.
This question is known as the $P-W$ problem to which
Martin and Meyer \cite{Mar}
has provided a positive solution by a semantical method.

Let us explain why Theorem~\ref{mainBB'} is sufficient for the $P-W$ problem:
To argue by contradiction, we assume that the $P-W$ problem did not hold.
The assumption implies that there would exist distinct formulas
$\alpha, \beta$ such that $BB'I \vdash \alpha \to \beta$ and $BB'I
\vdash \beta \to \alpha$.
Since $\alpha$ is distinct from $\beta$, by Theorem~\ref{mainBB'} 
both $\alpha \to \beta$ and $\beta \to \alpha$ are in fact provable in $BB'$.
However then $\beta \to \beta$ would be provable in $BB'$ by the rule of
modus ponens and an axiom scheme $B$,
which contradicts Theorem~\ref{mainBB'}.
%
\section{The system $LBI$ for the logic $BI$}
\setcounter{definition}{0}
%
Now we shall introduce Gentzen-type systems $LB$ and $LBI$,
where the cut elimination
theorem holds for $LBI$.
Using the cut elimination theorem, we will prove that
for any formula $\alpha$, $B \vdash \alpha$ \ \ if \ \ 
$BI \vdash \alpha$ \ and \ $\alpha$ is non-trivial.
This is a $B$--$BI$ analogue of Powers and Dwyer's theorem which states
the similar relation between $BB'$ and $BB'I$.

In the following, we will use Greek capital letters $\Gamma, \Delta,
\Sigma...$ for finite (possibly empty) sequences of formulas separated
by commas.  We denote the number of formulas in $\Gamma$ by $|\Gamma|$.
An expression of the form $\Gamma \ra \alpha$ is called a sequent, where
$\Gamma$ is a finite sequence of formulas and $\alpha$ is a formula.
Let $\Gamma \equiv \alpha_1, \cdots, \alpha_n$
( sometimes denoted by $( \alpha_1, \cdots, \alpha_n )$ ) and $\beta$
be a formula. We denote a formula $\alpha_1 \to \cdots \to \alpha_n
\to \beta$ by $\Gamma \to \beta$.
We assume here a familiarity with the basic knowledge of Gentzen-type
systems (see e.g. \cite{Gentzen}).

Initial sequents of $LBI$ are of the form 
\[ p \ra p \ \ \ \ \ \mbox{for any propositional variable $p$.} \]
Rules of inferences of $LBI$ are as follows:
$$
\infer[\mbox{(cut)}]{\Gamma,\Delta \ra \gamma}
			{\Gamma \ra \alpha & \alpha,\Delta \ra \gamma},
$$

$$\infer[(\to \mbox{right})]{\Gamma \ra \alpha \to \beta}
                          {\Gamma,\alpha \ra \beta},
\qquad
\infer[(\to \mbox{left})]{\Gamma,\alpha \to \beta,\alpha,\Delta \ra \gamma}
                    {\Gamma,\beta,\Delta \ra \gamma}.
$$

Initial sequents of $LB$ are of the form
for any formulas $\alpha$, $\beta$ and $\gamma$ and for any sequence $\Gamma$,
\[ \beta \to \Gamma \to \gamma, \alpha \to \beta, \alpha, \Gamma \ra \gamma. \]
The rules of $LB$ are the same as those of $LBI$.

Next we will introduce an auxiliary Gentzen-type system $L^*B$ to prove
that $B$ and $LB$ are logically equivalent.

Initial sequents of $L^*B$ are the same as those of $LB$.

Rules of inferences of
$L^*B$ are the following:
$$
\infer[\mbox{(cut*)}]{\Delta \ra \gamma}
			{\ra \alpha & \alpha,\Delta \ra \gamma},
$$

$$
\infer[(\to \mbox{right})]{\Gamma \ra \alpha \to \beta}
                          {\Gamma,\alpha \ra \beta},
\qquad
\infer[(\to \mbox{left*})]{\alpha \to \beta,\alpha,\Delta \ra \gamma}
                    {\beta,\Delta \ra \gamma}.
$$

We write $L \vdash \Gamma \ra \alpha \ \ 
( L \not\vdash \Gamma \ra \alpha )$ to mean that the sequent
$\Gamma \ra \alpha$ is
(resp. is not) provable in the Gentzen-type system $L$.
\begin{lemma} \label{B}
For any sequence $\Gamma$ of formulas and any formula $\alpha$,
$B \vdash \Gamma \to \alpha$ \ \ if and only if \ \ 
$L^*B \vdash \Gamma \ra \alpha$.
\end{lemma}
\begin{lemma} \label{LB}
For any sequence $\Gamma$ of formulas and any formula $\alpha$,
$LB \vdash \Gamma \ra \alpha$ \ \ 
if and only if \ \ 
$L^*B \vdash \Gamma \ra \alpha$.
\end{lemma}

PROOF.\ \ As rules of inferences of $L^*B$ are
those of $LB$ and initial sequents of $L^*B$ are the same as those of $LB$,
we have that $LB \vdash \Gamma \ra \alpha$ if $L^*B \vdash \Gamma \ra
\alpha$.  So, it suffices to show that both rules (cut) and ($\to$ left)
are derived rules of $L^*B$.
The following proof figure shows that (cut) is derived:
$$
\infer[\mbox{(cut*)}]{\Gamma, \Delta \ra \gamma}
	{\infer[(\to \mbox{right})]{\ra \Gamma \to \alpha}
		{\infer{\rule{15mm}{0mm}}{\Gamma \ra \alpha}} &
		\infer[(\to \mbox{left*})]{\Gamma \to \alpha, \Gamma, \Delta
			\ra \gamma}
		{\infer{\rule{3cm}{0mm}}{\alpha, \Delta \ra \gamma}}
	}.
$$
The following proof figure shows that ($\to$ left) is derived:
$$
\infer[\mbox{(cut)}]{\Gamma, \alpha \to \beta,\alpha,\Delta \ra \gamma}
	{\infer[(\to \mbox{right})]{\Gamma \ra \beta \to \Delta \to \gamma}
		{\infer{\rule{30mm}{0mm}}{\Gamma,\beta,\Delta \ra \gamma}} &
		\deduce{\beta \to \Delta \to \gamma,\alpha \to \beta,\alpha,
		\Delta \ra \gamma}{\mbox{initial sequent}}
	}. \ \ \ \ \Box
$$

From Lemma~\ref{B} and Lemma~\ref{LB}, the next theorem, which tells that
the system $LB$ is logically equivalent to $B$ logic, follows immediately.
\begin{theorem} \label{B-LB}
For any sequence $\Gamma$ of formulas and any formula $\alpha$,
$B \vdash \Gamma \to \alpha$ \ \ if and only if \ \ 
$LB \vdash \Gamma \ra \alpha$.
\end{theorem}

In the same way as the above, we can prove the following.

\begin{theorem} \label{BI-LBI}
For  and any sequence $\Gamma$ of formulas and any formula $\alpha$,
$BI \vdash \Gamma \to \alpha$ \ \ if and only if \ \ 
$LBI \vdash \Gamma \ra \alpha$.
\end{theorem}

Next we will prove the cut elimination theorem for $LBI$.
Our theorem can be proved in the standard way
( see \cite{Gentzen} ).  But the fact that $LBI$ does not have the
contraction rule will simplify the proof at two points.  The first point is
that we need not replace each cut rule by a mix rule. The second point is
that we can prove it by single induction on the length, not double induction
on the degree and the rank.
The {\it length} of the proof $P$, denoted by $L(P)$, is the
number of sequents appearing in $P$.  We denote the endsequent of a proof
$P$ by $end(P)$.
Our theorem makes mention also of the length of the cut-free proof.
%
\begin{theorem}[Cut elimination theorem for $LBI$] \label{cutBI}
If $P$ is a proof of $LBI$, then there exists a cut-free
proof $Q$ of $LBI$ such that $L(Q) \leq L(P)$ and $end(Q) \equiv end(P)$.
\end{theorem}

PROOF. \ \ It suffices to show that 

(*) {\it If $P$ is a proof of $LBI$, which contains only one
cut rule, occurring as the last inference, then there exits a cut-free
proof $Q$ such that $L(Q) < L(P)$ and $end(Q) \equiv
end(P)$}.

So, let us suppose that $P$ is a proof which contains a cut only as the
last inference:
$$
\infer[\mbox{(cut)}]{\Gamma,\Delta \ra \gamma}
			{\Gamma \ra \alpha & \alpha,\Delta \ra \gamma}.
$$
We prove (*) by induction on the length of $P$.  We divide the proof
into the following three cases:

Case 1. Either $\Gamma \ra \alpha$ or $\alpha, \Delta \ra \gamma$ is an
initial sequent.

Case 2. Either $\Gamma \ra \alpha$ or $\alpha, \Delta \ra \gamma$ is
a lower sequent of a rule, whose principal formula is not
(the occurence of) $\alpha$, to which the cut rule is applied.

Case 3. Both $\Gamma \ra \alpha$ and $\alpha, \Delta \ra \gamma$
are lower sequents of some rules such that principal formulas
of both rules are (occurrences of) $\alpha$ to which the cut rule is
applied.

In the following, we will show (*) only for Case 3 where $\alpha$
is of the form $\beta \to \delta$.  In this case, the last part
of $P$ is of the form
$$
\infer[\mbox{(cut)}]{\Gamma,\beta,\Delta \ra \gamma}
	{\infer{\Gamma \ra \beta \to \delta}{\Gamma,\beta \ra \delta} &
	 \infer{\beta \to \delta,\beta,\Delta \ra \gamma}
	 	{\delta,\Delta \ra \gamma}}.
$$
Consider the proof $P'$ of which the last part is of the form
$$
\infer[\mbox{(cut)}]{\Gamma,\beta,\Delta \ra \gamma}
	{\Gamma,\beta \ra \delta &
	 \delta,\Delta \ra \gamma}.
$$
Because $L(P') < L(P)$, we can eliminate this cut rule by the induction
hypothesis. \ \ $\Box$

In our joint paper \cite{OnoKomo} with Ono, we proved the cut elimination
theorem for logics without the contraction rule by double induction
on the grade and the length.  However we could prove it by induction
on the length like the above.

R. Hindley asked the author whether the implicational part of $LBCA$ logic
is logically equivalent to $BI$ logic,
where $LBCA$ (badly named in \cite{Komori86}) is obtained from the
intutionistic logic $LJ$ by deleting all structure rules.
We can answer the question in the negative here.
Whereas $(p \to p) \to q \ra q$ is provable
in $LBCA$, by the cut elimination theorem in the above
we have that it is not provable in
$LBI$. So, the implicational part of $LBCA$ logic
is not logically equivalent to $BI$ logic. All rules of $LBI$ are derivable
in $LBCA$, and so the logic $BI$ is weaker than $LBCA$.

Similarly to the proof of Theorem 6.6 of \cite{Takeuti}, we can derive
the following theorem from Theorem~\ref{cutBI}.
\begin{theorem} \label{interBI}
Craig's interpolation theorem holds for $LBI$.  More precisely,
if $LBI \vdash \Gamma, \Delta \ra \gamma$ and $\Gamma \neq \emptyset$
then there exists a formula $\alpha$ such that
\begin{enumerate}
\item $LBI \vdash \Gamma \ra \alpha$ and $LBI \vdash \alpha, \Delta \ra
\gamma$,
and
\item all propositional variables in $\alpha$ occur both in $\Gamma$
and $\Delta \cup \{\gamma\}$.
\end{enumerate}
\end{theorem}

By the cut elimination theorem and lack of the contraction rule,
only finite number of sequents can occur in a cut-free proof of
$\Gamma \ra \gamma$ for any sequent $\Gamma \ra \gamma$.  So, by
Theorem~\ref{BI-LBI}, we have
%
\begin{theorem}	\label{BI-decidable}
The logic $BI$ is decidable.
\end{theorem}

We are at the point of showing
the same relation between $B$ and $BI$
logics as what Powers and Dwyer showed between $BB'$ and $BB'I$ logics.
%

A sequent $\Gamma \ra \gamma$ is called trivial (non-trivial) if the formula
$\Gamma \to \gamma$ is trivial (resp. non-trivial).
\begin{theorem} \label{B-Powers}
For any sequent $\Gamma \ra \gamma$, $LB \vdash \Gamma \ra \gamma$ \ \ if \ \ 
$LBI \vdash \Gamma \ra \gamma$ \ and \ $\Gamma \ra \gamma$ is non-trivial.
\end{theorem}

PROOF. \ \ We prove this by induction on the length of the cut-free
$LBI$ proof of the sequent $\Gamma \ra \gamma$.  We divide the proof
into the following two cases:

Case 1. $\Gamma \ra \gamma$ is a lower sequent of ($\to$ right).

Case 2. $\Gamma \ra \gamma$ is a lower sequent of ($\to$ left).

For Case 1, it is trivial.  In Case 2, the last part of the proof is of
the form
$$
\infer[(\to \mbox{left})]{\Gamma,\alpha \to \beta,\alpha,\Delta \ra \gamma}
	{\Gamma,\beta,\Delta \ra \gamma}.
$$

If $\Gamma,\beta,\Delta \ra \gamma$ is non-trivial, then we have
$LB \vdash \Gamma,\beta,\Delta \ra \gamma$ by the induction
hypothesis.
So, we have
$LB \vdash \Gamma,(\alpha \to \beta),\alpha,\Delta \ra \gamma$.

If $\Gamma,\beta,\Delta \ra \gamma$ is trivial then $\Gamma$ is not
empty, since otherwise $\Gamma,\alpha \to \beta,\alpha,\Delta \ra \gamma$
becomes also trivial.
Let $\Gamma \equiv \delta,\Sigma$, then $\delta \equiv \Sigma \to \beta
\to \Delta \to \gamma$.  So, the lower sequent equals
$\Sigma \to \beta \to \Delta \to \gamma,\Sigma,\alpha \to \beta,\alpha,
\Delta \ra \gamma$.    
The following proof figure shows that the lower sequent is provable in $LB$:
$$
\infer[(\to \mbox{left})]{\Sigma \to \beta \to \Delta \to \gamma,
\Sigma,\alpha \to \beta,\alpha,\Delta \ra \gamma}	{
\infer{}{\deduce{\beta \to \Delta \to \gamma,\alpha \to \beta,\alpha,
		\Delta \ra \gamma}{\mbox{initial sequent}}
	}
							}.\ \ \Box
$$

To show the converse of Theorem~\ref{B-Powers}, it is sufficient to
prove that any trivial sequent is not provable in $LB$.
In fact, this will be proved in Theorem~\ref{main} in a stronger form.
%
\section{The system $LBB'I$ for the logic $BB'I$}
\setcounter{definition}{0}
%
Now we shall introduce Gentzen-type systems $LBB'$ and $LBB'I$, for both
of which the cut elimination theorem holds.
Using the cut elimination theorem, we will prove
syntactically Powers and Dwyer's theorem.

To explain the system $LBB'I$, we need an operation called a
{\em guarded merge} on
sequences of formulas, originally introduced in \cite{Mar}. Here by a merge of
sequences $\Gamma$ and $\Delta$, we mean a new sequence exactly consisting of
members of $\Gamma$ and $\Delta$ as multisets, in which both $\Gamma$ and
$\Delta$ preserve their original orders.
\begin{definition}
{\rm A {\em guarded merge} of $\Gamma$ and $\Delta$, denoted by 
$\Gamma \circ \Delta$, is a sequence obtained from a merge of sequences 
$\Gamma$ and $\Delta$ such that its rightmost formula is that of $\Delta$ if
$\Delta \neq \emptyset$.  $\Gamma \circ \Delta \equiv \Gamma$ if
$\Delta = \emptyset$.}
\end{definition}
Parentheses will be omitted following the convention that $\circ$ associates
to the right.

Initial sequents of $LBB'I$ are of the form 
\[ p \ra p \ \ \ \ \ \mbox{for any propositional variable $p$.} \]

Rules of inferences of $LBB'I$ are the following three.
$$
\infer[\mbox(cut)]{\Delta \circ \Gamma,\Sigma \ra \gamma}
{\Gamma \ra \alpha & \Delta,\alpha,\Sigma \ra \gamma},
$$
where $\Gamma \neq \emptyset$ or $\Delta = \emptyset$.
$$
\infer[(\to \mbox{right})]{\Gamma \ra \alpha \to \beta}
                          {\Gamma,\alpha \ra \beta}.
$$
$$
\infer[(\to \mbox{left})]{\Delta \circ ( \alpha \to \beta ) \circ \Gamma,
\Sigma \ra \gamma}{\Gamma \ra \alpha &
\Delta,\beta,\Sigma \ra \gamma},
$$
where $\Gamma \neq \emptyset$.

Initial sequents of $LBB'$ are of the form,
for any propositional variable $p$, any formulas $\alpha$ and $\beta$ and
any sequence $\Gamma$,
\[ ( \beta \to \Gamma \to p ) \circ ( \alpha \to \beta, \alpha ),
		 \Gamma \ra p. \]
The system $LBB'$ has five rules of inferences.  Three of them are
the same as those of $LBB'I$.  Additional two rules are as follows.
$$
\infer[(\to \mbox{left 1})]{\Gamma \circ ( \alpha \to \beta,\alpha ),
\Delta \ra \gamma}{\Gamma,\beta,\Delta \ra \gamma},
$$
where we call (the occurrence of) the formula $\alpha$
a {\it semi-principal} formula of ($\to$ left 1).
$$
\infer[(\to \mbox{left 2})]{( \alpha \to \Delta \to p ) \circ \Gamma,
\Delta \ra p}{\Gamma \ra \alpha},
$$
where $\Gamma \neq \emptyset$ and $p$ is a propositional variable, and
we say that (occurrences of) formulas in $\Delta$ and the
propositional variable $p$ are
{\it semi-principal} formulas of ($\to$ left 2).

Next we will introduce an auxiliary Gentzen-type system $L^*BB'$ to prove
that $BB'$ and $LBB'$ are logically equivalent.
Initial sequents of $L^*BB'$ are the same as those of $LBB'$.

Rules of inferences of
$L^*BB'$ are the following:
$$
\infer[\mbox{(cut*)}]{\Gamma,\Delta \ra \gamma}
			{\Gamma \ra \alpha & \alpha,\Delta \ra \gamma},
$$
$$
\infer[(\to \mbox{right})]{\Gamma \ra \alpha \to \beta}
                          {\Gamma,\alpha \ra \beta},
\qquad
\infer[(\to \mbox{left*})]{\Gamma,\alpha \to \beta,\alpha,\Delta \ra \gamma}
                    {\Gamma,\beta,\Delta \ra \gamma}.
$$

Clearly, $L^*BB' \vdash \Gamma \ra \gamma$ if $BB' \vdash \Gamma \to \gamma$.
Conversely, $BB' \vdash \Gamma \to \gamma$ if $L^*BB' \vdash \Gamma \ra \gamma$
because all rules of $L^*BB'$ are those of $LB$.
So we have
%
\begin{lemma} \label{BB'}
For any sequence $\Gamma$ of formulas and any formula $\alpha$,
$BB' \vdash \Gamma \to \alpha$ \ \ if and only if \ \ 
$L^*BB' \vdash \Gamma \ra \alpha$.
\end{lemma}
%

We need the following three lemmas to prove Lemma~\ref{LBB'} corresponding to
Lemma~\ref{LB}.
\begin{lemma}
The following rule (cut**) is derived in $L^*BB'$:
$$
\infer[\mbox(cut**)]{\Delta,\beta,\Sigma \ra \gamma}
{\beta \ra \alpha & \Delta,\alpha,\Sigma \ra \gamma}.
$$
\end{lemma}

PROOF. \ \ The following proof figure shows that (cut**) is derived:
$$
\infer[\mbox{(c*)}]{\Delta, \beta, \Sigma \ra \gamma}
	{\infer[(\to \mbox{r})]{\Delta \ra \alpha \to \Sigma \to \gamma}
		{\infer{\rule{25mm}{0mm}}{\Delta,\alpha,\Sigma \ra \gamma}}
	&
	\infer[\mbox{(c*)}]{\alpha \to \Sigma \to \gamma,\beta,\Sigma
					 \ra \gamma}
		{\infer[(\to \mbox{r})]{\ra \beta \to \alpha}{\beta \ra \alpha} 
			&
		\infer[(\to \mbox{r})]{\beta \to \alpha,\alpha \to
		 \Sigma \to \gamma,\beta,\Sigma \ra \gamma}
		 {\infer{}{\mbox{initial sequent}}}
		}
	}.
$$
\ \ $\Box$
%
\begin{lemma}
The following rule ($\to$ left**) is derived in $L^*BB'$:
$$
\infer[(\to \mbox{left**})]{\alpha \to \beta,\delta,\alpha,\Delta \ra \gamma}
                    {\delta,\beta,\Delta \ra \gamma}.
$$
\end{lemma}

PROOF. \ \ The following proof figure shows that ($\to$ left**) is derived:
$$
\infer[\mbox{(cut**)}]{\alpha \to \beta,\delta,\alpha,\Delta \ra \gamma}
	{\infer[(\to \mbox{right})]{\delta \ra \beta \to \Delta \to \gamma}
		{\infer{\rule{30mm}{0mm}}{\delta,\beta,\Delta \ra \gamma}} &
		\infer[(\to \mbox{right})]{\alpha \to \beta,\beta
		 \to \Delta \to \gamma,\alpha,\Delta \ra \gamma}
		 {\infer{}{\mbox{initial sequent}}}
	}. \ \ \Box
$$
%
\begin{lemma}
The following rule ($\to$ left***) is derived in $L^*BB'$:
$$
\infer[(\to \mbox{left***})]{\Gamma,\alpha \to \beta,\Delta,\alpha,\Sigma
				 \ra \gamma}
		{\Gamma,\Delta,\beta,\Sigma \ra \gamma}.
$$
\end{lemma}

PROOF. \ \ 
When $\Delta = \emptyset$, ($\to$ left***) equals ($\to$ left*).  Let
$\Delta \equiv \delta, \Theta$.
The following proof figure shows that ($\to$ left***) is derived:
$$
\infer[\mbox{(c*)}]{\Gamma,\alpha \to \beta,\Delta,\alpha,\Sigma \ra \gamma}
	{\infer[(\to \mbox{r})]{\Gamma \ra \Delta \to \beta \to
				 \Sigma \to \gamma}
	{\infer{\rule{34mm}{0mm}}{\Gamma,\Delta,\beta,\Sigma \ra \gamma}}
	&
	\infer[\to \mbox{(l**)}]{\Delta \to \beta \to \Sigma \to \gamma,
	\alpha \to \beta, \Delta,\alpha,\Sigma \ra \gamma}
	  {\infer[(\to \mbox{l*})]{\alpha \to \beta,\Theta \to \beta \to \Sigma \to
	  \gamma,\Theta,\alpha,\Sigma \ra \gamma}{
	\infer{\rule{50mm}{0mm}}{\infer[(\to \mbox{r})]
		{\alpha \to \beta,\beta \to \Sigma
		 \to \gamma,\alpha,\Sigma \ra \gamma}
		 {\infer{}{\mbox{initial sequent}}}}
	}}
	}.
$$
\ \ $\Box$
%
\begin{lemma} \label{LBB'}
For any sequence $\Gamma$ of formulas and any formula $\alpha$,
$LBB' \vdash \Gamma \ra \alpha$ \ \ 
if and only if \ \ 
$L^*BB' \vdash \Gamma \ra \alpha$.
\end{lemma}

PROOF.\ \ As all rules of inferences of $L^*BB'$ are those of $LBB'$
and initial sequents of $L^*BB'$ are the same as those of $LBB'$,
$LBB' \vdash \Gamma \ra \alpha$ if $L^*BB' \vdash \Gamma \ra
\alpha$.  The rule ($\to$ left 1) is equal to ($\to$ left***).
So, it suffices to show that the rules (cut),
($\to$ left) and ($\to$ left 2)
are derived rules of $L^*BB'$.

We prove by induction on $|\Gamma|$ that (cut) is derived.
When $|\Gamma| = 1$, (cut) equals (cut**).  Let $\Gamma \equiv \Theta,\delta$.
The following proof figure shows that (cut) is derived in this case:
$$
\infer[\mbox{(the induction hypothesis)}]{\Delta \circ ( \Theta,\delta ),\Sigma
		\ra \gamma}
	{\infer[(\to \mbox{right})]{\Theta \ra \delta \to \alpha}
		{\Gamma \ra \alpha} &
		\infer[(\to \mbox{left***})]{\Delta \circ 
			( \delta \to \alpha,\delta ),\Sigma \ra \gamma}
			{\Delta,\alpha,\Sigma \ra \gamma}}.
$$

The following proof figure shows that ($\to$ left) is derived:
$$
\infer[\mbox{(cut)}]{\Delta \circ ( \alpha \to \beta ) \circ \Gamma,\Sigma
				\ra \gamma}
	{\Gamma \ra \alpha &
	\infer[(\to \mbox{left***})]{\Delta \circ ( \alpha \to \beta,\alpha ),
	\Sigma	\ra \gamma}
			{\Delta, \beta, \Sigma \ra \gamma}
	}.
$$

The following proof figure shows that ($\to$ left 2) is derived:
$$
\infer[\mbox{(cut)}]{( \alpha \to \Delta \to p ) \circ \Gamma,
\Delta \ra p}{
	\infer[(\to \mbox{right})]{\Sigma \ra \beta \to \alpha}
	{\Gamma \ra \alpha} &
	\deduce{( \alpha \to \Delta \to p ) \circ ( \beta \to \alpha,\beta ),
		\Delta \ra p}{\mbox{initial sequent}}},
$$
where $\Gamma \equiv \Sigma, \beta$.	 \ \ \ \ $\Box$

From Lemma~\ref{BB'} and Lemma~\ref{LBB'}, the next theorem follows immediately.
\begin{theorem} \label{BB'-LBB'}
For any sequence $\Gamma$ of formulas and any formula $\alpha$,
$BB' \vdash \Gamma \to \alpha$ \ \ if and only if \ \ 
$LBB' \vdash \Gamma \ra \alpha$.
\end{theorem}

In the same way as the above, we can prove the following.

\begin{theorem} \label{BB'I-LBB'I}
For any sequence $\Gamma$ of formulas and any formula $\alpha$,
$BB'I \vdash \Gamma \to \alpha$ \ \ if and only if \ \ 
$LBB'I \vdash \Gamma \ra \alpha$.
\end{theorem}

In the system $LBB'I$, the {\it length} of the proof $P$, denoted by $L(P)$,
is defined as same as in the system $LBI$.  But in the system $LBB'$,
we have to give the following definition, though it is essentially same
as that in $LBB'I$. In the below, $|\alpha|$ denotes the number of
(occurrences of) the
logical connective $\to$ appearing in a formula $\alpha$. For examples,
$|p| = 0$ and $|p \to q| = 1$.
% the definition is a little different from that in $LBI$ because of
% the complexity of initial sequents.  The {\it length} of the proof $P$ of
% the system $LBB'$, denoted by $L(P)$, is defined by $L(P) =
% (\mbox{ the number of sequents appearing in} P) + (\mbox{ the number of
% the logical connective} \to \mbox{ appearing initial sequents of} P)$.
\begin{definition}
{\rm Let $P$ be a proof of $LBB'$.  The {\em length} $L(P)$ of $P$ is
defined recursively as follows.

If $\Gamma \ra p$ is initial sequent, then
\[ L(\Gamma \ra p) =
\mbox{the number of the logical connective} \to \mbox{appearing in } \Gamma.\]

If (\#) be (cut) or ($\to$ left), then
\[ L \left( \mbox{\infer[(\#)]{\Gamma \ra \gamma}{P & Q}} \right)
 =  L(P) + L(Q) +1. \]
\[ 
\begin{array}{lcr}
L\left(\mbox{\infer[(\to \mbox{right})]{\Gamma \ra \alpha \to \beta}{P}}
\right) & = & L(P) +1. \\
L\left(\mbox{\infer[(\to \mbox{left 1})]{\Gamma \circ
( \alpha \to \beta, \alpha ),
	\Delta \ra \gamma}{P}}\right) & = & L(P) + 2|\alpha| + 1. \\
L\left(\mbox{\infer[(\to \mbox{left 2})]{( \alpha \to \Delta \to p ) \circ
	\Gamma,\Delta \ra p}{P}}\right) & = & L(P) + 2|\Delta \to p| - |\Delta|
	+1.
\end{array}
\]
}
\end{definition}

By the above definition, if a proof $P$ contains no cut, then $L(P)$ is
equal to the number of (occurrences of) the logical connective
$\to$ appearing in $end(P)$.
We need the following lemma to prove the cut elimination theorem for $LBB'$.
\begin{lemma} \label{right arrow}
For any sequence $\Gamma$ of formulas and any formulas $\alpha$ and $\beta$,
if a sequent $\Gamma \ra \alpha \to \beta$ has a proof $P$ of $LBB'$, \ \ 
then
$\Gamma, \alpha \ra \beta$ has a proof $Q$ of $LBB'$ such that $L(Q) < L(P)$.
\end{lemma}

PROOF.\ \ By induction on the length of $P$. \ \ $\Box$

Next we will prove the cut elimination theorem for $LBB'$.
The theorem can be proved in the same way as the system $LBI$
except the case of initial sequents and the case of semi-principal formulas.
%
\begin{theorem}[Cut elimination theorem for $LBB'$] \label{cutBB'}
If $P$ is a proof of $LBB'$, then there exists a cut-free
proof $Q$ of $LBB'$ such that $L(Q) \leq L(P)$ and $end(Q) \equiv end(P)$.
\end{theorem}

PROOF. \ \ It suffices to show that 

(*) {\it If $P$ is a proof of $LBB'$, which contains only one
cut rule, occurring as the last inference, then there exits a cut-free
proof $Q$ of $LBB'$ such that $L(Q) < L(P)$ and $end(Q) \equiv
end(P)$}.

So, let us suppose that $P$ is a proof which contains a cut only as the
last inference:
$$
\infer[\mbox{(cut)}]{\Delta \circ \Gamma,\Sigma \ra \gamma}
			{\Gamma \ra \alpha & \Delta,\alpha,\Sigma \ra \gamma}.
$$
We prove (*) by induction on the length of $P$.  In the following,
principal formulas are defined as usual and semi-principal formulas are
defined in the definitions of the rules ($\to$ left 1) and ($\to$ left 2).
We divide the proof
into the following four cases:

Case 1. $\Gamma \ra \alpha$ is an
initial sequent.

Case 2. $\Delta,\alpha,\Sigma \ra \gamma$ is an initial sequent.

Case 3. Either $\Gamma \ra \alpha$ or $\Delta,\alpha,\Sigma \ra \gamma$ is
a lower sequent of a rule such that (the occurence of) $\alpha$
is neither a principal formula nor a semi-principal formula of the rule.

Case 4. Both $\Gamma \ra \alpha$ and $\Delta,\alpha,\Sigma \ra \gamma$
are lower sequents of some rules such that principal formulas
of both rules are (occurrences of) $\alpha$.

Case 5. $\Delta,\alpha,\Sigma \ra \gamma$ is a lower sequent of ($\to$
left 1) or ($\to$ left 2) and (the occurence of) $\alpha$ is a
semi-principal formula of the rule.

Case 6. $\Gamma \ra \alpha$ is a lower sequent of ($\to$ left 2) and
(the occurence of) $\alpha$ is a semi-principal formula of the rule.

In the following, we will show (*) only for Case 2, Case 4 and Case 6.

In Case 2, the last part
of $P$ is of the form
$$
\infer[\mbox{(cut)}]{\Sigma \ra p}
			{\Gamma \ra \alpha & 
			( \beta \to \Delta \to p ) \circ ( \gamma \to \beta,
			\gamma ),\Delta \ra p}.
$$
We divide Case 2 into the following four subcases:
(Subcase 2.1) $\alpha \equiv \beta \to \Delta \to p$,
(Subcase 2.2) $\alpha \equiv \gamma \to \beta$,
(Subcase 2.3) $\alpha \equiv \gamma$,
(Subcase 2.4) $\alpha \in \Delta$.
We will show here only for Subcase 2.1 and Subcase 2.4.

In Subcase 2.1, the last part of $P$ is of the form
$$
\infer[\mbox{(cut)}]{\Gamma \circ ( \gamma \to \beta, \gamma ), \Delta \ra p}
			{\Gamma \ra \beta \to \Delta \to p & 
			( \beta \to \Delta \to p ) \circ ( \gamma \to \beta,
			\gamma ), \Delta \ra p}.
$$
Consider the proof $P'$ of which the last part is of the form
$$
\infer[(\to \mbox{left 1})]{\Gamma \circ ( \gamma \to \beta,\gamma ),\Delta
	\ra p}{\Gamma,\beta,\Delta \ra p}.
$$
By Lemma~\ref{right arrow}, the sequent $\Gamma,\beta,\Delta \ra p$ has
a cut-free proof whose length is less than $L(P)-1$.  So, we have
a cut-free proof $Q$ of $\Gamma \circ ( \gamma \to \beta,\gamma ),\Delta
\ra p$ such that $L(Q) < L(P)$.

In Subcase 2.4, the last part of $P$ is of the form
$$
\infer[\mbox{(cut)}]{(( \beta \to \Delta \to p ) \circ
	( \gamma \to \beta, \gamma ), \Sigma) \circ \Gamma,\Theta \ra p}
			{\Gamma \ra \alpha & 
	( \beta \to \Delta \to p ) \circ
	( \gamma \to \beta, \gamma ), \Sigma, \alpha, \Theta \ra p},
$$
where $\Delta \equiv \Sigma,\alpha,\Theta$.
Consider the cut-free proof $Q$ of which the last part is of the form
$$
\infer[(\to \mbox{left 1})]{(( \beta \to \Delta \to p ) \circ
	( \gamma \to \beta, \gamma ), \Sigma) \circ \Gamma,\Theta \ra p}
{\infer[(\to \mbox{left 1})]{(\beta \to \Delta \to p, \beta,
	\Sigma) \circ \Gamma,\Theta \ra p}
{\infer[(\to \mbox{left 1})]{(\Delta \to p,\Sigma) \circ \Gamma,\Theta \ra p}
{\infer{}
{\infer[(\to \mbox{left 2})]{( \alpha \to \Theta \to p ) \circ \Gamma,
	\Theta \ra p}{\Gamma \ra \alpha}}}}}.
$$
We can easily prove that $L(Q) < L(P)$.

In Case 4, $\alpha$
is of the form $\beta \to \delta$.  We divide Case 4 into the following
three subcases: (Subcase 4.1) $\alpha$ is a principal formula of ($\to$ left),
(Subcase 4.2) $\alpha$ is a principal formula of ($\to$ left 1),
(Subcase 4.3) $\alpha$ is a principal formula of ($\to$ left 2).
We will show here only for Subcase 4.1.

In Subcase 4.1, the last part
of $P$ is of the form
$$
\infer[\mbox{(cut)}]{\Sigma \circ \Gamma \circ \Delta,\Theta \ra \gamma}
	{\infer{\Gamma \ra \beta \to \delta}{\Gamma,\beta \ra \delta} &
	 \infer{\Sigma \circ ( \beta \to \delta ) \circ \Delta,\Theta
	 		 \ra \gamma}
	 	{\Delta \ra \beta & \Sigma,\delta,\Theta \ra \gamma}}.
$$
Consider the proof $P'$ of which the last part is of the form
$$
\infer[\mbox{(cut)--2}]{\Sigma \circ \Gamma \circ \Delta,\Theta \ra \gamma}
	{\infer[\mbox{(cut)--1}]{\Gamma \circ \Delta \ra \delta}{
		\Delta \ra \beta & \Gamma,\beta \ra \delta}
	 &
	 \Sigma,\delta,\Theta \ra \gamma}.
$$
We can eliminate (cut)--1 by the induction hypothesis.
The length of the proof obtained from $P'$ eliminating (cut)--1
is less than the length of $P$.  So, we can also eliminate (cut)--2
by the induction hypothesis and the length of the obtained proof
is less than the length of $P$.

In Case 6, the last part
of $P$ is of the form
$$
\infer[\mbox{(cut)}]{\Delta \circ (( \alpha \to \Theta \to p ) \circ
		\Gamma,\Theta),\Sigma \ra \gamma}
		{\infer[(\to \mbox{left 2})]{
		  ( \alpha \to \Theta \to p ) \circ \Gamma,\Theta \ra p}{
		  \Gamma \ra \alpha}
		  &
		\Delta,p,\Sigma \ra \gamma}.
$$
Consider the cut-free proof $Q$ whose last part is of the form
$$
\infer[(\to \mbox{left})]{\Delta \circ (( \alpha \to \Theta \to p ) \circ
	\Gamma,\Theta),\Sigma \ra \gamma}
	{\Gamma \ra \alpha &
	\infer[(\to \mbox{left 1})]{\Delta \circ (\Theta \to p, \Theta),
		\Sigma \ra \gamma}
{\infer{}
{\Delta,p,\Sigma \ra \gamma}}}.
$$
We can easily prove that $L(Q) < L(P)$.
 \ \ $\Box$

The cut elimination theorem for $LBB'I$ can be proved
in an easier way than that for $LBB'$.
%
\begin{theorem}[Cut elimination theorem for $LBB'I$] \label{cutBB'I}
If $P$ is a proof of $LBB'I$, then there exists a cut-free
proof $Q$ of $LBB'I$ such that $L(Q) \leq L(P)$ and $end(Q) \equiv end(P)$.
\end{theorem}

Recently, the author has known that the system $LBB'I$ is the same as
the Gentzen formulation for the system ${\bf T}_\to - {\bf W}$ in
{\bf \S8.11} of \cite{Anderson}.  But
the cut elimination theorem for the formulation has not been
proved in \cite{Anderson}.

By the cut elimination theorem and lack of the contraction rule,
only finite number of sequents can occur in a cut-free proof of
$\Gamma \ra \gamma$ for any sequent $\Gamma \ra \gamma$.  So, by
Theorem~\ref{BB'-LBB'} and Theorem~\ref{BB'I-LBB'I}, we have
%
\begin{theorem}	\label{BB'-decidable}
Both logics $BB'$ and $BB'I$ are decidable.
\end{theorem}

Now, we shall prove Powers and Dwyer's theorem.

\begin{theorem}[Powers and Dwyer's theorem] \label{Powers}
For any sequent $\Gamma \ra \gamma$, $LBB' \vdash \Gamma \ra \gamma$
\ \ if \ \ 
$LBB'I \vdash \Gamma \ra \gamma$ \ and \ $\Gamma \ra \gamma$ is non-trivial.
\end{theorem}

PROOF. \ \ We prove this by induction on the length of the cut-free
$LBB'I$ proof of the sequent $\Gamma \ra \gamma$.  We divide the proof
into the following two cases:

Case 1. $\Gamma \ra \gamma$ is a lower sequent of ($\to$ right).

Case 2. $\Gamma \ra \gamma$ is a lower sequent of ($\to$ left).

For Case 1, it is trivial.
%
In Case 2, the last part of the proof is of
the form
$$
\infer[(\to \mbox{left})]{\Delta \circ ( \alpha \to \beta ) \circ \Gamma,
\Sigma \ra \gamma}{\Gamma \ra \alpha &
\Delta,\beta,\Sigma \ra \gamma}.
$$

We divide Case 2 into the following four subcases:

Subcase 2.1.  Both $\Gamma \ra \alpha$ and $\Delta,\beta,\Sigma \ra \gamma$ are
	non-trivial.

Subcase 2.2.  $\Gamma \ra \alpha$ is non-trivial and $\Delta,\beta,\Sigma
	\ra \gamma$ is trivial.

Subcase 2.3.  $\Gamma \ra \alpha$ is trivial and $\Delta,\beta,\Sigma
	\ra \gamma$ is non-trivial.

Subcase 2.4.  Both $\Gamma \ra \alpha$ and $\Delta,\beta,\Sigma \ra \gamma$ are
	trivial.

In the following, we will show it only for Subcase 2.2. We divide Subcase 2.2
into the following two cases: (2.2.1) $\Delta = \emptyset$,\ \ 
(2.2.2) $\Delta \equiv \delta,\Theta$.

(2.2.1)\ \ The endsequent is $( \alpha \to \Sigma \to \Pi \to p ) \circ
\Gamma,\Sigma \ra \gamma$, where $\gamma \equiv \Pi \to p$ and
$\beta \equiv \Sigma \to \Pi \to p$.
Consider the proof of which the last part is of the form
$$
\infer[(\to \mbox{right})]{
	( \alpha \to \Sigma \to \Pi \to p ) \circ \Gamma,\Sigma \ra \gamma}
	{\infer{}
	{\infer[(\to \mbox{left 2})]{( \alpha \to \Sigma \to \Pi \to p )
		\circ \Gamma,\Sigma,\Pi \ra p}
	{\Gamma \ra \alpha}}}.
$$
By the induction hypothesis, the sequent $\Gamma \ra \alpha$ is provable
in $LBB'$.  So, this shows that the endsequent is provable in $LBB'$.

(2.2.2)\ \ The endsequent is $(\Theta \to \beta \to \Sigma \to \Pi \to p,
\Theta) \circ ( \alpha \to \Lambda \to q ) \circ
\Gamma,\Sigma \ra \gamma$, where $\gamma \equiv \Pi \to p$,
$\beta \equiv \Lambda \to q$ and $\delta \equiv
\Theta \to \beta \to \Sigma \to \Pi \to p$.
Consider the proof of which the last part is of the form
$$
\infer[(\to \mbox{left 1})]{
	(\Theta \to \beta \to \Sigma \to \Pi \to p,\Theta) \circ
	 ( \alpha \to \Lambda \to q ) \circ \Gamma,\Sigma \ra \gamma}
	{\infer{}
	{\infer[(\to \mbox{right})]{( \beta \to \Sigma \to \Pi \to p ) \circ
	 ( \alpha \to \Lambda \to q ) \circ \Gamma,\Sigma \ra \gamma}
	{\infer{}
	{\infer[(\to \mbox{left 2})]{( \beta \to \Sigma \to \gamma ) \circ
	 ( \alpha \to \beta ) \circ \Gamma,\Sigma,\Pi \ra p}
	{\infer[(\to \mbox{right})]{( \alpha \to \beta )
		\circ \Gamma \ra \beta}
	{\infer{}
	{\infer[(\to \mbox{left 2})]{( \alpha \to \beta )
		\circ \Gamma,\Lambda \ra q}{\Gamma \ra \alpha}}}}}}}}.
$$
By the induction hypothesis, the sequent $\Gamma \ra \alpha$ is provable
in $LBB'$.  So, this shows that the endsequent is provable in $LBB'$.
\ \ \ $\Box$
%
%
\section{Proof of Main Theorem} \label{lastsec}
\setcounter{definition}{0}
%
\begin{theorem}                           \label{base}
For any propositional variable $p$, the formula $p \to p$ is not
provable in $BB'$.
\end{theorem}

PROOF. \ \ \ 
By the cut elimination theorem for the system $LBB'$.
\ \  $\Box$

Henceforth, a formula $\alpha$ is only used to denote a formula $\alpha_{1}
\to \cdots \alpha_{n} \to p$. Hence the
number $n$ associated to $\alpha$ may be treated implicitly. 
Under such a circumstance, Nagayama \cite{Nagayama} introduced
the following notation: \\
{\bf Notation}. We denote a formula $\alpha_{i} \to \cdots \alpha_{n} \to p$
by $\overline{\alpha_i}$.
In particular, we can write $\alpha$ as $\overline{\alpha_{1}}$.

Nagayama showed in \cite{Nagayama} the following normalization
theorem for the system $LBB'I$ using the cut elimination theorem for
$LBB'I$.

\begin{theorem}[Normalization Theorem for $LBB'I$]        \label{normal}
Assume 
$\Delta, \alpha, \Gamma \ra \gamma$ is provable in $LBB'I$.
Then there are 
$\Gamma_i, \Sigma_i, \Delta_i \; (0 \leq i \leq n)$ and a cut-free proof of
$\Delta, \alpha, \Gamma \ra \gamma$
in $LBB'I$ such that:
$$
%\infer*{\Delta,\alpha, \Gamma \ra \gamma}{
       \infer[( \to \mbox{left})]{\Delta_0, \alpha, \Gamma_0 \ra p}
             {\infer*{\Sigma_1 \ra \alpha_1}{}
              &
              \infer*{\Delta_1, \overline{\alpha_2}, \Gamma_1 \ra p}
                     {\infer[( \to \mbox{left})]
                            {\Delta_{i-1}, \overline{\alpha_i},
			     \Gamma_{i-1} \ra p}
                            {\infer*{\Sigma_i \ra \alpha_i}{}
                             &
                             \infer*{\Delta_i, \overline{\alpha_{i+1}},
			      \Gamma_i \ra p}
                                     {\infer*{\Sigma_n \ra \alpha_n}{}
                                      &
                                      \infer*{\Delta_n, p, \Gamma_n \ra p}{}
                                     }}}}
%				     }
$$
\hspace{37mm}
$\infer*{\Delta, \alpha, \Gamma \ra \gamma}{},$
\\
where

\noindent (1)
a part of the proof, which we call a {\em tail}:
$$
\infer*{\Delta, \alpha, \Gamma \ra \gamma}
       {\Delta_0, \alpha, \Gamma_0 \ra p}
$$
does not contain any inference rule whose principal formula is (the occurence
of) $\alpha$.

\noindent (2)
$\Delta_{i-1}, \overline{\alpha_i}, \Gamma_{i-1} \equiv \Delta_i \circ
( \overline{\alpha_{i+1}} ) \circ 
\Sigma_i, \Gamma_i\;(1 \leq i \leq n)$.
\end{theorem}
We call the proof above, a {\it normalized proof} w.r.t. $\alpha$
of $\Delta,\alpha,\Gamma \ra \gamma$.
Notice here that by the requirement for the ($\to$ left) rule of $LBB'I$,
every $\Sigma_i$ in the above proof must be nonempty.  The following
holds. \\
(*) $\Gamma_i$ is a proper latter segment of $\Gamma_j$ for
$0 \leq j < i \leq n$. \\
Here, we say that $\Sigma$ is a latter segment of $\Gamma$ when
$\Gamma \equiv \Delta, \Sigma$.

The outline of the proof of the main theorem was obtained by Nagayama. However
due to the lack of the consideration on $LBB'$, this contained an essential
gap. With the cut-elimination theorem on $LBB'$, now we can successfully prove
the main theorem.
\begin{theorem}                           \label{main}
For any formula $\alpha$, the formula $\alpha \to \alpha$ is not
provable in $BB'$.
\end{theorem}

PROOF. \ \ \ 
Suppose otherwise.
Let $A$ be the set of all formulas $\beta$ such that $\beta \to \beta$
is provable in $BB'$.  Then $A$ is nonempty.  Let $\alpha$ be a formula
in $A$ whose length is minimum among formulas in $A$.
We consider a cut-free $LBB'$ proof
of $\alpha,\Gamma \ra p$, where $\alpha \equiv \Gamma \to p$.
We divide the proof into the following three cases according to
the last inference of the proof:
(Case 1) the last inference is ($\to$ left),
(Case 2) the last inference is ($\to$ left 1),
(Case 3) the last inference is ($\to$ left 2).
We will show here only for Case 1, however arguments for Case 2 and Case 3
are essentially  the same.

In Case 1, the last part of proof would be either one of the following type:

\noindent Subcase 1.1
$$
\infer[( \to \mbox{left})]
      {\alpha, \Delta \circ ( \beta \to \gamma ) \circ \Sigma, \Theta \ra p}
      {\alpha, \Sigma \ra \beta  &  \Delta, \gamma, \Theta \ra p},
$$
where $\Gamma \equiv \Delta \circ ( \beta \to \gamma ) \circ \Sigma, \Theta$
and $\Sigma \neq \emptyset$.

\noindent Subcase 1.2
$$
\infer[( \to \mbox{left})]
      {\alpha, \Delta \circ ( \beta \to \gamma ) \circ \Sigma, \Theta \ra p}
      {\Sigma \ra \beta   &     \alpha, \Delta, \gamma, \Theta \ra p},
$$
where $\Gamma \equiv \Delta \circ ( \beta \to \gamma ) \circ \Sigma, \Theta$.

\noindent Subcase 1.3
$$
\infer[( \to \mbox{left})]
      {\alpha, \Delta_1 \circ \Sigma_1, \Gamma_1 \ra p}
      {\Sigma_1 \ra \alpha_1   & \Delta_1, \overline{\alpha_2},
      \Gamma_1 \ra p},
$$
where $\Gamma \equiv \Delta_1 \circ \Sigma_1, \Gamma_1$ and
$\alpha \equiv \alpha_1 \to \overline{\alpha_2}$.

Our goal is to construct a shorter formula $\delta$ than $\alpha$,
such that both $\alpha \ra \delta$ and $\delta \ra \alpha$ are
provable in $LBB'$.
So, we would obtain that $\delta \ra \delta$ is provable in $LBB'$, which
contradicts to the minimality of $\alpha$. 

We argue it according to the subcases above.

{\em Subcase 1.1}.
In this case, we know that the sequent
$\alpha, \Sigma \ra \beta$ is provable in $LBB'$. 
Let $\delta$ be $\Sigma \to \beta$. Clearly $\delta$ is shorter than $\alpha$,
and
$\alpha \ra \delta$ is provable in $LBB'$. 
Now we consider the proof whose last part is of the form
$$
\infer[( \to \mbox{left 1})]
      {\delta, \Delta \circ ( \beta \to \gamma ) \circ \Sigma, \Theta \ra p}
      {\infer{}
      {\infer[(\to \mbox{left 1})]{\Delta \circ ( \beta \to \gamma, \beta ),
      	 \Theta \ra p}{\Delta, \gamma, \Theta \ra p}}}.
$$
This proof shows that 
$\delta \ra \alpha$ is provable in $LBB'$.

{\em Subcase 1.2}.
The same argument as that in Subcase 1.1 proves the claim.

{\em Subcase 1.3}.
In this case, the argument is not so simple as cases discussed in the above.
We need Nagayama's
normalization theorem for $LBB'I$.  First, we consider a normalized $LBB'I$
proof w.r.t. $\overline{\alpha_2}$ of $\Delta_1, \overline{\alpha_2},
\Gamma_1 \ra p$.
Since $\Sigma_1 \neq \emptyset$,
$|\Gamma_1|\leq n-1$. If the normalized proof has a tail whose length is 1,
then $|\Gamma_1| = n-1$. This is
because 
$\Gamma_i$ is a proper latter segment of $\Gamma_j$ for
$1 \leq j < i \leq n$.
This would imply $\Delta_1 = \emptyset$, and as a result,
$\Sigma_1 \equiv \alpha_1$ by the fact that
$\Sigma_1, \Gamma_1 \equiv \alpha_1, \cdots, \alpha_n$.
However, this would imply 
$\alpha_1 \ra \alpha_1$ were provable in $LBB'$, which contradicts to the 
minimality of the $\alpha$. 
Thus there is a tail in the normalized proof w.r.t. $\overline{\alpha_2}$ of
$\Delta_1, \overline{\alpha_2}, \Gamma_1 \ra p$ has a tail whose length is
greater than 1.
According to the last part of the normalized proof, we divide Subcase 1.3
into the following three cases
with $\alpha_i \equiv \beta \to \gamma$: \\
\noindent Subcase 1.3.1
$$
\infer[( \to \mbox{left})]
      {\Pi \circ ( \alpha_i ) \circ \Theta, \Lambda, 
\overline{\alpha_2}, \Gamma_1 \ra p}
      {\Theta \ra \beta
       &
       \Pi,\gamma, \Lambda, \overline{\alpha_2},
       \Gamma_1 \ra p},
$$
where $\Delta_1 \equiv \Pi \circ ( \alpha_i ) \circ \Theta, \Lambda$.

\noindent Subcase 1.3.2
$$
\infer[( \to \mbox{left})]
      {( \Pi, \overline{\alpha_2}, \Lambda) \circ ( \alpha_i )
       \circ \Theta, \Phi \ra p}
      {\Theta \ra \beta
       &
       \Pi, \overline{\alpha_2}, \Lambda, \gamma,
        \Phi \ra p},
$$
where $\Delta_1, \overline{\alpha_2}, \Gamma_1
\equiv ( \Pi, \overline{\alpha_2}, \Lambda) \circ ( \alpha_i )
\circ \Theta, \Phi$.

\noindent Subcase 1.3.3
$$
\infer[( \to \mbox{left})]
      {\Lambda \circ ( \alpha_i ) \circ ( \Theta, \overline{\alpha_2},
       \Pi), \Phi \ra p}
      {\Theta, \overline{\alpha_2}, \Pi \ra \beta
       &
       \Lambda, \gamma, \Phi \ra p},
$$
where $\Delta_1, \overline{\alpha_2}, \Gamma_1
\equiv \Lambda \circ ( \alpha_i ) \circ ( \Theta, \overline{\alpha_2},
\Pi),\Phi$. 

Finally we construct a shorter formula $\delta$ than $\alpha$ claimed above.
We demonstrate the construction for Subcase 1.3.3, however arguments
for Subcase 1.3.1 and Subcase 1.3.2 are essentially same.
First, consider the proof of which the last part is of the form
$$
\infer{\alpha, \Theta \circ \Sigma_1, \Pi \ra \beta}
      {\Sigma_1 \ra \alpha_1
       &
       \Theta, \overline{\alpha_2}, \Pi \ra \beta }.
$$
Let $\delta$ be $\Theta \circ \Sigma_1 \to \Pi \to \beta$.
Clearly $\delta$ is shorter than $\alpha$, and
the above proof shows that $\alpha \ra \delta$ is provable in $LBB'I$.
Since $\alpha \ra \delta$ is non-trivial,
Powers and Dwyer's theorem implies
that
$\alpha \ra \delta$ is provable in $LBB'$.

Now we consider the proof of which the last part is of the form
$$
\infer[( \to \mbox{left})]
      {\delta, \Lambda \circ ( \alpha_i ) \circ ( \Theta \circ
       \Sigma_1, \Pi), \Phi \ra p}
      {\delta, \Theta \circ \Sigma_1, \Pi \ra \beta
       &
       \Lambda, \gamma, \Phi \ra p }.
$$
Because the sequent $\delta, \Theta \circ \Sigma_1, \Pi \ra \beta$ is
trivial, it is provable in $LBB'I$.
As $\Lambda \circ ( \alpha_i ) \circ (\Theta \circ \Sigma_1,
\Pi), \Phi \equiv \Delta_1 \circ \Sigma_1,\Gamma_1$,
this shows that $\delta \ra \alpha$ is provable in $LBB'I$.
Since $\delta \ra \alpha$ is non-trivial,
Powers and Dwyer's theorem implies
that
$\delta \ra \alpha$ is provable in $LBB'$.  Therefore $\delta \ra \delta$ is
provable in $LBB'$.  But this contradicts the minimality of the length
of $\alpha$.
\ \ $\Box$

By Theorem~\ref{Powers} and Theorem~\ref{main}, we have Theorem~\ref{mainBB'}.
As a trivial formula is not provable in the logic $BB'$, of course it is
not provable in the logic $B$.  So, we have Theorem~\ref{mainB} by
Theorem~\ref{B-Powers}.  It follows from Theorem~\ref{mainB} and
Theorem~\ref{BI-decidable} that the logic $B$ is decidable.  Therefore,
we have Theorem~\ref{decidable} by Theorem~\ref{BI-decidable} and
Theorem~\ref{BB'-decidable}.

{\bf Acknowledgement.} The author would like to thank M. Nagayama
for sending him her manuscript~\cite{Nagayama}.  The last section
of the present paper
would never exist without Nagayama's paper.
The author also wishes to thank J. Slaney, R.K. Meyer, H. Ono, E.P. Martin,
M.W. Bunder and referees for useful discussions with them and
for pointing out to him errors,
some of which are serious, in the previous versions.
The author thanks M. Tatsuta for his \TeX 's style file proof.sty. 
\nocite{Anderson2}
\nocite{Routley}
% \bibliography{logic}
% \bibliographystyle{jplain}
\begin{thebibliography}{10}

\bibitem{Anderson}
Alan~Rose Anderson and Nuel D.~Belnap Jr.
\newblock {\em Entailment: The logic of relevance and necessity}, Vol.~1.
\newblock Princeton university Press, 1975.

\bibitem{Anderson2}
Alan~Rose Anderson, Nuel D.~Belnap Jr., and J.~Michael Dunn.
\newblock {\em Entailment: The logic of relevance and necessity}, Vol.~2.
\newblock Princeton university Press, 1992.

\bibitem{Gentzen}
Gerhard Gentzen.
\newblock Untersuchungen \"{u}ber das logische schliessen.
\newblock {\em Mathematische Zeitschrift}, Vol.~39, pp. 176--210, 405--431,
  1935.
\newblock Translated in \cite{Szabo}.

\bibitem{Komori86}
Yuichi Komori.
\newblock Predicate logics without the structure rules.
\newblock {\em Studia Logica}, Vol.~45, pp. 393--404, 1986.

\bibitem{Mar}
Errol~P. Martin and Robert~K. Meyer.
\newblock Solution to the {$P-W$} problem.
\newblock {\em Journal of Symbolic Logic}, Vol.~47, pp. 869--887, 1982.

\bibitem{Nagayama}
Misao Nagayama.
\newblock Syntactic solution to the {$P-W$} problem.
\newblock submitted to Journal of Symbolic Logic, 1993.

\bibitem{OnoKomo}
Hiroakira Ono and Yuichi Komori.
\newblock Logics without the contraction rule.
\newblock {\em Journal of Symbolic Logic}, Vol.~50, pp. 169--201, 1985.

\bibitem{Routley}
Richard Routley, Robert~K. Meyer, Val Plumwood, and Ross~T. Brady.
\newblock {\em Relevant logics and their rivals 1}.
\newblock Ridgeview, 1982.

\bibitem{Szabo}
Manfred~E. Szabo.
\newblock {\em The collected papers of Gerhard Gentzen}.
\newblock North-Holland, Amsterdam, 1969.

\bibitem{Takeuti}
Gaisi Takeuti.
\newblock {\em Proof theory}, Vol.~81 of {\em Studies in Logic and the
  Foundations of Mathematics}.
\newblock North-Holland, Amsterdam, 1975.

\end{thebibliography}
\end{document}
