% \documentclass[envcountsect,envcountsame]{llncs}

% \usepackage{latexsym,amsmath,amssymb,url,gastex,epigraph}

\input{prooftree}

%% Theorem environments

\spnewtheorem{defn}[theorem]{Definition}{\bfseries}{\rmfamily}
\spnewtheorem{conj}[theorem]{Conjecture}{\bfseries}{\itshape}
% \spnewtheorem{comment}[theorem]{Comment}{\bfseries}{\itshape}

%% General mathematical notations

\newcommand{\pow}[1]{\mbox{Pow}(#1)}
\newcommand{\defeq}{=_{\mbox{\scriptsize{def}}}}
\newcommand{\restrict}{\upharpoonright}
\newcommand{\nat}{\mathbb{N}}
\newcommand{\natzero}{\mathbb{N}_0}
\newcommand{\integers}{\mathbb{Z}}
\newcommand{\range}[2]{\{{#1},\ldots,{#2}\}}
\newcommand{\setcomp}{\;|\;}
\newcommand{\pair}[2]{\langle{#1},{#2}\rangle}
\newcommand{\partialfn}{\rightharpoonup}
\newcommand{\mathmin}[1]{\mbox{min}(#1)}
\newcommand{\mathmax}[1]{\mbox{max}(#1)}


%% Language
\newcommand{\fv}[1]{{\mathcal{V}(#1)}}
\newcommand{\vars}{\mathcal{V}}
\newcommand{\monoid}{\langle R,\circ,e \rangle}
\newcommand{\abgroup}{\langle R,\circ,e,-\rangle}



%% Proof systems

\newcommand{\LJ}{\mathrm{LJ}}
\newcommand{\LK}{\mathrm{LK}}
\newcommand{\hilbert}[1]{\mathrm{HL}_{#1}}
\newcommand{\LBI}{\mathrm{LBI}}
\newcommand{\dl}[1]{\mathrm{DL}_{#1}}
\newcommand{\dcalc}{\mathcal{D}}

%% Display logic structures

\newcommand{\emp}{\mathbf{0}}
\newcommand{\aemp}{\emptyset}
\newcommand{\memp}{\varnothing}
\newcommand{\inv}{\natural}
\newcommand{\ainv}{\sharp}
\newcommand{\minv}{\flat}
\newcommand{\app}{\bullet}
\newcommand{\aapp}{\mathrel{;}}
\newcommand{\mapp}{\mathrel{,}}
\newcommand{\imp}{\mathbin{- \! {\bullet}}}
\newcommand{\aimp}{\Rightarrow}
\newcommand{\mimp}{\multimap}

\newcommand{\dpost}{\rightleftarrows_D}
\newcommand{\displayeq}{\equiv_{D}}
\newcommand{\adrewr}{\rightarrow_{AD}}
\newcommand{\assocrewr}{\rightarrow_A}
\newcommand{\adeq}{\equiv_{AD}}
\newcommand{\plaindel}[2]{\mbox{$#1 \setminus #2$}}
\newcommand{\del}[2]{\mbox{$(#1) \setminus #2$}}
\newcommand{\builtfrom}[2]{#1 \lhd #2}
\newcommand{\notbuiltfrom}[2]{#1 \ntriangleleft #2}
\newcommand{\con}{{\cal C}}


%% Logical symbols

\newcommand{\true}{\top}
\newcommand{\false}{\bot}
\renewcommand{\implies}{\rightarrow}
\renewcommand{\conj}{\mathrel{\&}}
\newcommand{\atrue}{\true_{a}}
\newcommand{\afalse}{\false_{a}}
\newcommand{\aconj}{\conj_{a}}
\newcommand{\adisj}{\vee_{a}}
\newcommand{\mtrue}{\true^*}
\newcommand{\mfalse}{\false^{\!*}}
\newcommand{\mneg}{\mathord{\sim}}
\newcommand{\mor}{\mathrel{\overset{\vcenter{\offinterlineskip
\hbox{\scriptsize{$\ast$}}\vskip-1.5ex}}{\vee}}}
\newcommand{\wand}{\mathrel{\hbox{---}\llap{$\ast$}}}
\newcommand{\bigand}{\textstyle\bigwedge}
\newcommand{\bigor}{\textstyle\bigvee}
\newcommand{\dlantform}[1]{\Psi_{#1}}
\newcommand{\dlconform}[1]{\Upsilon_{#1}}
\newcommand{\myC}{\textbf{C}}
\newcommand{\myS}{\textbf{S}}

%% Provability and satisfiability relations

\newcommand{\seq}[2]{{#1 \vdash #2}}
\newcommand{\entails}[3]{#2 \vdash_{#1} #3}
\newcommand{\notseq}[2]{#1 \not\vdash #2}
\newcommand{\drvequiv}[2]{#1 \dashv\vdash #2}
\newcommand{\sat}[2]{#1 \models_\rho #2}
\newcommand{\notsat}[2]{#1 \not\models_\rho #2}
\newcommand{\drvof}[1]{\begin{array}{c}\vdots\\{#1}\end{array}}
\newcommand{\drvfrom}[2]{\[{#1} \leadsto {#2}\]}
\newcommand{\LADI}{\mathrm{LADI}}

%% Logical proof rule labels

\newcommand{\ax}{\mbox{(Id)}}
\newcommand{\bunchequiv}{\mbox{(Equiv)}}
\renewcommand{\cut}{\mbox{(Cut)}}
\newcommand{\acut}{\mbox{(ACut)}}
\newcommand{\mcut}{\mbox{(MCut)}}
\newcommand{\subst}{\mbox{(Subst)}}
\newcommand{\truel}{\mbox{($\true$L)}}
\newcommand{\truer}{\mbox{($\true$R)}}
\newcommand{\falsel}{\mbox{($\false$L)}}
\newcommand{\falser}{\mbox{($\false$R)}}
\newcommand{\mtruel}{\mbox{($\mtrue$L)}}
\newcommand{\mtruer}{\mbox{($\mtrue$R)}}
\newcommand{\mfalsel}{\mbox{($\mfalse$L)}}
\newcommand{\mfalser}{\mbox{($\mfalse$R)}}
\newcommand{\negr}{\mbox{($\neg$R)}}
\newcommand{\negl}{\mbox{($\neg$L)}}
\newcommand{\andr}{\mbox{($\&$R)}}
\newcommand{\andl}{\mbox{($\&$L)}}
\newcommand{\orr}{\mbox{($\vee$R)}}
\newcommand{\intorr}[1]{\mbox{($\vee \mathrm{R}_{#1}$)}}
\newcommand{\orl}{\mbox{($\vee$L)}}
\newcommand{\impr}{\mbox{($\rightarrow$R)}}
\newcommand{\impl}{\mbox{($\rightarrow$L)}}
\newcommand{\starl}{\mbox{($*$L)}}
\newcommand{\starr}{\mbox{($*$R)}}
\newcommand{\wandl}{\mbox{($\wand$L)}}
\newcommand{\wandr}{\mbox{($\wand$R)}}
\newcommand{\morl}{\mbox{($\mor$L)}}
\newcommand{\morr}{\mbox{($\mor$R)}}
\newcommand{\mnegl}{\mbox{($\mneg$L)}}
\newcommand{\mnegr}{\mbox{($\mneg$R)}}
\newcommand{\atruer}{\mbox{($\atrue$R)}}
\newcommand{\afalsel}{\mbox{($\afalse$L)}}
\newcommand{\aconjl}{\mbox{($\aconj$L)}}
\newcommand{\aconjr}{\mbox{($\aconj$R)}}
\newcommand{\adisjl}{\mbox{($\adisj$L)}}
\newcommand{\adisjr}{\mbox{($\adisj$R)}}
\newcommand{\rewr}{\mbox{($\equiv$)}}
\newcommand{\rewrl}{\mbox{($\dashv\vdash$L)}}
\newcommand{\rewrr}{\mbox{($\dashv\vdash$R)}}
\newcommand{\eq}{\mbox{($=$)}}
\newcommand{\MP}{\mbox{(MP)}}

% Display rule labels

\newcommand{\adl}[2]{\mbox{(AD{#1}{#2})}}
\newcommand{\mdl}[2]{\mbox{(MD{#1}{#2})}}
\newcommand{\display}{\mbox{($\displayeq$)}}
\newcommand{\adrule}{\mbox{($\adeq$)}}

% Structural rule labels
\newcommand{\weak}{\mbox{$\mathrm{(W)}$}}
\newcommand{\contr}{\mbox{$\mathrm{(C)}$}}
\newcommand{\assoc}{\mbox{$\mathrm{(\alpha)}$}}
\newcommand{\aunitcl}{\mbox{$\mathrm{(\aemp C_L)}$}}
\newcommand{\aunitcr}{\mbox{$\mathrm{(\aemp C_R)}$}}
\newcommand{\aunitwl}{\mbox{$\mathrm{(\aemp W_L)}$}}
\newcommand{\aunitwr}{\mbox{$\mathrm{(\aemp W_R)}$}}

% Derived proof rule labels
\newcommand{\dlantl}{\mbox{($\dlantform{}$L)}}
\newcommand{\dlconr}{\mbox{($\dlconform{}$R)}}

% \begin{document} 

\section{Display calculi for (some) substructural logics}%\vspace{-0.2cm}
\label{sec:display_calc}

We now recall the class of display calculi for which Craig
interpolation is established in~\cite{brotherston-gore-interpolation}.

We assume a fixed infinite set of propositional variables.  \emph{Formulae} $F$ and \emph{structures} $X$ are then given by the following grammars, where $P$ ranges over propositional variables:
\[\begin{array}{l}
F ::= P \mid \true \mid \false \mid \neg F \mid F \conj F \mid F \vee F \mid F \implies F \mid \atrue \mid \afalse \mid F \aconj F \mid F \adisj F
\\[0.3em]
X ::= F \mid \aemp \mid \ainv X \mid X \aapp X
\end{array}\]
Formula connectives with an ``a'' subscript stand for an \emph{additive} version of that connective, while connectives without a subscript are construed as \emph{multiplicative}.
However, in the Isabelle formulation we do not duplicate the connectives in
this way --- 
rather, we identify which logical rules for which our various results apply.
We write $F,G$ etc.\ to range over formulae and $W,X,Y,Z$ etc.\ to range over structures.
If $X$ and $Y$ are structures then $\seq{X}{Y}$ is a \emph{consecution}.  

The complete set of proof rules for our display calculi is given in
Figure~\ref{fig:rules}\footnote{how to stop this going to the end of the
document?}.
As usual, we begin by giving a set of \emph{display postulates}, and taking the least equivalence closed under the postulates to be our notion of \emph{display-equivalence}.  We then have the usual \emph{display theorem}, which says that for any structure occurrence $Z$ in a consecution $\seq{X}{Y}$, one has either $\seq{X}{Y} \displayeq \seq{Z}{W}$ or $\seq{X}{Y} \displayeq \seq{W}{Z}$ for some $W$, depending on whether $Z$ occurs positively or negatively in $\seq{X}{Y}$.   Rearranging $\seq{X}{Y}$ into $\seq{Z}{W}$ or $\seq{W}{Z}$ in this way is called \emph{displaying} $Z$. We remark that the display postulates ``build in'' commutativity of the structural semi-colon, so that we consider only calculi for commutative logics.

Brotherston and Gor\'e~\cite{brotherston-gore-interpolation} consider the additive rules, collectively, and each structural rule, individually, to be \emph{optional} inclusions in their calculi.
At present, our mechanisation assumes the presence of the unit rules $\aunitwl$, $\aunitwr$, $\aunitcl$, $\aunitcr$ and the associativity rule $\assoc$.
Thus the smallest display calculus we consider gives multiplicative linear logic $\mathrm{MLL}$.
By adding the additive logical rules we obtain multiplicative-additive linear logic $\mathrm{MALL}$,
and by adding the full weakening rule $\weak$ or the full contraction rule $\contr$ we obtain affine or strict variants of these logics, respectively.
Note that rules for weakening and contraction on the right can be derived using
the display postulates from the corresponding left rules.
Of course, if we add \emph{both} weakening and contraction then we obtain standard classical propositional logic.

No matter which variant of these display calculi we consider, we have the standard \emph{cut-elimination} result due to Belnap.  Since we omit the cut rule from our presentation of the display calculi in Figure~\ref{fig:rules}, we state it here in the weaker form of \emph{cut admissibility}:

\begin{theorem}[cf.~\cite{brotherston-gore-interpolation}]
\label{thm:cut_elim} If $\seq{X}{F}$ and $\seq{F}{Y}$ are both provable then so is $\seq{X}{Y}$.  Moreover, this property is not affected by the presence or otherwise of the additive logical rules (collectively), or of any of the structural rules.
\end{theorem}


%The following definition shows how to interpret the structural connectives.

%\begin{defn}[Interpretation of structures]
%\label{defn:consecution_validity} For any structure $X$ we define the formulas $\dlantform{X}$ and
%$\dlconform{X}$ by mutual structural induction on $X$ as:
%\[\begin{array}{rcl@{\hspace{0.5cm}}rcl@{\hspace{0.9cm}}rcl@{\hspace{0.5cm}}rcl}
%\dlantform{F} & = & F &
%\dlantform{\aemp} & = & \true & \dlconform{F} & = & F & \dlconform{\aemp} & = & \false \\
%\dlantform{\ainv X} & = & \neg\dlconform{X} &
%\dlantform{X_1 \aapp X_2} & = & \dlantform{X_1} \conj \dlantform{X_2} & \dlconform{\ainv X} & = & \neg\dlantform{X} & \dlconform{X_1 \aapp X_2} & = & \dlconform{X_1} \vee \dlconform{X_2}\\
%\end{array}\]
%For any consecution $\seq{X}{Y}$ we define its \emph{formula interpretation} to be
%$\seq{\dlantform{X}}{\dlconform{Y}}$.
%\end{defn}
%
%\begin{defn}[Antecedent and consequent parts]
%\label{defn:parts} A \emph{part} of a structure $X$ is an occurrence of one of its substructures.
%We classify the parts of $X$ as either \emph{positive} or \emph{negative} in
%$X$ as follows:
%\begin{itemize}
%\item $X$ is a positive part of itself;
%\item a negative / positive part of $X$ is
%    a positive / negative part of $\ainv X$;
%\item a positive / negative part of $X_1$ or %of
%      $X_2$ is a positive / negative part of $X_1 \aapp X_2$.
%\end{itemize}
%$Z$ is said to be an \emph{antecedent / consequent part} of a
%consecution $\seq{X}{Y}$ if it is a positive / negative part of $X$ or a
%negative / positive part of $Y$.
%\end{defn}





%\begin{defn}[Display-equivalence]
%\label{defn:displayeq} We define \emph{display-equivalence}
%$\displayeq$ to be the least equivalence on consecutions containing the (symmetric) relation $\dpost$ given by
%the following \emph{display postulates}:
%\[\begin{array}{c@{\hspace{0.3cm}}c@{\hspace{0.3cm}}c@{\hspace{0.3cm}}c@{\hspace{0.3cm}}c}
%\seq{X ; Y}{Z} & \dpost & \seq{X}{\ainv Y ; Z} & \dpost & \seq{Y ; X}{Z} \\
%\seq{X}{Y ; Z} & \dpost & \seq{X ; \ainv Y}{Z} & \dpost & \seq{X}{Z ; Y} \\
%\seq{X}{Y} & \dpost & \seq{\ainv Y}{\ainv X} & \dpost & \seq{\ainv\ainv X}{Y}
%\end{array}\]
%\end{defn}
%
%Note that Defn.~\ref{defn:displayeq} builds in the
%commutativity of $\aapp$ on the left and right of consecutions,
%i.e., we are assuming both $\&$ and $\vee$ commutative.  %This
%%makes life slightly easier, but is not crucial to our
%%developments.

%\begin{proposition}[Display property]
%\label{prop:display} For any antecedent / consequent part $Z$
%of a consecution $\seq{X}{Y}$, one can construct a structure
%$W$ such that $\seq{X}{Y} \displayeq \seq{Z}{W}$ / $\seq{X}{Y}
%\displayeq \seq{W}{Z}$, respectively.
%\end{proposition}
%
%\begin{proof}(Sketch) For any $\seq{X}{Y}$, the display
%  postulates of Defn.~\ref{defn:displayeq} allow us to display each of
%  the immediate substructures of $X$ and $Y$ (as the
%  antecedent or consequent as appropriate). The proposition follows by
%  iterating.  \qed\end{proof}

%\begin{comment}
%\label{com:logics}
%Under the formula interpretation of consecutions given by
%Definition~\ref{defn:consecution_validity}, certain of our display calculi
%can be understood as follows:
%\begin{description}
%\item[$\dcalc_{\mathrm{MLL}} \!=\!$]
%$\dcalc_0 + \assoc, \aunitcl, \aunitcr, \aunitwl, \aunitwr$ is multiplicative linear logic (LL);
%\item[$\dcalc_{\mathrm{MALL}} =$]
% $\dcalc_0^+ + \assoc, \aunitcl, \aunitcr, \aunitwl, \aunitwr$ is multiplicative additive LL;
%\item[$\dcalc_{\mathrm{CL}} =$]
% $\dcalc_0 + \assoc, \aunitcl, \aunitcr, \weak, \contr$ is
%  standard classical propositional logic.
%\end{description}
%\end{comment}

\begin{figure}[t] 
{\small
\mbox{\bf Display postulates:}
\[\begin{array}{c@{\hspace{0.3cm}}c@{\hspace{0.3cm}}c@{\hspace{0.3cm}}c@{\hspace{0.3cm}}c}
\seq{X ; Y}{Z} & \dpost & \seq{X}{\ainv Y ; Z} & \dpost & \seq{Y ; X}{Z} \\&\\
\seq{X}{Y ; Z} & \dpost & \seq{X ; \ainv Y}{Z} & \dpost & \seq{X}{Z ; Y} \\&\\
\seq{X}{Y} & \dpost & \seq{\ainv Y}{\ainv X} & \dpost & \seq{\ainv\ainv X}{Y}
\end{array}\]\vspace{0.1cm}

\mbox{\bf Identity rules:}
\[\begin{array}{c@{\hspace{1.5cm}}c}%@{\hspace{0.8cm}}c}
\begin{prooftree}
\phantom{X'}
\justifies
\seq{P}{P}
\using \ax
\end{prooftree}
&
\begin{prooftree}
\seq{X'}{Y'}
\justifies
\seq{X}{Y}
\using \;\;\seq{X}{Y} \displayeq \seq{X'}{Y'} \;\;\display
\end{prooftree}
\end{array}\] \vspace{0.1cm}

\mbox{\bf Multiplicative logical rules:}
\[\begin{array}{c@{\hspace{0.6cm}}c@{\hspace{0.6cm}}c@{\hspace{0.6cm}}c}
\begin{prooftree}
\seq{\aemp}{X}
\justifies
\seq{\true}{X}
\using \truel
\end{prooftree}
&
\begin{prooftree}
\phantom{X}
\justifies
\seq{\aemp}{\true}
\using \truer
\end{prooftree}
&
\begin{prooftree}
\seq{F ; G}{X}
\justifies
\seq{F \conj G}{X}
\using \andl
\end{prooftree}
&
\begin{prooftree}
\seq{X}{F}
\phantom{w}
\seq{Y}{G}
\justifies \seq{X \aapp Y}{F \conj G}
\using \andr
\end{prooftree}
\\ & \\
\begin{prooftree}
\phantom{X}
\justifies
\seq{\false}{\aemp}
\using \falsel
\end{prooftree}
&
\begin{prooftree}
\seq{X}{\aemp}
\justifies
\seq{X}{\false}
\using \falser
\end{prooftree}
&
\begin{prooftree}
\seq{F}{X}
\phantom{w}
\seq{G}{Y}
\justifies
\seq{F \vee G}{X \aapp Y} \using \orl
\end{prooftree}
&
\begin{prooftree}
\seq{X}{F ; G} \justifies \seq{X}{F \vee G} \using \orr
\end{prooftree}
\\ & \\
\begin{prooftree}
\seq{\ainv F}{X} \justifies \seq{\neg F}{X} \using \negl
\end{prooftree}
&
\begin{prooftree}
\seq{X}{\ainv F} \justifies \seq{X}{\neg F} \using \negr
\end{prooftree}
&
\begin{prooftree}
\seq{X}{F}
\phantom{w}
\seq{G}{Y}
\justifies
\seq{F \implies G}{\ainv X \aapp Y} \using \impl
\end{prooftree}
&
\begin{prooftree}
\seq{X \aapp F}{G}
\justifies
\seq{X}{F \implies G}\using \impr
\end{prooftree}
\end{array}\]\vspace{0.1cm}

\mbox{\bf Additive logical rules:}
\[\begin{array}{c@{\hspace{0.6cm}}c@{\hspace{0.4cm}}c}
\begin{prooftree}
\phantom{X}
\justifies
\seq{\afalse}{X}
\using \afalsel
\end{prooftree}
&
\begin{prooftree}
\seq{F_i}{X}
\justifies
\seq{F_1 \aconj F_2}{X}
\using \;i \in \{1,2\}\,\aconjl
\end{prooftree}
&
\begin{prooftree}
\seq{F}{X}
\phantom{w}
\seq{G}{X}
\justifies
\seq{F \adisj G}{X} \using \adisjl
\end{prooftree}
\\ & \\
\begin{prooftree}
\phantom{X}
\justifies
\seq{X}{\atrue}
\using \atruer
\end{prooftree}
&
\begin{prooftree}
\seq{X}{F}
\phantom{w}
\seq{X}{G}
\justifies \seq{X}{F \aconj G}
\using \aconjr
\end{prooftree}
&
\begin{prooftree}
\seq{X}{F_i}
\justifies
\seq{X}{F_1 \adisj F_2}
\using \;i \in \{1,2\}\,\adisjr
\end{prooftree}
\end{array}\]\vspace{0.1cm}

\mbox{\bf Structural rules:}
\[\begin{array}{c@{\hspace{0.6cm}}c@{\hspace{0.6cm}}c@{\hspace{0.6cm}}c}
\begin{prooftree}
\seq{\aemp ; X}{Y} \justifies \seq{X}{Y} \using \aunitcl
\end{prooftree}
&
\begin{prooftree}
\seq{X}{Y ; \aemp} \justifies \seq{X}{Y} \using \aunitcr
\end{prooftree}
&
\begin{prooftree}
\seq{X}{Y} \justifies \seq{\aemp ; X}{Y} \using \aunitwl
\end{prooftree}
&
\begin{prooftree}
\seq{X}{Y} \justifies \seq{X}{Y ; \aemp} \using \aunitwr
\end{prooftree}
\\ & \\
\multicolumn{4}{c}{
\begin{prooftree}
\seq{(W ; X) ; Y}{Z}
\justifies
\seq{W ; (X ; Y)}{Z} \using \assoc
\end{prooftree}
\qquad
\begin{prooftree}
\seq{X}{Z}
\justifies
\seq{X ; Y}{Z}
\using \weak
\end{prooftree}
\qquad
\begin{prooftree}
\seq{X ; X}{Y}
\justifies
\seq{X}{Y}
\using \contr
\end{prooftree}}
\end{array}\]}\vspace{-0.4cm}
\caption{Display calculus proof rules  In the display rule $\display$, the relation $\displayeq$ is the least equivalence containing the relation $\dpost$ given by the display postulates.\label{fig:rules}}
\label{f-rules}
\end{figure}

% \end{document} 

