\section{Separation, Conservativity, and Decidability}
\label{sec:conserv}

%\subsection{Separation}

% A nested sequent $S$ is BiILL-\emph{valid} if there is
% an arrow $I\to\tau^s(S)$ in the free BiILL-category.

In this section we return our attention to the relationship between our calculi
and the categorical semantics (Defs.~\ref{Def:FILLcat} and~\ref{def:free}).
Def.~\ref{def:tau_nested} gave a translation of nested sequents to formulae;
we can hence define validity for nested sequents.

\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. The formula
translation of Def.~\ref{def:tau_nested} hence maps 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.
\end{definition}

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$.
%A nested sequent
%$X$ is an {\em intuitionistic sequent} if it has no nesting of
%sequents on the left of an arrow, and no occurrences of $\excl$.
%% can be produced by 
%% the following grammar:
%% $$
%% X ::= (\Gamma \seq \Delta, X, \dots, X)
%% $$
%% where $\Gamma$ and $\Delta$ are multisets of intuitionistic formulas. 
%% In other words, in an intuitionistic sequent, there is no nesting to the left of the
%% sequent arrow, and the exclusion connective $\excl$ is absent. 
Let us define $\filldn$ as 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$.

\begin{theorem}[Separation]
\label{thm:separation}
Nested FILL-sequents are $\filldn$-provable iff they are
$\biilldn$-provable.
% An intuitionistic sequent is provable in $\filldn$ if and only if it is provable
% in $\biilldn.$
\end{theorem} 
\begin{proof}
  One direction, from $\filldn$ to $\biilldn$, is easy. The other
  holds because every sequent in a $\biilldn$ derivation
  of a FILL-sequent is also a FILL-sequent. 
%   One direction, from $\filldn$ to $\biilldn$, is easy. The other
%   follows from the fact that in every derivation of an intuitionistic
%   sequent in $\biilldn$, every sequent that appears in the derivation
%   is also intuitionistic.
% This can be checked by a simple inspection of the rules of $\biilldn.$ 
%% , as the only rule that can create the sequent arrow on 
%% the left is the $\excl_l$ rule. Since we start with an intuitionistic sequent, this
%% will never happen.
\end{proof}

Thm.~\ref{thm:separation} tells us that every deep inference proof of a
FILL-sequent is entirely constructed from FILL-sequents,
each with a $\tau$-translation to FILL-formulae. This contrasts 
%to 
with display
calculus proofs, which must
introduce the FILL-untranslatable $<$ even for simple theorems.
%Therefore 
By separation, and the equivalence of $\biilldc$ and $\biilldn$
(Cor.~\ref{cor:dc=dn}), the conservativity of BiILL over FILL reduces to
checking the soundness of each rule of $\filldn$.

\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}

In the proofs below we will abuse notation by omitting explicit reference to
$\tau^a$ and $\tau^s$, writing $\Gamma_1\limp\Delta_1$ for $\tau^a(\Gamma_1)\limp
\tau^s(\Delta_1)$ for example.

\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}

\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{proof}
We will prove this for a single sequent first, by induction on its size. The
base case is the sequent $\cdot\seq\cdot$, whose $\tau^s$-translation is $I\limp
\bot$. The existence of an arrow $\bot\to I\limp\bot$ is, by
Lem.~\ref{lem:basic_arr}, equivalent to the existence of $\bot\otimes I\to\bot$;
this is the unit arrow $\rho$. The induction case involves the sequent $\cdot\to
T_1,\ldots,T_l$, with each $T_i$ hollow; the required arrow exists by
composing the arrows 
%that exist by the induction hypothesis with
given by the induction hypothesis with
$\bot\to\bot\parr\cdots\parr\bot$. The multiset case then follows easily
by considering the cases where $\Vc$ is empty and non-empty.
\end{proof}

\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{proof}
We prove this for a single sequent first, by induction on its size. The base
case requires an arrow
$
(\Gamma_1\limp\Delta_1)\parr(\Gamma_2\limp\Delta_2)
\;\to\;
\Gamma_1\otimes\Gamma_2\limp\Delta_1\parr\Delta_2
$
(ref. Lem.~\ref{lm:dist}), which exists by Lem.~\ref{lem:basic_arr}(ii) and (i).
The induction case
%, involving the sequents $\Gamma^i\seq\Delta^i,T^i_1,\ldots,
%T^i_l$ for $i=1,2$,
follows similarly. The multiset case then follows easily by
considering the cases where $\Tc$ is empty and non-empty.
\end{proof}

\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}
\begin{proof}
All three cases follow by induction on the size of $X[~]$. In all 
three cases
the induction step
%, for sequents $\Gamma'_i\seq X_i[\cdots],\Tc'_i$ for $i=1,2$,
is easy, and so we focus on the base cases. By Lem.~\ref{lem:basic_arr} the base
case for (i) requires an arrow:
\begin{equation}\label{eq:mt_1}
(\Gamma_1\limp A\parr\Tc_1)\otimes(\Gamma_2\limp B\parr\Tc_2)\otimes
\Gamma_1\otimes\Gamma_2 \quad\to\quad (A\otimes B)\parr\Tc.
\end{equation}
By the `evaluation' arrows $\varepsilon$ there is an arrow from the left hand
side of \eqref{eq:mt_1} to $(A\parr\Tc_1)\otimes(B\parr\Tc_2)$.
Composing this with weak distributivity takes us to $((A\parr\Tc_1)
\otimes B)\parr\Tc_2$, and then to $(A\otimes B)\parr\Tc_1\parr
\Tc_2$. Lem.~\ref{lem:merg} completes the result. The base cases for (ii) and
(iii) follow by similar arguments (App.~\ref{app:conserv}).
\end{proof}

\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{proof}
As FILL-sequents nest no sequents to the left of $\seq$, we can
modify the rules of Fig.~\ref{fig:fbilld} to replace the multisets $\Sc,\Sc'$
of sequents
and formulae with multisets $\Gamma,\Gamma'$ of formulae only, and
remove the hollow multisets of sequents $\Uc$ entirely (see
App.~\ref{app:conserv}).

Therefore by Lem.~\ref{lem:ctxt} the soundness of $pl_1$ amounts to the
existence in the free FILL-category of an arrow
$$
\Gamma\limp(A\otimes\Gamma'\limp\Tc')\parr\Tc \quad\to\quad
\Gamma\otimes A\limp(\Gamma'\limp\Tc')\parr\Tc.
$$
This follows by two uses of Lem.~\ref{lem:basic_arr}(i). Similarly $pr_2$
requires an arrow
$$
\Gamma\limp\Tc\parr A\parr(\Gamma'\limp\Tc') \quad\to\quad
\Gamma\limp\Tc\parr(\Gamma'\limp\Tc'\parr A)
$$
which exists by Lem.~\ref{lem:basic_arr}(ii).

$id^d$: by induction on the size of $X[~]$. The base case requires an arrow
$I\to p\limp p\parr\Vc$, which exists by Lems.~\ref{lem:hollow}
and~\ref{lem:basic_arr}. Induction involves a sequent $\cdot\seq
X[p\seq p,\Vc],\Tc'$, with $\Tc'$ hollow, and hence requires an arrow $I\to I\limp
X[p\seq p,\Vc]\parr\Tc'$. By Lem.~\ref{lem:basic_arr} and the arrow
$I\otimes I\to I$
we need an arrow $I\to X[p\seq p,\Vc]\parr\Tc'$; by the
induction hypothesis we have $I\to X[p\seq p,\Vc]$; this extends to $I\to
X[p\seq p,\Vc]\parr\bot$; Lem.~\ref{lem:hollow} completes the proof.

$\bot^d_l$: by another induction on $X[~]$. The base case $I\to\bot\limp\Vc$
follows by Lems.~\ref{lem:basic_arr} and~\ref{lem:hollow}; induction
follows as with $id^d$.

$\bot^d_r$: By Lem.~\ref{lem:ctxt} and the unit property of $\bot$.

$I^d_l$: By Lem.~\ref{lem:ctxt} we need an arrow $(\Gamma\limp\Tc)
\otimes\Gamma\otimes I\to\Tc$; this exists by the unit property of $I$
and the `evaluation' arrow $\varepsilon$.

$I^d_r$: another induction on $X[~]$. The base case arrow $I\to I\limp I\parr
\Vc$ exists by Lems.~\ref{lem:basic_arr} and~\ref{lem:hollow};
induction follows as with $id^d$.

$\otimes^d_l$, $\limp^d_r$, and $\parr^d_r$ are trivial by the formula
translation.

$\otimes^d_r$: compose the arrow $I\to I\otimes I$ with the arrows defined by
the validity of the premises, then use Lem.~\ref{lem:merg_tens}(i). $\limp^d_l$
and $\parr^d_r$ follow similarly via Lem.~\ref{lem:merg_tens}(ii) and (iii).
\end{proof}

\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}
\begin{proof}
By Cors.~\ref{cor:filldc_complete} and~\ref{cor:dc=dn} and
Thms.~\ref{thm:separation} and~\ref{thm:filldn_sound}.
\end{proof}

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. 

Thm.~\ref{thm:filldn-conserv} gives us a sound and complete calculus 
for $\fill$ that enjoys a genuine subformula property. This in turn allows one to prove
NP-completeness of the tautology problem for $\fill$ (i.e., deciding whether a formula
is provable or not), as we show next. The complexity does not in fact change even
when one adds exclusion to $\fill.$

%\subsection{Decidablity}

%% The {\em tautology problem } in a proof system (or a logic, in the semantic sense) 
%% is the problem of determining whether a given formula is
%% provable in that proof system (resp., valid in the logic). 
%% One of the nice features of the deep inference calculus $\biilldn$
%% is that, since structural rules are absent, the size of the structures (sequents) in a proof
%% of a formula $B$ is bounded by the size of $B.$ This gives us immediately a decision procedure
%% for the tautology problem for $\biill.$ We show in fact we can prove a more precise bound, i.e., NP-completeness,
%% of the complexity of the tautology problem for both $\biill$ and $\fill.$ 
%% This result is new as far as we know, although the NP-completeness of $\fill$ is 
%% not surprising, and can be easily proved using
%% existing sequent calculi for $\fill$ as well. What is more interesting here is that adding exclusion
%% to $\fill$ does not change the complexity. 

\begin{theorem}
The tautology problems for BiILL and FILL are NP-complete. 
\end{theorem}
\begin{proof}
({\em Outline.}) 
Membership in NP is proved by showing that every cut-free proof of a formula $A$ in $\biilldn$
can be checked in PTIME in the size of $A$. This is not difficult
to prove given that each connective in $A$ is introduced exactly once in the proof. 
NP-hardness is proved by encoding Constants-Only MLL (COMLL), which is 
NP-hard~\cite{Lincoln94}, in $\filldn.$
\end{proof}
% \begin{theorem}
% The tautology problems for BiILL and FILL are NP-complete. 
% \end{theorem}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LocalWords: intuitionistic iff conservativity subformula BiILL Defs Thm multiset eq COMLL MLL nnf PTIME

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

