\section{Introduction}\label{s-intro}
Belnap's Display Calculus~\cite{Belnap82JPL} is a powerful modular
approach to structural proof theory. Display calculi are often easy to
design for a given logic~\cite{Gore:SLD} and enjoy a generic algorithm
for cut-elimination. However they usually require the logic to be
expanded with new structural connectives, raising 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.
Various authors~\cite{Brunnler09AML,poggiolesi-tree-hypersequents,Gore10AiML,Gore11LMCS,Park13,Clouston13CSL} have addressed
these shortcomings by using some variation of
\emph{nested sequent calculus} with \emph{deep
inference}~\cite{kashima-cut-free-tense}.
% There is a body of recent
% work~\cite{Brunnler09AML,poggiolesi-tree-hypersequents,Gore10AiML,Gore11LMCS,Park13,Clouston13CSL}
% that addresses these shortcomings by using some variation of
% \emph{nested sequent calculus} with \emph{deep
% inference}~\cite{kashima-cut-free-tense}.
Such deep nested calculi
employ a
syntax similar to display calculi, but lack their ease of design and
generic cut-elimination algorithm.
Conversely, deep nested calculi can
be designed to have a genuine subformula property, and
%enjoy
a
``separation property'' that trivially yields conservativity
results~\cite{Gore10AiML,Gore11LMCS,Clouston13CSL}.
%As such
Since display
calculi and deep nested calculi can have contrasting strengths,
it is
useful to provide sequent calculi in both styles for
a given logic. The crux of such a development is the proof of
equivalence between 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 {\em
shallow} inference nested sequent calculus, and it is the proof of
the equivalence of shallow and deep calculi 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}.
Schellinx~\cite{Schellinx:Some} considered the
standard multiple-conclusioned sequent calculus for intuitionistic logic (where the
right-implication rule is restricted to prevent collapse to classical logic) without weakening
and contraction, and showed that it
does not enjoy cut-elimination.
Hyland and de Paiva~\cite{Hyland:Full} gave this logic (with cut) the name
Full Intuitionistic Linear Logic, and defined categorical semantics for it, giving several natural
examples of categories exhibiting the required structure. They further claimed to have found
a cut-free sequent calculus for FILL, in which term-assignments on formulae are put to
novel use to block unsound applications of right-implication, via a freeness check on
abstracted variables. Reasoning about freeness in the presence of binders is a well known
source of subtle error, and a major topic of formalisation research
(e.g.~\cite{Urban:Nominal}). Indeed Bierman~\cite{Bierman:Note} found a
counter-example to Hyland and de Paiva's cut-elimination proof exploiting a binding-related
error, and presented two solutions using even more complex type-annotations, one due
to Bellin. Bra\"uner and de Paiva~\cite{Brauner:Formulation} subsequently suggested a
cut-free calculus relying on annotations on sequents, rather than formulae. Two previous
claims in the literature to annotation-free sequent calculi for FILL were erroneous, as
discussed in~\cite{Clouston13CSL}.
Our recent contribution~\cite{Clouston13CSL} to this rather vexed history was to show that
annotations are not necessary; we gave a sound and
complete display calculus for $\fill$ and showed how it can be
compiled into two equivalent nested sequent calculi, one with shallow inference
and the other with deep inference. In particular the deep calculus is cut-free complete for
$\fill$, enjoys the sub-formula property, and supports terminating
backward proof-search, from which we obtained the NP-completeness of
the validity problem for $\fill$.
The derivation of these results, given in more detail in~\cite{ARXIV},
is unavoidably highly technical, and given its difficulty and the history of FILL outlined
above we sought to formalise our results in the proof assistant Isabelle/HOL.
The completed formalisation presented in this paper finally
establishes the correctness of a sequent calculus for this logic.
In fact an initial attempt to prove the soundness of our calculus was found
to be flawed only when we tried to formalise it (see below for more details), so this development has
been an invaluable part of even our `pen-and-paper' work.
We now outline our proof stategy~\cite{Clouston13CSL} as formalised in this paper.
FILL has the usual relation between multiplicative conjunction $\mlcn$ and
implication $\mlim$,
where $\to$ denotes an arrow in a category (see \S\ref{sec:cats}):
\begin{equation}
\label{eq:1}
(A \mlcn B) \to C \mbox{ iff }
(B \mlcn A) \to C \mbox{ iff }
A \to (B \mlim C)
\end{equation}
The \emph{display property}, which underlies the generic cut-elimination
algorithm of display calculi, requires the introduction of new structural connectives, so it is clarifying to
regard a display calculus as defining a larger logic with new logical connectives. In this case
we have a multipicative \emph{exclusion} $\excl$, defined with respect to multiplicative
disjunction (or \emph{par}) $\mldn$ in a manner dual to \eqref{eq:1}:
\begin{equation}
\label{eq:2}
C\to (A \mldn B) \mbox{ iff }
C\to (B \mldn A) \mbox{ iff }
(C~\excl~ B) \to A
\end{equation}
In \S\ref{s-deriv} and \S\ref{sec:cats},
we extend the syntax of $\fill$ with $\excl$
and extend the semantics of $\fill$ to obtain
Bi-Intuitionistic Linear Logic ($\biill$).
In \S\ref{sec:dl} we give a display calculus $\biilldc$
which is easily seen to be sound
and complete for $\biill$ and hence complete for the sublogic $\fill$.
The soundness of $\biilldc$ for
$\fill$ corresponds to the conservativity
of $\biill$ over $\fill$.
We first attempted to prove the soundness
result directly via a rewriting strategy which
removed occurrences of exclusion from
a $\biilldc$-derivation of a $\fill$-formula to give an exclusion-free
$\biilldc$-derivation of the same $\fill$-formula.
This rewriting strategy turned out to be flawed, as it may not always
terminate. Instead, we define two nested sequent calculi for $\biill$:
$\biillsn$ with shallow inference in \S\ref{sec:eqdlshallow}, and $\biilldn$ with deep
inference in \S\ref{sec:eqshallowdeep}.
The equivalence of $\biillsn$ and $\biilldn$,
established as Thm.~\ref{thm:eqshallowdeep} in \S\ref{sec:eqshallowdeep}, is the technical highlight of
the formalisation, with 616 cases verified. Thm.~\ref{thm:separation}
in \S\ref{sec:soundness} shows that because
of a \emph{separation} property, $\biilldn$ easily specialises to a deep nested calculus
$\filldn$ with no trace of exclusion. Thm.~\ref{thm:filldn_sound} then
shows that the calculus $\filldn$ is
sound
%\marginpar{changed ``complete'' to ``sound''}
for
$\fill$, thereby proving conservativity of $\biill$ over $\fill$.
\S\ref{sec:related} concludes.
% We give $\fill$ extended with $\excl$ the name Bi-Intuitionistic Linear Logic ($\biill$), and
% define syntax in \S\ref{s-deriv} and semantics in \S\ref{sec:cats} with respect to
% $\biill$, with $\fill$ as a special case. A display calculus $\biilldc$, easily seen to be sound
% and complete for $\biill$ and hence complete for the sublogic $\fill$, is then defined in
% \S\ref{sec:dl}. The soundness of this calculus $\biilldc$ for
% $\fill$ corresponds to the conservativity
% of $\biill$ over $\fill$.
% We first attempted to prove the soundness
% result directly via a rewriting strategy which
% removed occurrences of exclusion from
% a $\biilldc$-derivation of a $\fill$-formula to give an exclusion-free
% $\biilldc$-derivation of the same $\fill$-formula.
% This rewriting strategy turned out to be flawed, as it may not always
% terminate. Instead, we define two nested sequent calculi for $\biill$:
% $\biillsn$ with shallow inference in \S\ref{sec:eqdlshallow}, and $\biilldn$ with deep
% inference in \S\ref{sec:eqshallowdeep}.
% The equivalence of $\biillsn$ and $\biilldn$,
% established as Thm.~\ref{thm:eqshallowdeep} in \S\ref{sec:eqshallowdeep}, is the technical highlight of
% the formalisation, with 616 cases verified. Thm.~\ref{thm:separation}
% in \S\ref{sec:soundness} shows that because
% of a \emph{separation} property $\biilldn$ easily specialises to a deep nested calculus
% $\filldn$ with no trace of exclusion. Thm.~\ref{thm:filldn_sound} then
% shows that the calculus $\filldn$ is
% \textbf{sound}
% %\marginpar{changed ``complete'' to ``sound''}
% for
% $\fill$, thereby proving conservativity of $\biill$ over $\fill$.
% \S\ref{sec:related} concludes.
Our methodology is summarised
%by the diagram
below, 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$ formulae only:
%We annotate each
%arrow with
%a reference to the definition or
%the theorem justifying the implication denoted by
%the arrow.
%\marginpar{[AT:] I can't find where the separation theorem is proved. Jeremy?}
%\begin{figure}%[t]
%$$
\begin{equation*}
\xymatrix@C=12ex{
\mbox{$\fill$-category} \ar[r]^{\mbox{{\small Def. \ref{Def:FILLcat}}}} &
\mbox{$\biill$-category} \ar@{<->}[r]^{~\mbox{\small Thm. \ref{thm:dc=biill}}} &
\mbox{$\biilldc$} \ar@{<->}[d]^{\mbox{\small Thm. \ref{thm:biilldc=biillsn}}} \\
\mbox{$\filldn$} \ar[u]^{\mbox{{\small Thm. \ref{thm:filldn_sound}}}} &
%\mbox{$\filldn$} \ar[u]^{\mbox{{\small Thm. \ref{thm:filldn-conserv}}}} &
\mbox{$\biilldn$} \ar@{-->}[l]^{~\mbox{ \small Thm.\ \ref{thm:separation}}} &
\mbox{$\biillsn$} \ar@{<->}[l]^{\mbox{{\small Thm. \ref{thm:eqshallowdeep}}}}
}
\end{equation*}
We used Isabelle/HOL 2005
%rather than the latest version
so that we
could rework the cut-elimination proofs from our previous work on
formalising cut elimination for display
calculi~\cite{DBLP:conf/tphol/DawsonG02}. % for this particular display calculus.
As discussed
%we shall see
in \S\ref{sec:eqdlshallow}, one
%of the problems
problem we found was the lack of support for nested datatypes
involving multisets. The Isabelle/HOL theory files for our
formalisation are at:
\url{http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/fill}
%$$
%\caption{The relation between the semantics and proof systems for FILL/BILL.}
%\label{fig:relation}
%\end{figure}
%% \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.
%\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: