\documentclass[a4paper]{llncs}
\usepackage{amsmath}
\usepackage{amssymb}
\newcommand{\bimbo}{ Bimb\'{o} }
\newcommand{\limp}{\to}
\newcommand{\verum}{\ensuremath{\mathbf{t}}}
\newcommand{\rarrow}{\ensuremath{R_{\limp}}}
\newcommand{\rarrowt}{\ensuremath{R_{\limp}^{\verum}}}
\newcommand{\tarrow}{\ensuremath{T_{\limp}}}
\newcommand{\tarrowt}{\ensuremath{T_{\limp}^{\verum}}}
\newcommand{\lrarrow}{\ensuremath{LR_{\limp}}}
\newcommand{\lrarrowc}{\ensuremath{\myb{LR_{\limp}}}}
\newcommand{\lrarrowt}{\ensuremath{LR_{\limp}^{\verum}}}
\newcommand{\lrarrowtc}{\ensuremath{\myb{LR_{\limp}^{\verum}}}}
\newcommand{\lrarrowstr}{\ensuremath{LR_{\limp\semic}}}
\newcommand{\ltarrow}{\ensuremath{LT_{\limp\semic}}}
\newcommand{\ltarrowt}{\ensuremath{LT_{\limp\semic}^{\verum}}}
\newcommand{\ltarrowc}{\ensuremath{\myb{LT_{\limp\semic}^{\verum}}}}
\newcommand{\tcirc}{\ensuremath{\bigcirc\!\!\!\!\verum}}
\newcommand{\ltarrowtcirc}{\ensuremath{LT_{\limp\semic}^{\tcirc\;}}}
\newcommand{\str}{\ensuremath{Str}}
\newcommand{\astr}[2]{#1\{#2\}}
\newcommand{\seq}{\ensuremath{\vdash}}
\newcommand{\myb}[1]{\ensuremath{[#1]}}
\newcommand{\semic}{\ensuremath{\; ; \;}}
\newcommand{\smsc}{\ensuremath{;}}
\newcommand{\tick}{\checkmark}
\newcommand{\strttleft}{(T\ensuremath{_{\verum}\seq\smsc})}
\newcommand{\strbleft}{(B\ensuremath{\seq\smsc})}
\newcommand{\strbpleft}{(B\ensuremath{'\seq\smsc})}
\newcommand{\strwleft}{(W\ensuremath{\seq\smsc})}
\newcommand{\strktleft}{(K\ensuremath{_{\verum}\seq\smsc})}
\title{Results from their second paper}
\begin{document}
\maketitle
\begin{description}
\item[Page 3:] We proved cut theorems and other important properties
about these calculi -- including that all agree on the pure
implicational formulas.
\item[Page 4:] \ltarrowtcirc is equivalent to \rarrowt whereas
\ltarrowt is equivalent to \tarrowt. The difference between the two
calculi is that in \ltarrowtcirc, $\verum$ is left identity
only, and in \ltarrowtcirc, it is full identity because of the two new
rules $\strktleft$ and $\strttleft$, which are special versions of thinning and
permutation.
\item[Page 4:] We define an algorithm (called $\pi$), which turns proofs in
\ltarrowtcirc into proofs in \lrarrowt.
\item[Page 4:] Every theorem of \tarrowt{} has an irredundant proof in
\lrarrowtc , and it is straightforward to convert those proofs into
proofs in \lrarrowt{} that do not contain the ($\seq\verum$) axiom.
\item[Page 4:] We define an algorithm (called $\tau$), which turns
proofs in \lrarrowt{} into proofs in \ltarrowtcirc{}, by restoring
the distinctions inherent to \ltarrowtcirc.
\item[Page 4:] In section 1, we prove that the addition of the
constant \verum{} does not prevent the decidability of \rarrow{} to be
extended to \rarrowt.
\item[Page 4:] In section 2, we consider the relationship of the
calculi \ltarrowtcirc and \lrarrowt, especially, from the point of
view of transforming proofs in the former into proofs in the latter.
\item[Page 4:] Section 3 describes the transformations
from \lrarrowtc{} to \lrarrowt, and
further, to \ltarrowtcirc.
\item[Page 4:] Section 4 completes the proof of the decidability of
\ltarrow. There we show that proofs that do not belong to
\ltarrowt{} can be unequivocally distinguished from those that do.
\item[Page 4:]It is well-known that \rarrowt is conservative over
\rarrow, which also follows from the cut theorem for \lrarrowtc.
\item[Page 4:] A consecution calculus for \tarrow has to include
\verum. Footnote 7 then says: There is a consecution calculus for
\tarrow{} without \verum{} in \bimbo 2007b Section 3.2. However, the
absence of \verum{} makes the calculus intricate and difficult to
use. There is a so-called merge calculus for \tarrow{} in Anderson and
Belnap (1975), which is more similar to a sequent calculus than to a
consecution calculus. We are not aware of the existence of a sequent
calculus (of the usual sort) for \tarrow.
\item[Page 4:] Therefore, we first prove that the conservative
extension of \lrarrowc{} with \verum{} inherits decidability from
\lrarrowtc (Raj thinks this should be just \lrarrowc ).
\item[Curry's Lemma:] Curry’s Lemma states that if a sequent
$\alpha'\seq A$ is obtainable by contractions from a sequent
$\alpha \seq A$ and the latter has a proof in \lrarrowc, then
$\alpha' \seq A$ has a proof in \lrarrowc{} of length less than or equal
to the length of the proof of $\alpha \seq A$.
\begin{quote}
So this is just height-preserving contraction admissibility for \lrarrowc?
\end{quote}
\item[Page 5:] A proof tree is redundant if it contains a branch with
a sequent $\alpha' \seq A$ below another sequent $\alpha \seq A$
from which it can be obtained by contractions (including the
degenerate case of the null contraction, i.e., where a sequent is
simply repeated).
\item[Page 5:] This opens the door to Kripke's distinctive
contribution, which shows that every branch in such an irredundant
proof search tree is finite. First, two sequents $\alpha \seq A$ and
$\alpha' \seq A$ are said to be cognate, when exactly the same
formulas -- not counting multiplicity -- occur in them. This
partitions sequents into cognation classes. Kripke's Lemma says that
if a sequence of distinct cognate sequents $\Gamma_0, \Gamma_1,
\cdots $, is irredundant in the sense that for no $\Gamma_i,
\Gamma_j$ (where $i < j$), $\Gamma_i$ is obtainable from $\Gamma_j$
by contractions, then the sequence is finite.
\item[Page 5:] Lemma 1. If a sequent $\alpha' \seq A$ is obtainable by
contractions from a sequent $\alpha \seq A$ and the latter has a
proof in \lrarrowtc, then $\alpha' \seq A$ has a proof of length
less than or equal to the length of the proof of $\alpha\seq A$. The
proof is by induction on the length of the proof of $\alpha\seq A$.
\begin{quote}
Raj: So \lrarrowtc{} has contraction admissibility?
\end{quote}
\item[Page 6:] We proved in \bimbo and Dunn (2012b) (see lemma 2.5)
that \rarrow{} and \lrarrowc{} have the same set of theorems.
\item[Page 6:] \rarrowt{} is decidable.
\item[Page 6:] We proved in \bimbo and Dunn (2012b, Section 4) that
the single cut rule is admissible in \ltarrowtcirc{} and that $A$ is
a theorem of \rarrowt{} iff $\verum\seq A$ is provable in
\ltarrowtcirc. The cut theorem implies that $\verum\seq A$ has a
cut-free proof in \ltarrowtcirc provided $A$ is a theorem of \rarrowt.
\item[Page 7:] Definition ($\pi$) transformation. Let $\delta$ be a
proof in \ltarrowtcirc{}. The transformation $\pi$ of $\delta$ is the
following consecutive applications of steps (1)-(4):
\begin{enumerate}
\item replace every $\semic$ by a comma;
\item Omit all the parentheses from complex structures
\item Omit the lower sequent, if the corresponding lower consecution
was the result of an application of the \strbleft, \strbpleft, or
\strttleft{} rules.
\item Insert finitely many sequents between
$\Gamma, A_1, A_1, A_2, A_2, \cdots , A_n, A_n \seq B$
and
$\Gamma, A_1, A_2, \cdots , A_n \seq B$
if the corresponding lower consecution resulted by an application
of \strwleft{} to two occurrences of a complex structure comprising
$n$ atomic structures that we denote by $A_1, \cdots , A_n$. The
inserted $n-1$ sequents are consecutive contractions of
$A_1, \cdots , A_n$
starting from
$\Gamma, A_1, A_1, A_2, A_2, \cdots , A_n, A_n \seq B$.
\end{enumerate}
\item[Page 7:] The transformation in effect ``blurs'' the proof $\delta$ so
that (1) semi-colons are seen as commas, (2) parentheses are not
seen (unless they are in a formula), (3) identical sequents just
above each other are squashed into one, and (4) contractions of
complex structures are emulated by consecutive contractions on
their atomic structures. For our purposes, it is even more
important that certain features of the proofs are not destroyed.
\item[Page 7:] Footnote 11 says This list may contain multiple
occurrences of a formula; however, for the purposes of describing
this step it is easier to work with a listing of atomic structures
whether they are identical formulas or not.
\item[Page 7:] Notice that if $n > 1$ in step (4), then different
orderings of contractions (of different formulas) result in
distinct proofs in \lrarrowt. We give an example of the
transformation.
\item[Page 8:] Let $\pi(U \seq A)$ be the result of apply steps
(1)-(2) from this definition. It is obvious that $\pi(U \seq A)$
is a traditional sequent.
\item[Page 8:] Lemma 4 (Simplification). If $\delta$ is a proof in
the sense of \ltarrowtcirc, then $\pi(\delta)$ obtained by the
transformation is a proof in \lrarrowt.
\item[Page 9:] Lemma 5: If $A$ is a theorem of \tarrowt, then
$\verum\seq A$ is provable in \lrarrowtc. However, it may be
useful to emphasise that $A$ has an irrerundant proof in
\lrarrowtc.
\item[Page 10:] Lemma 6. If $\delta$ is a proof in \ltarrowt, then
$\pi(\delta)$ contains the applications of the connective rules
and of the contraction rule in the original order in $\delta$.
\item[Page 10:] If A is a theorem of \rarrow, then it is provable in \ltarrowt
(without the cut rule).
\item Every theorem of \tarrow is of the form $A_1 \limp A_2 \limp
\cdots \limp (A_n \limp p)$ where $n \in \mathbb{N}^+$ and $p$ is a
propositional variable.
\item We will assume that a given formula $A$ is tested for
provability using \lrarrowtc. This can mean -- equivalently -- searching
for a proof of either of the sequents $\verum \seq A$ or $\seq A$.
\item[Page 12:] Lemma 7. If $\delta$ is a proof of $\verum \seq A$ in
\lrarrow, then there is a proof $\delta'$ of the same end sequent that
does not contain occurrences of the axiom $\seq \verum$.
\item[Page 13] Lemma 8. If $\astr{U}{X \semic Y} \seq A$ is provable in
\ltarrowtcirc, then $\astr{U}{\verum \semic Y \semic X} \seq A$ and
$\astr{U}{\verum \semic (Y \semic X)} \seq A$ are provable
\item[Page 13] Lemma 9. If $\astr{U}{X \semic Y \semic Z} \seq A$ is provable
in \ltarrowtcirc, then $\astr{U}{V} \seq A$ is provable too, where
$V$ is any permutation and grouping of the three structures $X$
and $Y$ and $Z$ with a $\verum$ on the left and associated with the
leftmost of those three structures.
\item[Page 14] Lemma 10. If $\astr{U}{ X \semic Y \semic Z} \seq A$ is
provable in \ltarrowtcirc, then $\astr{U}{V} \seq A$ is provable
too, where $V$ is any permutation and grouping of the three
structures $X$ and $Y$ and $Z$ associated together with a $\verum$ as
the leftmost structure.
\item[Page 15] If there are $n > 1$ consecutive applications of the \strwleft
rule in $\delta$ at this point, then we consider them
together. First, we divide n into all the possible ordered sums
(including $n$ itself). (For example, if $n = 3$ then we get $1 + 1 +
1$, $1 + 2$, $2 + 1$ and $3$.) It is trivial that there are finitely
many possibilities for each n. The total number of ordered sums is
$2^{n−1}$.
\item[Page 18] Lemma 11 (Distinction). If $A$ is a theorem of \tarrow{}
with $\seq\verum$-free proofs $\delta_1$, $\delta_2$, $\cdots$,
$\delta_n$ in \lrarrowt obtained from the irredundant proofs of
$\verum \seq A$ in \lrarrowtc, then $\exists i$ such that $\tau
(\delta_i)$ is a proof of $\verum\seq A$ in $\ltarrow$.
\end{description}
\end{document}