\section{Introduction}

Multiplicative Intuitionistic Linear Logic (MILL) contains as connectives only
tensor $\otimes$, its unit $I$, and its residual $\limp$,
where we use $I$ rather than the usual $1$ to avoid a clash with the
categorical notation for terminal object.
The connective par $\parr$ and its unit $\bot$ are traditionally
only introduced when we move to classical Multiplicative Linear Logic (MLL),
but Hyland and de Paiva's Full Intuitionistic
Linear Logic (FILL) \cite{Hyland:Full} shows that a sensible notion of
par can be added to MILL without collapse to classicality. FILL's semantics are
categorical, with the interaction between the $(\otimes,I,\limp)$
and $(\parr,\bot)$ fragments entirely described by the equivalent formulae
shown below:
\begin{equation}\label{eq:wdis}
(p\otimes (q\parr r)) \,\limp\, ((p\otimes q)\parr r)
\qquad\qquad\qquad
((p\limp q)\parr r) \,\limp\, (p\limp(q\parr r))
\end{equation}
The first formula is variously called \emph{weak distributivity}
\cite{Hyland:Full,Cockett:Weakly}, \emph{linear distributivity}
\cite{Cockett:Proof}, and \emph{dissociativity} \cite{Dosen:Proof}. The second
we call Grishin~(b)~\cite{Gore:SLD}. Its converse, called Grishin
(a), is not FILL-valid, and indeed adding it to FILL recovers MLL.

From a traditional sequent calculus perspective, FILL is the logic specified
by taking a two-sided sequent calculus for MLL, which enjoys
cut-elimination, and restricting its $(\limp R_2)$
rule to apply only to ``singletons on the right'', giving $(\limp
R_1)$, as shown below:
\[
 \AxiomC{$\Gamma, A \sequent B$}
 \LeftLabel{$(\mlim R_1)$}
 \UnaryInfC{$\Gamma \sequent A \mlim B$}
 \DisplayProof
\qquad\qquad\qquad\qquad
 \AxiomC{$\Gamma, A \sequent B, \Delta$}
 \LeftLabel{$(\mlim R_2)$}
 \UnaryInfC{$\Gamma \sequent A \mlim B, \Delta$}
 \DisplayProof
\]
Since exactly this restriction converts Gentzen's LK for ordinary
classical logic to Gentzen's LJ for intuitionistic logic,
%while preserving cut-elimination,
FILL arises very naturally. Unfortunately
% The problem for FILL, however, is that
the resulting calculus fails cut-elimination~\cite{Schellinx:Some}%
% All published counter-examples
% involve additive connectives, but the purely
% multiplicative $(p\limp q)\parr(r\parr s)\turn p\limp(q\parr r),s$
% sequent cannot be proved without first cutting on $(p\limp q)\parr r$%
%\footnote{There is also work on natural deduction and proof nets for
%  FILL
%  \cite{Cockett:Proof,Bellin:Subnets,Martini:Experiments,dePaiva:Parigot}. In
%  this setting the problems of cut-elimination are side-stepped; see
%  the discussion of ``essential cuts'' in \cite{Cockett:Proof} in
%  particular.}%
.
(Note that there is also work on natural deduction and proof nets for FILL
\cite{Cockett:Proof,Bellin:Subnets,Martini:Experiments,dePaiva:Parigot}. In
this setting the problems of cut-elimination are side-stepped; see
the discussion of ``essential cuts'' in \cite{Cockett:Proof} in
particular.)

Hyland and de Paiva~\cite{Hyland:Full} therefore sought a middle
ground between the too weak $(\limp R_1)$ and the unsound $(\limp
R_2)$ by annotating formulae with \emph{term assignments}, and using
them to restrict the application of $(\limp R_2)$ - the restriction
requires that the variable typed by $A$ not appear free in the
terms typed by $\Delta$. Reasoning with freeness in the presence of
variable binders is notoriously tricky, and a bug was subsequently
found by Bierman \cite{Bierman:Note} which meant that the proof of the
sequent below requires a cut that is not eliminable:
\begin{equation}\label{eq:Bierman}
  (a\parr b)\parr c \turn a,(b\parr c\limp d)\parr e\limp d\parr e
\end{equation}
Bierman~\cite{Bierman:Note} presented two possible corrections to
the term assignment system, one due to Bellin. These were subsequently
refined by Br\"{a}uner and de Paiva~\cite{Brauner:Formulation} to replace
the term assignments by rules annotated with a binary relation between
formulae on the left and on the right of the turnstile, which effectively
trace variable occurrence. The only existing annotation-free sequent
calculi for FILL~\cite{DBLP:conf/obpdc/GalmicheB95,Gore:SLD} are
incorrect. The first~\cite{DBLP:conf/obpdc/GalmicheB95} uses $(\limp
R_2)$ without the required annotations, making it unsound, and
also contains other transcription errors. The second~\cite{Gore:SLD}
identifies FILL with `Bi-Linear Logic', which fails weak distributivity
and has an extra connective called `exclusion', of which more shortly.

The existing correct annotated sequent
calculi~\cite{Bierman:Note,Brauner:Formulation} have some
weaknesses. First, the introduction rules for a connective do not
define that connective in isolation, as was Gentzen's ideal. Instead,
they introduce $\limp$ on the right only when the context in which the rule
sits obeys the rule's side-condition. A consequence is that they
cannot be used for naive backward proof search since we must apply the
rule upwards blindly, and then check the side-conditions once we have
a putative derivation. Second, the term-calculus that results from the
annotations has not been shown to have any computational content since its sole
purpose is to block unsound inferences by tracking variable
occurrence~\cite{Brauner:Formulation}. Thus, $\fill$'s close
relationship with other logics is obscured by these complex
annotational devices, leading to it being described as
proof-theoretically ``curious''~\cite{Cockett:Proof}, and leading
others to conclude that $\fill$ ``does not have a satisfactory proof
theory''~\cite{Chaudhuri:Inverse}. 
% These factors may have impeded
% $\fill$'s application 
% to computer science, despite it being
% suggested as a basis 
% for
% concurrent object-oriented logic programming
% \cite{DBLP:conf/obpdc/GalmicheB95} and intrinsically parallel linear
% functional programming \cite{Brauner:Formulation}.

We believe these difficulties 
%in obtaining a simple proof theory for FILL 
arise because efforts have focused on an `unbalanced'
logic. We show that adding an `exclusion'
%\marginpar{Symmetric is
%  dangerous since it has many connotations.}
connective $\excl$, dual to
$\limp$, gives a fully `balanced' logic, which we call
Bi-Intuitionistic Linear Logic (BiILL). The beauty of $\biill$ is that
it has a simple {\em display calculus}~\cite{Belnap82JPL,Gore:SLD} $\biilldc$
that inherits Belnap's general cut-elimination theorem ``for free''.
A similar situation has already been observed in classical modal
logic, where it has proved impossible to extend traditional Gentzen
sequents to a uniform and general proof-theory encompassing the
numerous extensions of normal modal logic K. Display calculi capture a
large class of such modal extensions uniformly and
modularly~\cite{DBLP:journals/logcom/Wansing94,kracht-power} by
viewing them as fragments of (the display calculi for) tense logics,
which conservatively extend modal logic with two modalities
$\blacklozenge$ and $\blacksquare$,
respectively adjoint to
%that respectively form an adjoint
%relationship with
the original $\Box$ and $\Diamond$.

% Of course, we still need to show that we can recover FILL as a
% fragment of BiILL and this is where it gets complicated. 
In tense logics, the conservativity result is trivial since both modal
and tense logics are defined with respect to the same Kripke
semantics. 
%where tense modalities are defined via the inverse of the
%Kripke accessibility relation.
With BiILL and FILL,
however, there is no such existing conservativity result via semantics.
%
The conservativity of BiILL over FILL would follow 
if we could show that a derivation of a FILL formula in $\biilldc$
preserved FILL-validity downwards: unfortunately, this does not
hold, as explained next.

Belnap's generic cut-elimination procedure applies to $\biilldc$
because of the ``display property'', whereby any substructure of a
sequent can be displayed as the whole of either the antecedent or
succedent. The display property for $\biilldc$ is obtained via certain
reversible structural rules, called {\em display rules}, which encode
the various adjunctions between the connectives, such as the one
between par and exclusion. Any $\biilldc$-derivation of a FILL formula
that uses this adjunction to display a substructure contains
occurrences of a structural connective which is an exact proxy
for exclusion. That is, a $\biilldc$-derivation of a FILL formula may
require inference steps that have no meaning in FILL, thus
we cannot use our display calculus $\biilldc$ directly to show
conservativity of BiILL over FILL. We circumvent this problem by
showing that the structural rules to maintain the display property become
{\em admissible}, provided one uses {\em deep inference}.

% We show that FILL is conservative over BiILL via a proof-theoretic argument. 
% More precisely, we show that in constructing a proof of a FILL formula in BiILL,
% one only needs to consider inference steps which are sound in FILL. 
% This is however not true in general in our display calculus $\biilldc$. 
% Display calculi contain certain reversible structural rules, called {\em display rules}, 
% which use the various adjunctions between connectives to deliver the
% ``display property'', whereby any substructure of 
% a sequent can be displayed as the whole of either the antecedent or succedent.
% Display property is essential to guarantee that Belnap's generic
% cut-elimination procedure can be applied to $\biilldc$. However, this also
% means that a proof of a FILL formula in $\biilldc$ may
% contain occurrences of the exclusion connective, as a result of 
% a use the adjunction between par and exclusion. 
% As a consequence, the interpretation of such proofs falls 
% outside the semantics of FILL. We get around this problem by showing
% that structural rules to maintain the display property become
% admissible, provided one uses {\em deep inference}, as we shall explained next.

%argument, and
%their categorical semantics are not an appealing basis for such an argument.
%In Section~\ref{sec:conservativity}, 
%% For the first time, we 
%% prove conservativity directly 
%% through the proof theory of a display calculus,
%% using a novel sequent rewriting procedure that turns each display
%% calculus derivation of a $\fill$-formula into a tree of sequents free
%% of all traces of $\mllx$. When these sequents are interpreted
%% %as FILL-formulae
%% in the categorical semantics, the binary tree preserves $\fill$-validity
%% downwards,
%% and naturally sees rules applied deeply inside
%% structures, rather than shallowly at the top level. 
%% Thus our annotation-free display calculus for $\biill$ trivially enjoys
%% cut-elimination for $\fill$, and hints that \emph{deep inference} may be
%% appropriate.

%% Display calculi use reversible structural rules which use the
%% various adjunctions between connectives to deliver the ``display
%% property'' whereby any substructure of a sequent can be displayed as
%% the whole of either the antecedent or succedent. 
%% To maintain this property, they also use introduction rules which
%% introduce a formula as either the whole
%% of the antecedent or succedent.

%% \begin{comment}
%% , meeting Gentzen's
%% desire to have rules that define each connective uniquely. That is, we
%% cannot introduce a formula directly into an existing context as
%% exemplified by the rule $(\limp R_2)$ shown earlier, but must
%% introduce it alone as exemplified by the rule $(\limp R_1)$ shown
%% earlier. 
%% \end{comment}

%% Viewed upwards, introduction rules for display calculi 
%% use ``shallow inference'' and can require disassembling structures into an
%% appropriate form using the display rules, meaning that display calculi
%% do not enjoy a ``substructure property''. The modularity of display
%% calculi also demands explicit structural rules for associativity,
%% commutativity and weak-distributivity. These necessary aspects of
%% display calculi make them unsuitable for proof search since the
%% various structural rules and reversible rules can be applied
%% indiscriminately.

% Despite having a general cut-elimination theorem, display
% calculi\marginpar{This is not true. The logical rules do exactly what
%   Gentzen's rules do.}
% lack a genuine subformula property, in the sense that, although
% connectives are decomposed in logical rules (reading the rules
% upwards), they are replaced by structural connectives. What is worse
% is that various structural rules that are needed to get modular
% cut-elimination may introduce extra structural connectives. 

Following a methodology established for bi-intuitionistic and tense
logics~\cite{Gore10AiML,Gore11LMCS}, we show that the display calculus
for $\biill$ can be refined to a {\em nested sequent
  calculus}~\cite{kashima-cut-free-tense,Brunnler09AML}, called
$\biilldn$, which contains no explicit structural rules, and hence no
cut rule, as long as its introduction rules can act ``deeply'' on any
substructure in a given structure.  To prove that $\biilldn$ is sound
and complete for $\biill$, we use an intermediate nested sequent
calculus called $\biillsn$ which, similar to our display calculus, has
explicit structural rules, including cut, and uses {\em shallow}
inference rules that apply only to the topmost sequent in a
nested sequent. Our shallow inference calculus $\biillsn$
can simulate cut-free proofs of our display calculus $\biilldc$, and
vice versa. It enjoys cut-elimination, the display
property and coincides with the deep-inference calculus $\biilldn$
with respect to (cut-free) derivability. Together these imply that
$\biilldn$ is sound and (cut-free) complete for BiILL. Our deep nested
sequent calculus $\biilldn$ also enjoys a {\em separation property}: a
$\biilldn$-derivation of a formula $A$ uses only introduction rules
for the connectives appearing in $A.$ By selecting from $\biilldn$
only the introduction rules for the connectives in FILL, we obtain a
nested (cut-free and deep inference) calculus $\filldn$ which is
complete for FILL.  We then show that the rules of $\filldn$ are also
sound for the semantics of FILL. The conservativity
of BiILL over FILL follows since a FILL formula $A$ which is
valid in BiILL will be cut-free derivable in $\biilldc$, and hence in
$\biilldn$, and hence in $\filldn$, and hence valid in FILL.


%% The separation property allows us to give semantically
%% complete and cut-free fragments of $\biill$, such as FILL, simply by selecting the
%% introduction rules from $\biilldn$ for the desired connectives. 
%% We
%% thus obtain a cut-free deep inference calculus for $\fill$ which is
%% sound and complete, and as a consequence of the equivalence of
%% $\biilldn$ and $\biill$, we also obtain the conservativity of 
%% BiILL over FILL.


Viewed upwards, introduction rules for display calculi use shallow
inference and can require disassembling structures into an appropriate
form using the display rules, meaning that display calculi do not
enjoy a ``substructure property''. The modularity of display calculi
also demands explicit structural rules for associativity,
commutativity and weak-distributivity. These necessary aspects of
display calculi make them unsuitable for proof search since the
various structural rules and reversible rules can be applied
indiscriminately. As structural rules are admissible in the nested
deep inference calculus $\biilldn$, proof search in it is easier to
manage than in the display calculus. Using $\biilldn$, we show that
the tautology problem for $\biill$ and $\fill$ are in fact
NP-complete.
%which allows us to prove NP-completeness of $\fill$ and $\biill$.

%For full proof details we refer readers to the extended version of this paper
%\cite{ARXIV}.
%\marginpar{Delete for arXiv version}

\emph{We gratefully acknowledge the comments of the anonymous reviewers. 
This work is partly supported by the ARC Discovery Projects DP110103173
and DP120101244.}

%% \emph{We gratefully acknowledge the comments and suggestions of
%% Jeremy Dawson.}

%% A key step is in showing that all structural rules of $\biillsn$ are
%% admissible in $\biilldn.$ 
%% Then in Section~\ref{sec:conserv} we show that the deep inference system
%% enjoys some interesting properties that would be difficult to prove directly in the
%% shallow-inference system. 


% We therefore
% take the hint and develop a nested sequent calculus for \biill{} which
% allows inference rules to be applied in certain deeply nested
% contexts. The resulting deep nested sequent calculus is cut-free
% complete for \biill{} and enjoys a separation property that allows us
% to construct complete subsystems of \biill{}, including \fill. It also
% has a genuine subformula property, gives 
% terminating backward proof search, and allows us to prove that
% \biill{} and \fill{} are NP-complete.





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LocalWords: intuitionistic MLL Hyland de Paiva dissociativity residuation classicality Grishin Bierman adjoint BiILL Belnap conservativity succedent subformula Gentzen LK LJ eliminable Bellin uner annotational Kripke adjunction versa derivability

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: 

