\section{Conclusion}

We have given three cut-free sequent calculi for FILL without complex 
annotations, showing that, far from being a
curiosity that demands new approaches to proof theory, 
FILL is in a broad family of linear and substructural logics 
captured by display calculi.
%easily using the known methodology for building display
%calculi~\cite{Belnap82JPL,Gore:SLD}.

Various substructural logics can be defined by using a (possibly
non-associative or non-commutative) multiplicative conjunction and its
left and right residual(s) (implications). Many of these logics have
cut-free sequent calculi with
comma-separated structures in the antecedent and a single formula in
the succedent.
%
Each of these logics has a dual  logic with disjunction and its
residual(s) (exclusions); their proof theory requires sequents built out
of comma-separated structures in the succedent and a single formula in the
antecedent. 
%
These logics can then be combined using numerous ``distribution
principles''
\cite{Grishin:Generalisation,DBLP:journals/jphil/Moortgat09}, of which
weak distributivity is but one example.
%, which allow the components to interact.
However, obtaining an adequate sequent calculus for these
combinations is often non-trivial. On the other hand, display calculi
for these logics, their duals, and their combinations, are extremely
easy to obtain using the known methodology for building display
calculi~\cite{Belnap82JPL,Gore:SLD}. We followed this methodology to obtain
$\biill$ in this paper, but needed a conservativity result to ensure the
resulting calculus $\biilldc$ was sound for FILL.
%
\begin{comment}
  Various substructural logics can be defined by using a, possibly
  non-associative or non-commutative, multiplicative conjunction and
  its left and right residual(s) (implications). Many of these logics
  can be given an adequate proof-theory using sequents built out of
  comma-separated structures in the antecedent and single formulae in
  the succedent.
%
Each of these logics has a dual substructural logic defined using a
multiplicative disjunction, possibly non-associative or non-commutative,
and its left and right residual(s) (exclusions). Many of these dual logics can
be given an adequate proof-theory using sequents built out of comma-separated
structures in the succedent and single formulae in the antecedent. 
%
These logics can also be combined using numerous ``distribution
principles''
\cite{Grishin:Generalisation,DBLP:journals/jphil/Moortgat09}, of which
weak distributivity is but one example, which allow the components to
interact. However obtaining an adequate sequent calculus for these
combinations is often non-trivial. On the other hand, display calculi
for these logics, their duals, and their combinations, are extremely
easy to obtain using the known methodology for building display
calculi~\cite{Belnap82JPL,Gore:SLD}. 
\end{comment}
%
%We followed this methodology to obtain $\biill$, but needed a
%conservativity result to ensure the resulting calculus $\biilldc$ was
%sound for FILL. For the first time, we obtained this result using the
%proof-theory of display calculi. For some logics, it is also possible
%to refine these display calculi into shallow and deep nested sequent
%calculi which are cut-free complete, enjoy a true subformula
%property and enable terminating backward proof search.
%
We finally note some specific variations on FILL deserving particular
attention.

\noindent
\textbf{Grishin (a).} Adding the converse of Grishin (b) to FILL
recovers MLL. For example $(B\limp\bot)\parr C\turn B\limp C$ is provable
using Grn(b), but its converse requires Grn(a). Thus there is another
`full' non-classical extension of MILL with Grishin (a) as its
interaction principle \emph{instead} of (b). We do not know what
significance this logic may have.

\noindent
\textbf{Mix rules.} It is easy to give structural rules for the \emph{mix}
sequents $A,B\turn A,B$ and $\Phi\turn\Phi$ which have been studied
in FILL \cite{Cockett:Proof,Bellin:Subnets} and so it is natural
to ask if the results of this paper
%, such as $<$-deletion,
can be extended to
them. Intriguingly, our new structural connectives suggest a new mix rule with
sequent form $A<B\turn B>A$ which, given Grishin (b), is stronger than
the mix rule for comma (given Grishin (a), it is weaker).

\begin{comment}
\noindent
\textbf{Non-Commutativity.} We are investigating whether our general
methodology can be extended to a version of FILL where $\otimes$ and
$\parr$ are non-commutative~\cite{Cockett:Proof}.
\end{comment}

\noindent
\textbf{Exponentials.} Adding exponentials~\cite{Brauner:Cut} to
our display calculus for
FILL may be possible~\cite{belnap-linear}.

\noindent
\textbf{Additives.} While it has been suggested that FILL could be
extended with additives, the only attempt in the literature is
erroneous~\cite{DBLP:conf/obpdc/GalmicheB95}. It is not clear how easy
this extension would be
%see the footnote in
\cite[Sec. 1]{Chang:Judgmental}; it is certainly not straightforward
with the display calculus. The problem is most easily seen through the
categorical semantics: additive conjunction $\adcn$ and its
unit $\adtp$ are limits, and $p\parr\mbox{-}$ is a right
adjoint in BiILL but is not necessarily so in FILL. But right adjoints
preserve limits. Then BiILL plus additives is
not conservative over FILL plus additives, because the sequents
$(p\parr q)\adcn(p\parr r)\turn p,(q\land r)$ and $\adtp\turn p,
\adtp$ are valid in the former but not the latter, despite the
absence of $\excl$ or $<$. 
%This breakdown is a side effect of
%the display calculus tendency to multiply adjunctions. 
We are
currently investigating solutions.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LocalWords: substructural succedent BiILL conservativity subformula Grna Grnb adjoint Grishin MLL

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