%\section{Equivalence of Categorial and Display Turstiles}\label{sec:eqcatsdl}

In the following, 
\texttt{(?A |- ?B)} is a sequent with arbitrary formulae
on each side.  Arbitrary structures would appear as \texttt{(\$?A |- \$?B)}~\cite{DBLP:conf/tphol/DawsonG02}.

%% \begin{lemma}
%% Every formula-sequent
%% \texttt{(?A |- ?B)} is derivable in
%% the display calculus $\biilldc$ iff it is also derivable
%% using \verb!biill_cat_rules! (containing cut).
%% \begin{verbatim}
%% dc_cat_equiv : "((?A |- ?B) : derrec (rulefs rlsb) {}) =
%%   ((?A |- ?B) : derrec (rulefs biill_cat_rules) {})"
%% \end{verbatim}
%% \end{lemma}

%% Using cut-admissibility for $\biilldc$ we obtain
\begin{theorem}\label{thm:dc=biill}
$\biilldc$ %(Fig.~\ref{Fig:dc}) 
is \emph{sound} and \emph{cut-free complete} for
BiILL-validity (where the appellation \texttt{cf} captures cut-free).
\begin{verbatim}
dc_cat_equiv_cf : "((?A |- ?B) : derrec (rulefs rlscfb) {}) =
  ((?A |- ?B) : derrec (rulefs biill_cat_rules) {})"
\end{verbatim}
\end{theorem}


%% \begin{corollary}\label{cor:filldc_complete}
%% The display calculus $\filldc$ is cut-free complete for
%% FILL-validity.
%% \end{corollary}

%% Soundness of $\filldc$ w.r.t. FILL-validity is not obvious, as derivations
%% of a FILL formula in $\filldc$ may still use 
%% the display rule $drp$, which may introduce the structural connective for exclusion
%% that does not have any interpretation in FILL category. 
%% As we shall see in the next sections, we can get rid of the display rules and
%% other structural rules by adopting deep inference. 




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