

% We have now done this with FILL, both strengthening
% confidence in our CSL paper and more importantly showing the way that
% this useful methodology should be formalised in the future.

% Fig 1 seems incomplete, as it is missing $\biilldn$ (from which
% $\filldn$ is derived from the separation property). I'm also not sure
% what the meaning of the single-headed vs double-headed arrows are.
% E.g. $\biilldc$ and $\filldc$ are equivalent so should be a
% double-headed arrow maybe? I mostly find the figure confusing to be
% honest.

% The paragraph starting "The display property of display and shallow
% nested sequent calculi corresponds to the categorical notion of
% adjunctions" is mostly cut-and-pasted from the abstract and doesn't
% read very clearly. First, it's not really the case that the display
% property corresponds to adjunctions; it's more that the display
% property stems from every connective coming equipped with an
% adjunction. Familiar example - conjunction and implication. The phrase
% "an extension of the desired logic with additional adjunctions", which
% is good enough for an abstract but a bit vague on its own, can then be
% more precisely explained by saying the connectives without adjunctions
% in the logic, e.g. disjunction, must be supplied with one to get the
% display property, effectively embedding the logic of interest into a
% larger logic. The question is then whether the larger logic is
% conservative over the original, i.e. whether questions of the original
% logic are answered correctly be the larger logic. This conservativity
% does not hold for all logics, but when it does deep nested sequent
% calculi's "separation property" is ideal for proving it.

% The paragraph on FILL could more explicitly make our case for that -
% FILL's proof theory has been the source of some error in the past, and
% the proof theoretical approaches to it are either complex in form (as
% with Bierman, Bellin, Hyland and de Paiva) or simple in form at the cost
% of complex proofs of correctness (our work). Ours is the first
% machine-checked work on FILL, finally establishing the correctness of
% a proof theory for this logic.

% Finally - no conclusion, e.g. no related or future work? No mention
% that this formalisation was important for rooting out a major but
% subtle error in our original conservativity proof?
% Regards,

%   Ranald

% K, at Alwen's request here's a suggested new first two paragraphs. I
% suggest that they could replace the first four paragraphs of the
% current intro. This is pretty brutal in the sense that it involves
% cutting a lot of material that explains in more depth the various
% different proof styles. Perhaps some of this material is too essential
% to cut; perhaps not. But I do think that the intro should cut to the
% important stuff - what Jeremy has achieved - more rapidly.

% **********

\section{Introduction}\label{s-intro}

%\subsection{Gentzen Sequent Calculi: Pros and Cons}

% Sequent calculi provide a rigorous basis for meta-theoretic studies of
% various logics. The central theorem is cut-elimination/admissibility,
% which states that detours through lemmata can be avoided, since it can
% lead to many important meta-logical properties like consistency,
% interpolation, and Beth definability. Cut-free sequent calculi are
% also used for automated deduction, for nonclassical extensions of
% logic programming, and for studying the connection between normalising
% lambda calculi and functional programming.  Sequent calculi, and their
% extensions, therefore play an important role in logic and computation.
% It therefore makes
% sense to develop general modular approaches to proof theory.

Belnap's Display Calculi~\cite{Belnap82JPL,belnap-linear} and
Kashima's deep (inference) nested sequent
calculi~\cite{kashima-cut-free-tense} are two powerful modular
approaches to structured proof theory with many similarities, but with
contrasting strengths. Display calculi are often easy to design for a
given logic~\cite{Gore:SLD} and enjoy a generic algorithm for
cut-elimination. But they usually require the logic to be expanded
with additional new logical connectives, begging the question of
conservativity, and hence soundness, with respect to the original
logic. They also do not enjoy a genuine subformula property and hence
are ill-suited to backwards proof search. Deep nested sequent calculi,
on the other hand, are not so easy to design, do not come equipped
with generic cut-elimination, but do have a genuine subformula
property.
%Their design is also easier using an extension of the original
%logic, but 
Often, they enjoy a ``separation property'' which trivially
ensures conservativity, and hence soundness, with respect
to the original logic.  Recent work claims the best of both
worlds by giving sequent calculi in both styles for various
logics~\cite{Brunnler09AML,poggiolesi-tree-hypersequents,Gore10AiML,Gore11LMCS,Strassburger13,Park13},
with the crux being the equivalence of the display and deep
nested calculi.

Proving the equivalence of display and deep nested calculi is
technically intricate and can involve the verification of hundreds of
cases. Such proofs proceed via an intermediate calculus, a
\emph{shallow} inference nested sequent calculus, and it is the proof
of the equivalence of shallow and deep systems that is the most
demanding, requiring that every possible interaction of shallow and
deep proof rules be covered. We hence have a fruitful proof theoretic
methodology which cries out both for mechanised proof checking to
increase confidence in its results, and for the use of automated
tactics to reduce the drudgery of attaining them. We
describe such a formalisation for Full
Intuitionistic Linear Logic (FILL)~\cite{Hyland:Full}, following our earlier
work on display and deep nested calculi for this logic~\cite{Clouston13CSL}.

% Sequent calculi provide a rigorous basis for meta-theoretic studies of
% various logics. The central theorem is cut-elimination/admissibility,
% which states that detours through lemmata can be avoided, since it can
% lead to many important meta-logical properties like consistency,
% interpolation, and Beth definability. Cut-free sequent calculi are
% also used for automated deduction, for nonclassical extensions of
% logic programming, and for studying the connection between normalising
% lambda calculi and functional programming.  Sequent calculi, and their
% extensions, therefore play an important role in logic and computation.

% %There are 
% Two properties
% % which 
% are crucial for the utility of
% traditional Gentzen sequent calculi
% %,especially for backward proof search.  
% One is the subformula property, which requires that all
% formulae that appear in the premises be subformulae of the conclusion,
% since it guarantees that each logical rule reduces the complexity of
% the task. The other is the ability to alter the logical rules to
% absorb the structural rules while preserving both cut-elimination and
% the subformula property. 
% % Then, various techniques, like loop-checking, can be applied to tame
% % backward proof search using sequent calculi.

%\subsection{General Sequent Frameworks: Hyper-sequents, Labels, Display}

\begin{figure}[t]
$$
\xymatrix{
\mbox{$\fill$-category} \ar[r] & \mbox{$\biill$-category} \ar@{<->}[r] & \mbox{$\biilldc$} \ar@{<->}[d] \\
\mbox{$\filldn$} \ar[u] & \mbox{$\biilldn$} \ar@{-->}[l] & \mbox{$\biillsn$} \ar@{<->}[l]
}
$$
\caption{The relation between the semantics and proof systems for FILL/BILL.}
\label{fig:relation}
\end{figure}

% Instead of proving cut-elimination for each new logic anew, proof
% theorists have developed three main modular methodologies for
% obtaining sequent calculi that guarantee the redundancy of the cut
% rule: display calculi~\cite{Belnap82JPL}, labelled calculi~\cite{Negri2005} 
% and hyper-sequent calculi~\cite{Avron91}. Each has been used to give cut-free sequent calculi for large
% classes of (non-classical) logics, and prove the
% decidability of some.
%
% These three general methodologies can be roughly 
% as below:
% \begin{description}
% \item[Display calculi:] rely on an extension of the original logical
% connectives by enough additional connectives to guaranted the
% existence of an adjoint connective for every original logical
% connective. As we shall point out, this is closely related to the
% categorical semantics of the original logic, although display calculi
% do not explicitly rely on such semantics. Display calculi enjoy 
% cut-admissibility by inspection of the rules to guarantee that they
% obey eight simple conditions given by Belnap~\cite{belnap-display}.
% They do not enjoy a genuine subformula property since they require
% explicit structural rules to guarantee modularity.
% \item[Labelled Calculi:] Labelled calculi rely on a known Kripe
%   semantics for the logic in question and they essentially reify the
%   first-order clauses of the semantic definition by utilising an
%   explicit relational atoms representing the Kripke relation. Although
%   they enjoy cut-admissibility, it is not in the language of the
%   original logic, but in the language of a translation of it into
%   first order logic.  They enjoy a subformula property, but it does
%   not lead directly to decidability because some semantic properties of the
%   explicit Kripke relation essentially become first-order universal
%   quantifiers, introducing the usual complications of contraction.
% \item[Hyper-sequent calculi:] rely on an algebraic semantics for the
%   logic in question and deliver cut-free completeness, rather than
%   cut-admissibility, by extending the algebraic semantics to ensure
%   that they enjoy a Dedekind-McNeil completion. They enjoy a genuine
%   subformula property but also sometimes require explicit structural
%   rules, hence backward proof search is sometimes possible, but not
%   always so.
% %
% \end{description}
% Thus 
%None of these general frameworks immediately lend themselves to
% backward proof search. 
% We focus on display calculi since they enjoy a
% genuine, algorithmic, cut-elimination theorem which does not rely on
% any semantics.

% The main disadvantage of display calculi is that they do not enjoy a
% genuine subformula property. Instead, display calculi can create
% arbitrarily large structures as we ``display'' and ``undisplay''
% between introduction rules. They also must contain many explicit structural
% rules as these guarantee modularity. 
% %during backward proof, but
% %they cannot be used for backward proof search. 
% Given their generality, taming display calculi is clearly desirable.
% %so in a number of papers, we have developed a methodology for doing
% %exactly this using 
% Kashima's shallow and deep 
% nested sequent
% calculi~\cite{kashima-cut-free-tense}
% offer one route, as explained next.

% Kashima's~\cite{kashima-cut-free-tense} 
% %gave a modular sequent framework for modal tense logics using 
% %nested sequent calculi come of two differentflavours.
% %Nested sequents come in two flavours. 
% %The 
% shallow inference calculi allow rules to introduce
% formulae only at the top level, similarly to traditional Gentzen
% sequents. They contain ``turn'' rules, which are analogues of the
% ``display postulates'' from display logic, enjoy a ``display
% property'' and a cut-admissibility theorem
% % very reminiscent of 
% similar to that of
% %the one from 
% display calculi. His deep inference nested sequent calculi allow rules to
% introduce formula at any arbitrary nesting level, thereby eliminating
% the need to ``display'' and ``undisplay''.  Moreover, they are bereft
% of all structural rules, including cut, since these rules are all
% ``absorbed'' into the other rules. They often retain a visual
% sub-formula property, so that mere inspection of the rules gives
% decidability. Kashima showed how to
% ``compile'' his shallow calculi for modal tense logics
% into his deep calculi for the same logics. Nested
% sequents and his technique have been significantly extended
% to handle many other logics~\cite{Brunnler09AML,Gore10AiML,Gore11LMCS,Strassburger13,Park13}.

% In a number of papers, we have developed a methodology
% for replacing structural rules with rules that propagate formulae, and
% shown that such rules can deliver decidability. Thus we have developed
% a methodology for compiling display calculi into shallow nested
% sequent calculi and converting the shallow nested sequent calculi into
% deep ones.

% The deep calculi have been
% re-invented, independently, as ``deep
% sequents''~\cite{bruennler-deep-sequents} and 
% as~\cite{poggiolesi-tree-hypersequents} ``tree
% hypesequents''. 

% %
% Kashima's nested sequent calculi are also able to handle many
% different logics, but their meta-theory is less well-developed. The
% main advantage of nested sequents is that they often retain a visual
% sub-formula property, so that mere inspection of the rules gives
% decidability of the logic in question.

% The display property of display and shallow nested sequent calculi
% corresponds to the categorical notion of adjunctions.  Indeed, the
% proof theory of many categorical logics can be developed as follows:
% define a sound and complete display calculus for an extension of the
% desired logic with additional adjunctions; translate this calculus to
% a shallow inference nested sequent calculus; translate this calculus
% to a deep inference nested sequent calculus; then prove this final
% calculus is sound with respect to the original logic. This complex
% chain of translations between the different calculi require proofs
% that are technically intricate and involve a large number of cases,
% and hence are ideal candidates for formalisation.  In the sequel, we
% outline a formalisation of our methodology for full intuitionistic
% linear logic ($\fill$), whose proof theory has a chequered history.


% Currently, the only general way of characterising classes of
% ``displayable logics'' has been Kracht's results on compiling
% primitive axioms into structural rules, capturing the same class of
% binary Kripke frames as do labelled calculi for modal logics. Our goal
% is to find a more general way to capture large classes of displayable
% logics, which can then be compiled into deep nested sequent calculi
% with rules amenable to backward proof search. Given the importance of
% adjunctions in display calculi, we believe that categorical semantics
% may provide this avenue.


$\fill$~\cite{Hyland:Full} is a substructural logic with linear
connectives $\mlcn$, $\mldn$, $\mlim$, a unit $\mltp$ for $\mlcn$, and
a unit $\mlbt$ for $\mldn$. Schellinx~\cite{Schellinx:Some} noted that
the standard multiple-conclusioned sequent rules for this logic do not
enjoy cut-elimination. Hyland and de Paiva~\cite{Hyland:Full} claimed
to have found a cut-free sequent calculus where type-annotations on
formulae tracked and blocked unsound applications of the standard
multiple-conclusioned rules. Biermann~\cite{Bierman:Note} found a
counter-example to Hyland and de Paiva's cut-elimination proof and
gave two solutions using even more complex type-annotations, one due
to Bellin. Bra\"uner and de Paiva~\cite{Brauner:Formulation} replaced
the type-annotations with a binary relation to track variable
occurrences, which also gave cut-elimination. None of these authors
give a computational interpretation for their annotations, so they are
merely complex syntactical devices to block unsound applications of
one multiple-conclusioned rule.  Recently, we gave a sound and
complete display calculus for $\fill$ and showed how it could be
compiled into two sound and complete nested sequent calculi for
$\fill$. Our shallow nested sequent calculus obeys
cut-elimination while our deep nested calculus is cut-free complete for
$\fill$, enjoys the sub-formula property, and enjoys terminating
backward proof-search, from which we obtained the NP-completeness of
the validity problem for $\fill$~\cite{Clouston13CSL}. The detailed
proofs of these results are highly technical, and require some fifty
pages to spell out~\cite{ARXIV}.
%
% Thus, the proof theoretical approaches for $\fill$ are either
% complex in form or
% simple in form at the cost of complex proofs of correctness (our
% work). 
Our formalisation formally
establishes the correctness of our proof theory for this logic.

Our final proof system $\filldn$ for $\fill$ is a nested sequent
calculus with deep inference, in which the inference rules can act on
arbitrary substructures inside a nested sequent. We derive this proof
system following the methodology we just outlined and summarised in
Figure~\ref{fig:relation} where a solid arrow indicates that
every valid formula in the source is
also valid in the target, and a dashed arrow 
represents the same notion restricted to $\fill$ formula only. 


We start at the categorical semantics for $\fill$ in which $\limp$ and
$\mlcn$ are intimately related by adjunctions shown below as~(\ref{eq:1}):
\begin{eqnarray}
   \label{eq:1}
  (A \mlcn B) \to C \mbox{ iff }
  (B \mlcn A) \to C \mbox{ iff }
  A \to (B \mlim C)
\\
   \label{eq:2}
  C\to (A \mldn B) \mbox{ iff }
  C\to (B \mldn A) \mbox{ iff }
  (C~\excl~ B) \to A
\end{eqnarray}
%% \begin{eqnarray}
%%   \label{eq:1}
%%  (A \mlcn B) \mlim C \mbox{ iff }
%%  (B \mlcn A) \mlim C \mbox{ iff }
%%  A \mlim (B \mlim C)
%% \\
%%   \label{eq:2}
%%  C~\excl~ (A \mldn B) \mbox{ iff }
%%  C~\excl~ (B \mldn A) \mbox{ iff }
%%  (C~\excl~ B) \excl~ A 
%% \end{eqnarray}
We extend $\fill$ with an ``exclusion'' connective $\excl$, which is
intimately related to linear disjunction $\mldn$ by the adjunctions
shown in~(\ref{eq:2}).  The generalisation ensures that the extended
logic $\biill$ can be encoded directly as a display calculus
$\biilldc$ (with the display property). As explained previously, it is
not obvious that $\biill$ is conservative over $\fill$, but we 
resolve this issue later. 

Sticking with $\biill$,
we prove the soundness and completeness of $\biilldc$ wrt.\
$\biill$-categories in Section~\ref{sec:cats}. From $\biilldc$, we
derive a nested sequent calculus $\biillsn$ which is very similar to a
display calculus, but with more Gentzen-like introduction rules. We
prove that $\biilldc$ and $\biillsn$ are equivalent in
Section~\ref{sec:eqdlshallow}. A problem with both $\biilldc$ and
$\biillsn$ is that the structural connective (proxy)
%, $<$ or $\seq$ respectively, 
for $\excl$ is needed when proving
purely $\fill$-formulae, even though they contain no occurrences of
$\excl$. This problem is caused by the structural rules present in
both proof systems that guarantee that each has the display
property. These structural rules can be absorbed if we allow deep
inference, so we refine our shallow nested sequent calculus $\biillsn$
into a deep nested sequent calculus $\biilldn$ for $\biill$. In
Section~\ref{sec:eqshallowdeep} we show that $\biillsn$ and $\biilldn$
are in fact equivalent. This is the most difficult part of our
methodology since it involves a highly combinatorial proof. Indeed, in
mechanising this proof, we need to consider hundreds of ways in which
the shallow rules in $\biillsn$ may interact with the deep rules in
$\biilldn.$ Automatic tactics in Isabelle/HOL help to discharge many
of these cases automatically. Unlike both $\biilldc$ and $\biillsn$,
the proof system $\biilldn$ enjoys a ``separation''
property~\cite{Clouston13CSL}: every structural connective that
appears in any cut-free proof of a formula is a structural proxy for a
logical connective of that formula. Thus a cut-free $\filldn$-proof of a
$\fill$-formula does not require the structural proxy for
$\excl$ since $\fill$-formulae never contain occurrences of $\excl$.  
Then, simply deleting the introduction rules for $\excl$ from
$\biilldn$ gives us a proof system $\filldn$ for $\fill$. We resolve
the issue of soundness by showing that
$\filldn$ is sound w.r.t.  $\fill$-categories in
Section~\ref{sec:soundness}. Section~\ref{sec:related} concludes.

The Isabelle/HOL theory files for our formalisation can be found at:

\url{http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/fill}

%\subsection{Table of Logics and Calculi}

% \begin{figure}[t]
%   \centering
% \begin{description}
% \item[$\ill$:] intuitionistic linear logic using
%   $\mlcn$,   $\mlim$, $\mltp$ as connectives
% \item[$\fill$:] $\ill$
%   extended with par 
%   $\mldn$ and
%   its unit 
%   $\mlbt$
% \item[$\biill$:] $\fill$ extended with a connective
%   $\mlrx$ which forms adjunctions with $\mldn$
% \item[\rm $\biilldc$:] our display calculus for $\biill$
% \item[\rm $\biillsn$:] our shallow nested sequent calculus for  $\biill$
% \item[\rm $\fillsn$:] our shallow nested sequent calculus for $\fill$
% \item[\rm $\biilldn$:] our deep nested sequent calculus for  $\biill$
% \item[\rm $\filldn$:] our shallow nested sequent calculus for $\fill$
% \end{description}
%   \caption{Various Logics and Calculi}
%   \label{fig:logics-and-calculi}
% \end{figure}

%% \paragraph{Outline of the paper.}

% Figure~\ref{fig:logics-and-calculi} lists the various logics and
% calculi that are discussed in the sequel.
%
%% In Section~\ref{sec:dl} we briefly describe our
%% Isabelle/HOL formalisation of our display calculi for
%% $\biill$ and Belnap's
%% cut-admissibility theorem for it.
%% %
%% In Section~\ref{sec:cats} we describe our
%% Isabelle/HOL formalisation of the categorical semantics of 
%% $\fill$ and its extension $\biill$.
%% %
%% In Section~\ref{sec:eqcatsdl} we describe how we proved the
%% soundness and completeness of the display calculus for $\biill$
%% w.r.t.\ its categorical semantics.
%% %
%% In Section~\ref{sec:shallow} we describe our formalisation of the 
%% shallow nested sequent calculus for $\biill$.
%% %
%% In Section~\ref{sec:eqdlshallow} we describe how we proved the
%% equivalence of the display calculus and the shallow nested sequent calculus.
%% %
%% In Section~\ref{sec:deep} we describe how we
%% formalised the deep nested sequent calculus for $\biill$.
%% %
%% In Section~\ref{sec:eqshallowdeep} we describe how we proved the
%% equivalence of the shallow and deep nested sequent calculi for $\biill$.
%% %
%% In Section~\ref{sec:soundness} we describe how we
%% proved the soundness of our deep nested sequent calculus for $\fill$.
%% %
%% In Section~\ref{sec:related} we describe related work.
%% %
%% In Section~\ref{sec:further} we describe further work and conclusions.

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





