\section{Soundness of the Deep Nested Sequent FILL}\label{sec:soundness}

\begin{definition}
A nested sequent $S$ is BiILL-\emph{valid} if there is an arrow $I\to\tau^s(S)$
in the free BiILL-category.
A nested sequent is a (nested) \emph{FILL-sequent} if it has no nesting of
sequents on the left of $\seq$, and no occurrences of $\excl$ at all. 
\end{definition}
The formula translation of $\tau^s$ (see Section~\ref{sec:cats}) can be adapted
straightforwardly to map FILL-sequents to
FILL-formulae. Such a sequent $S$ is FILL-valid if there is
an arrow $I\to\tau^s(S)$ in the free FILL-category.

In the Isabelle proofs we defined a FILL-sequent $S$ as a sequent such that
$\tau^s(S)$ has no occurrence of $\excl$.

%% The calculus $\biilldn$ enjoys a `separation' property
%% between the FILL fragment using only $\punit$, $\tunit$,
%% $\ltens$, $\parr$, and $\limp$ and the dual fragment
%% using only $\punit$, $\tunit$, $\ltens$, $\parr$, $\excl$.
Let $\filldn$ be the proof system obtained from
$\biilldn$ by restricting to FILL-sequents and removing the rules
$pr_1$, $pl_2$, $\excl_l^d$ and $\excl_r^d$. 
Our goal in this section is to show that $\filldn$ is sound w.r.t. FILL categories. 

%% \begin{theorem}[Separation~\cite{Clouston13CSL}]
%% Nested FILL-sequents are $\filldn$-provable iff they are $\biilldn$-provable.
%% \end{theorem}

In our formalisation, we in fact defined 
the rules \texttt{filldn} of $\filldn$ without requiring 
the sequents involved to be FILL-sequents.
We then defined a corresponding set \texttt{sfilldn} of rules, requiring
that the sequents are FILL-sequents. 
\begin{verbatim}
dn_der_biill_sfill : "[| ?c : derrec biilldn ?ps;
    ALL U. (U, ntau True ?c) : ipsubfml^* --> U ~: excl_fmls |] ==>
    ?c : derrec sfilldn ?ps"
\end{verbatim}

The soundness proof consists of a series of lemmas showing that
the rules of $\filldn$ preserves validity going downward (from premises
to conclusion). We illustrate one particularly challenging lemma that
involves context merging. 

%% \marginpar{Omit what ?}OMIT THIS - it doesn't seem any more significant than dozens of similar ones
%% we needed
%% \begin{lemma}\label{lem:basic_arr}
%% An arrow $A\otimes B\to C$ exists in the free FILL-category iff an arrow $A\to
%% B\limp C$ exists. Further, arrows of the following types exist for all formulae
%% $A,B,C$:
%% \begin{enumerate}
%% \item $A\limp B\limp C \;\to\; A\otimes B\limp C$ and
%%   $A\otimes B\limp C \;\to\; A\limp B\limp C$
%% \item $(A\limp B)\parr C \;\to\; A\limp B\parr C$.
%% \end{enumerate}
%% \end{lemma}

%% \begin{lemma}\label{lem:ctxt}
%% Let $X[~]$ be a positive FILL-context. If there exists an arrow $f:
%% \tau^s(S)\to\tau^s(T)$ in the free FILL-category then there also exists an arrow
%% $\tau^s(X[S])\to\tau^s(X[T])$.
%% %
%% Hence if $X[S]$ is FILL-valid then so is $X[T]$.
%% \end{lemma}

%% Rather than formalising the notion of a positive FILL-context, 
%% we simply note that, since when we use this theorem, $T$ will contain 
%% `$\seq$' we can assume that $\tau^a(T)$ contains an `$\excl$'.
%% This is enough to give the required conclusion.

%% \begin{verbatim}
%% fill_ctxt_cat_nseq : "[| ([?XS], ?XU) : ctxt {([?S], ?U)};
%%   (?W, ntau False ?U) : ipsubfml^*; ?W : excl_fmls; 
%%   ALL U. (U, ntau True ?XU) : ipsubfml^* --> U ~: excl_fmls |] ==>
%%   (ntau True ?XS |- ntau True ?XU) :
%%     derrec (rulefs fill_cat_rules) {ntau True ?S |- ntau True ?U}"
%% \end{verbatim}

%% \begin{lemma}\label{lem:hollow}
%% Given a multiset $\Vc$ of \emph{hollow} FILL-sequents, there exists an
%% arrow $\bot\to\tau^s(\Vc)$ in the free FILL-category.
%% \end{lemma}

%% \begin{verbatim}
%% fill_hollows_derF : "[| ?V : hollows;
%%   ALL U. (U, ntau False ?V) : ipsubfml^* --> U ~: excl_fmls |] ==>
%%   (ntau False ?V |- T) : derrec (rulefs fill_cat_rules) ?ps"
%% \end{verbatim}

%% \begin{lemma}\label{lem:merg}
%% Given a multiset $\Tc\in\Tc_1\merge\Tc_2$ of sequents and formulae, there is an
%% arrow $\tau^s(\Tc_1)\parr\tau^s(\Tc_2)\to\tau^s(\Tc)$ in the free FILL-category.
%% \end{lemma}

%% \begin{verbatim}
%% fill_rmerge_derT : "[| (?Ta, ?Tb, ?Tc) : rmerge;
%%   ALL U. (U, ntau True ?Tc) : ipsubfml^* --> U ~: excl_fmls |] ==>
%%   (ntau True ?Ta +++ ntau True ?Tb |- ntau True ?Tc) :
%%     derrec (rulefs fill_cat_rules) ?prems"
%% \end{verbatim}

\begin{lemma}\label{lem:merg_tens}
Take $X[~]\in X_1[~]\merge X_2[~]$ and $\Tc\in\Tc_1\merge\Tc_2$. Then the
following arrows exist in the free FILL-category for all $A, B,
\Gamma_1 $ and $\Gamma_2$:
\begin{enumerate}
\item $\tau^s(X_1[\Gamma_1\seq A,\Tc_1])\otimes\tau^s(X_2[\Gamma_2\seq B,\Tc_2])
  \;\to\; \tau^s(X[\Gamma_1,\Gamma_2\seq A\otimes B,\Tc])$;
\item $\tau^s(X_1[\Gamma_1\seq A,\Tc_1])\otimes\tau^s(X_2[\Gamma_2,B\seq \Tc_2])
  \;\to\; \tau^s(X[\Gamma_1,\Gamma_2,A\limp B\seq \Tc])$;
\item $\tau^s(X_1[\Gamma_1,A\seq \Tc_1])\otimes\tau^s(X_2[\Gamma_2,B\seq \Tc_2])
  \;\to\; \tau^s(X[\Gamma_1,\Gamma_2,A\parr B\seq \Tc])$;
\end{enumerate}
\end{lemma}
This lemma corresponds to soundness of branching logical rules 
of $\filldn.$ 
We proved the inductive part (involving the contexts $X_i$ and $X$) once,
in the form of \texttt{fill\_rmerge1\_der\_nseq}.
Then we proved the base case (without $X_i$ and $X$) for each connective, 
resulting in three theorems \texttt{lem27s} of which one is shown.
\begin{verbatim}
fill_rmerge1_der_nseq : "[| (?Ta, ?Tb, ?Tc) : rmerge1 (?A, ?B, ?C);
  ?prems = {ntau True ?A &&& ntau True ?B |- ntau True ?C};
  (?W, ntau False ?C) : ipsubfml^* & ?W : excl_fmls;
  ALL U. (U, ntau True ?Tc) : ipsubfml^* --> U ~: excl_fmls |] ==>
  (ntau True ?Ta &&& ntau True ?Tb |- ntau True ?Tc) :
    derrec (rulefs fill_cat_rules) ?prems"
lem27s (first one) :
  "[| (?A, ?B, ?C) : dn_ands; (?Ta, ?Tb, ?Tc) : rmerge1 (?A, ?B, ?C);
    ALL U. (U, ntau True ?Tc) : ipsubfml^* --> U ~: excl_fmls |] ==>
  (ntau True ?Ta &&& ntau True ?Tb |- ntau True ?Tc) :
    derrec (rulefs fill_cat_rules) {}"
\end{verbatim}

\begin{theorem}\label{thm:filldn_sound}
%$\filldn$ rules preserve FILL-validity.
%Every rule of $\filldn$ preserves FILL-validity.
For every rule of $\filldn$, if the premises are FILL-valid then so
is the conclusion.
\end{theorem}

\begin{verbatim}
filldn_rules_valid : "[| (?ps, ?c) : filldn;
  ALL U. (U, ntau True ?c) : ipsubfml^* --> U ~: excl_fmls |] ==>
  (T |- ntau True ?c) : derrec (rulefs fill_cat_rules)
    ((%p. T |- ntau True p) ` set ?ps)" 
\end{verbatim}

\begin{theorem}
\label{thm:filldn-conserv}
A FILL-formula is $\fill$-valid iff
it is $\filldn$-provable, and BiILL is conservative over FILL.
\end{theorem}

%% Note that the form of the theorem \texttt{filldn\_cat\_equiv} reflects
%% that we defined the rules \texttt{filldn} of $\filldn$ without requiring 
%% the sequents involved to be FILL-sequents.
%% The consequence of this is that while many of the proofs were simpler, 
%% in other cases we have to explicitly state conditions such as the first
%% condition of the following theorem.

%% We then defined a corresponding set \texttt{sfilldn} of rules, requiring
%% that the sequents are FILL-sequents.  However we still require the first
%% condition in the theorem \texttt{sfilldn\_cat\_equiv} 
%% because nothing in the definition of \texttt{fill\_cat\_rules} requires
%% that the formulae are free of exclusions.

%% \begin{lemma}
%%   If every proper subformula $U$ of $A$ is not a $\mlrx$-formula then
%%   the nested sequent $\mltp \seq A$ is (cut-free) derivable in
%%   $\filldn$ iff the display sequent $\mltp \vdash A$ is derivable in
%%   the deducibility relation defined using the categorical semantics
%%   for $\fill$ and hence $A$ is $\fill$-valid.
%% \begin{verbatim}
%% filldn_cat_equiv : "ALL U. (U, ?A) : ipsubfml^* --> U ~: excl_fmls 
%%   ==> ((T => ?A) : derrec filldn {}) =
%%       ((T |- ?A) : derrec (rulefs fill_cat_rules) {})"
%% \end{verbatim}
%% \end{lemma}

%% Note that it is also possible to prove soundness of $\filldn$ w.r.t. FILL syntactically,
%% i.e., via a translation into Schellinx's sequent calculus for FILL~\cite{Schellinx:Some}. 
%% See~\cite{ARXIV} for details. 

%% Finally, the consequence for $\filldc$ (and likewise $\fillsn$) of this result.

%% \begin{theorem}
%% \label{thm:filldn-sound}
%% If a FILL-formula is $\filldc$-provable, then it is $\fill$-valid.
%% \end{theorem}

%% That is, the display calculus $\filldc$ is sound for $\fill$, even though 
%% a $\filldc$-proof may contain intermediate steps whose $\tau$-translation 
%% contains `$\excl$'.

%% \begin{lemma}
%%   If $A$ and $B$ are free of exclusions, and $A \vdash B$ is cut-free
%%   provable in $\biilldc$ then it is derivable in the deducibility
%%   relation defined using the categorical semantics for $\fill$ and
%%   hence $A \mlim B$ is $\fill$-valid.
%% \begin{verbatim}
%% fill_dc_sound : "[| ALL U. (U, ?A) : ipsubfml^* --> U ~: excl_fmls;
%%        ALL U. (U, ?B) : ipsubfml^* --> U ~: excl_fmls;
%%       (?A |- ?B) : derrec (rulefs rlscf) {} |] ==>
%%       (?A |- ?B) : derrec (rulefs fill_cat_rules) {}"
%% \end{verbatim}
%% \end{lemma}

%% Note that the condition that $A$ and $B$ contain no exclusions reflects the
%% fact that our formalization defines formulae to (possibly) contain $\excl$.
%% But the theorem can be interpreted in a world in which $\excl$ does not exist
%% (noting the obvious fact that a $\filldc$-proof of an end-sequent which does
%% not contain $\excl$ is entirely $\excl$-free). 

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