\section{Formulae, sequents and derivations} %{Reasoning About Derivations and Derivability}
\label{s-deriv}
We explain briefly the data structures we use to encode formulae, structures,
sequents and derivations.
%
%% Proof-theorists typically work with sequents $\Gamma
%% \vdash \Delta$ where $\Gamma$ and $\Delta$ are ``collections'' of
%% formulae. The ``collections'' found in the literature increase in
%% complexity from simple sets for classical logic, to multisets for
%% linear logic, to ordered lists for substructural logics, to complex
%% tree structures for display logics.
%% A sequent rule typically has a rule name, a (finite) number of premises,
%% a side-condition and a conclusion.
%% Rules are read top-down as ``if all the premises hold then the
%% conclusion holds''. A derivation of the judgement $\Gamma \vdash
%% \Delta$ is typically a finite tree of judgements with root $\Gamma
%% \vdash \Delta$ where parents are obtained from children by ``applying
%% a rule''. We use ``derivation'' to refer to a
%% proof \emph{within} a calculus, reserving ``proof'' for a
%% meta-theoretic proof of a theorem \emph{about} the calculus.
%
%\subsection{Formulae and Subformulae}\label{subsec:formulae}
%
%We define a language of formulae.
The language of formulae for BiILL is defined using the grammar below
where $p$ denotes a propositional variable:
$$
A ::= p \mid I \mid \bot \mid A\otimes A \mid A\parr A \mid A\limp A \mid A\excl A
$$
A FILL formula is just a $\biill$ formula
without any occurrences of $\excl.$
$\biill$ formulae are defined formally in Isabelle as follows. We let the type variable
\texttt{'s} be (Isabelle) strings.
{\small
\begin{verbatim}
datatype 's pformula =
Btimes pformula pformula ("_ &&& _" [68,68] 67)
| Bplus pformula pformula ("_ +++ _" [66,66] 65)
| Blolli pformula pformula ("_ --o _" [64,64] 63)
| Bexcl pformula pformula ("_ --< _" [64,64] 63)
| Btrue ("T") | Bfalse("F") | FV string | PP string
\end{verbatim}
}
\noindent Here the binary constructors correspond to, respectively,
$\ltens$, $\parr$, $\limp$ and $\excl$, the unary constructors
\texttt{Btrue} and \texttt{Bfalse} encode the units $\tunit$ and $\punit$
respectively, the constructor \texttt{PP} is used to encode propositional
variables, and \texttt{FV} is used to encode ``scheme variables''; we shall
come back to these shortly.
%
We define the immediate (proper) subformula relation, \texttt{ipsubfml}.
% which will not need to be changed when new connectives are added.
{\small
\begin{verbatim}
ipsubfml :: "('a pformula * 'a pformula) set"
inductive "ipsubfml" (* proper immediate subformula relation *)
intrs ips_and1 "(P, P &&& Q) : ipsubfml" (etc)
\end{verbatim}
}
%\subsection{Structures, Sequents and Rules}\label{subsec:structures}
%% Sequents in display calculus are more general than the traditional notion
%% of sequents in Gentzen's system, where the only structural connective allowed
%% is the `comma'.
A $\biill$-sequent is a pair $X_a\turn X_s$ of an {\em antecedent}
and a {\em succedent} structure, defined respectively as follows:
$$
X_a ::= A \mid \Phi \mid X_a,X_a \mid X_aX_s
$$
where $\Phi$ is a structural constant. A $\fill$-sequent is a $\biill$-sequent containing no
occurrence of $<$ or $\excl$.
The relation between formulae and structures will
be made precise in the next section.
Structures are
%of our calculus $\biilldc$ are
represented by the datatype below:
{\small
\begin{verbatim}
datatype 's pstructr = Comma ('s pstructr) ('s pstructr)
| Gt ('s pstructr) ('s pstructr) | Lt ('s pstructr) ('s pstructr)
| Phi | Structform ('s pformula) | SV 's
\end{verbatim}
}
\noindent where \texttt{Comma}, \texttt{Gt}, \texttt{Lt} and \texttt{Phi} correspond
to the structural connectives `,', $>$, $<$ and $\Phi$.
The operator \texttt{Structform} casts a formula into
a structure. %, since a formula is a special case of a structure.
% (as in the premises of the cut rule given above).
The constructor \texttt{SV}
represents scheme variables for structures.
%% structure variables which appear in the statement of a rule
%% or theorem, and which are instantiated to actual structures of the calculus
%% when constructing derivations.
Since we must reason about arbitrary
derivations, we have to allow derivations to contain structure
variables and reason about their instantiations.
%% We therefore cannot use Isabelle's built-in unification facility for
%% instantiating its scheme variables as explained in more detail in
%% \cite{Dawson01}.
We do not encode explicitly the notion of antecedent/succeedent
structures in the data type; these notions are enforced via
separate predicates when needed (see e.g.
\S\ref{sec:eqdlshallow}).
%% Likewise, formulae of the calculus
%% are represented by a datatype which include a constructor \texttt{FV}
%% for formula variables which can be instantiated to actual formulae of
%% the calculus, and a constructor \texttt{PP} for a primitive proposition
%% variable $p$.
%% The notation in parentheses in the definition of datatype
%% \texttt{pformula}
%% %Figure~\ref{fig:isabelle-formulae}
%% describe an alternative infix syntax, closer to the actual
%% syntax of the calculus. Some complex manipulation of the syntax, available
%% through Isabelle's ``parse translations'' and ``print translations'',
%% allows structure variables and constants to be prefixed by the symbol
%% \texttt{\$}, and the notations \texttt{FV}, \texttt{SV} and
%% \texttt{Structform} to be omitted. For technical reasons related to
%% this, a different method is used to specify the alternative infix
%% syntax for structures and sequents: details omitted.
Sequents and rules of the calculus are represented by
%the Isabelle/HOL datatypes:
{\small
\begin{verbatim}
datatype 'a sequent = Sequent 'a 'a
types 'a psc = "'a list * 'a" (* single step inference *)
types 'a rule = 'a sequent psc
\end{verbatim}
}
\noindent The premises of a rule are represented using a list of sequents while
the conclusion is a single sequent. Thus \texttt{(prems, concl)}
means a rule with premises \texttt{prems} and conclusion \texttt{concl}.
We write \texttt{\$X |- \$Y} to denote \texttt{(Sequent X Y)}.
% can also be represented as
%% Thus \texttt{(\$"X" |- "A")} is equivalent
%% to the term \texttt{Sequent (SV "X") (Structform (FV "A"))}.
%% % is printed, and may be entered, as
% This doesn't seem to be used anywhere.
%% Functions \texttt{premsRule} and
%% \texttt{conclRule} return the premise list and the conclusion of a
%% rule respectively.
%% A structure expression is \emph{formula-free} if it
%% does not contain any formula as a sub-structure: that is, if it does
%% not contain any occurrence of the operator \texttt{Structform}. A
%% formula-free sequent is defined similarly.
% The constant \texttt{rls}
% represents the set of rules of \dRA, encoded using the datatypes just
% described: we omit the details of this code.
% Our definition of nested sequents is very similar, except that we do not have
% separate datatypes corresponding to sequents and structures.
% Rather we have a single datatype
% \begin{verbatim}
% datatype 's pnested = NComma ('s pnested) ('s pnested)
% | Nseq ('s pnested) ('s pnested)
% | NPhi
% | NStructform ('s pformula)
% | NSV 's
% \end{verbatim}
% The pretty-printing/parsing (\texttt{\$} for a nested sequent, its absence for
% a formula, omission of ``\texttt{NStructform}'' and ``\texttt{NSV}'') is
% similar to that for display logic.
%% Note that our formalisation defines variant sets of rules
%% both including and excluding the cut rule shown below.
%% \[
%% \AxiomC{$\Gamma \vdash A, \Delta$}
%% \AxiomC{$\Gamma, A \vdash \Delta$}
%% \LeftLabel{(cut)}
%% \BinaryInfC{$\Gamma \vdash \Delta$}
%% \DisplayProof
%% \]
%% Thus our cut-admissibility result will be of the form:
%% if $\Gamma \vdash A, \Delta$ is (cut-free) derivable
%% and $\Gamma, A \vdash \Delta$ is (cut-free) derivable
%% then $\Gamma \vdash \Delta$ is (cut-free) derivable.
%% In previous work~\cite{dawson-gore-embedding-comparing}, we describe
%% our initial attempts to formalise display calculi in various logical
%% frameworks and describe why we selected Isabelle/HOL. When we model a
%% derivation tree, explicitly, we do so using the capability in HOL of
%% defining types like the datatypes of SML, see \S\ref{s-dse}.
%% %Here we return to simpler sequents and seek generality.
%% In~\cite{dawson-gore-cut-admissibility}, we modelled a derivation tree
%% in HOL as a recursive structure which consists of a
%% root sequent (which should be the conclusion of some rule), and an
%% associated list of (sub)trees (each of which should derive a premise of
%% that rule). The type of explicit derivation trees is a recursive
%% datatype, such as:
%% \begin{verbatim}
%% datatype 'a dertree = Der 'a ('a dertree list)
%% | Unf 'a (* unfinished leaf which remains unproved *)
%% \end{verbatim}
%% %
%% We then had to define a predicate on such a tree, saying whether it
%% was in fact correctly based on the given rules, and so represented a
%% valid derivation.
%% %
%% We modelled a sequent rule as an object in HOL consisting of a list of
%% premises and a conclusion, each of which was a sequent in the language
%% of the logic. Notably, our language of formulae
%% included ``variables'' which could be instantiated with formulae,
%% so we defined functions for such substitutions.
%% %
%% Thus it is more accurate to say in
%% ~\cite{dawson-gore-cut-admissibility}, we used a deep embedding for
%% \emph{derivations}, \emph{rules} and \emph{variables}, since we
%% modelled each of these features of the proof-theory explicitly rather
%% than identifying them with the same features of Isabelle.
%% In alternative approaches to work of this type, the set of derivable
%% sequents can be modelled as an inductively defined set \texttt{ders}
%% (say),
%% % (as we describe in \S\ref{s-dp}).
%% where the derivation tree does not exist, but it ``happens'' in the
%% course of proving that a specific sequent is derivable. That is,
%% derivability in the sequent calculus studied equates to derivability
%% in Isabelle, giving a shallow embedding of {\em derivations}.
%% In such alternative approaches, the rules of the sequent calculus can
%% either be encoded explicitly
%% %(as assumed in the treatment in \S\ref{s-dp}),
%% or they can be encoded in the clauses for the inductive definition of
%% \texttt{ders}. In the latter case, the rules of the
%% sequent calculus under study are encoded as theorems of Isabelle.
%% Thus, even with a shallow embedding of derivations, we have a choice
%% of either a deep or a shallow embedding of {\em rules}:
%% %where \textit{ders} means the set of derivable sequents:
%% % \begin{gather}
%% % (\{P, Q\}, {P \land Q}) \in \mathit{rules} \tag{deep}
%% % \qquad
%% % \frac{ (ps, c) \in \mathit{rules} \quad ps \subseteq \mathtt{ders}}
%% % { c \in \mathtt{ders}}
%% % \\[1ex]
%% % \frac {P \in \mathtt{ders} \qquad Q \in \mathtt{ders}}
%% % {P \land Q \in \mathtt{ders}} \tag{shallow}
%% % \end{gather}
%% %
%% \begin{description}
%% \item[\rm Deep Rules and Shallow Derivation:] \ \\[0.5em]
%% \begin{tabular}[c]{l}
%% $\mathtt{(\{\Gamma \vdash P, ~~\Gamma \vdash Q\},
%% \;\; \Gamma \vdash P \land Q) \in rules}$
%% \\[0.5em]
%% $\mathtt{ [|~(ps, c) \in rules ~;~ ps \subseteq \mathtt{ders}~|]
%% ==> c \in \mathtt{ders}}$
%% \\[0.5em]
%% \end{tabular}
%% \item[\rm Shallow Rules and Shallow Derivations:] \ \\[0.5em]
%% \begin{tabular}[c]{l}
%% $\mathtt{[|~\Gamma \vdash P \in \mathtt{ders} ~;~
%% \Gamma \vdash Q \in \mathtt{ders}~|]
%% ==> \Gamma \vdash P \land Q \in \mathtt{ders}}$.
%% \end{tabular}
%% \end{description}
%% Finally, compared to \cite{dawson-gore-cut-admissibility}, it is much
%% more common to let the variables in a rule be the variables of the
%% theorem prover, and for the theorem prover to do the substitution. In
%% general, however, a deep embedding of one feature can be combined with
%% a shallow embedding of another.
%% Our experience is that shallow embeddings generally permit easier
%% proofs, but sometimes they are inadequate to express a desired
%% concept. For example, with a deep embedding of rules it is easy to
%% express that one set of rules is a subset of another set. With a deep
%% embedding of derivation trees it is easy to express that one property
%% of derivation trees is the conjunction of two other properties, or
%% that a derivation tree has a particular height, whereas to express
%% such things using \derl, \derrec, etc (see \S\ref{s-dp}), one would
%% have to redefine these predicates incorporating the particular
%% properties of interest. Indeed, in this work \cite{our-GLR-paper} we
%% discuss how we found a shallow embedding of derivability inadequate.
%% We have developed the code on which
%% \cite{dawson-gore-cut-admissibility} was based to reflect the fact
%% that Belnap's original proof applied generally to display calculi
%% satisfying certain conditions. Some of these conditions required a
%% deep embedding of variables (and, therefore, of the rules), for
%% example, that no structure variable appears twice in the conclusion of
%% the statement of a rule. For others, a shallow embedding of variables
%% was adequate, since the condition applied equally to the statement of
%% the rule and to all its substitution instances, for example that a
%% premise of a rule contains no variable not contained in the
%% conclusion.
%% \subsection{Our General Derivability Predicates} \label{s-dp}
We now briefly describe the functions we used to encode
derivability. A fuller account is given in \cite{DBLP:conf/lpar/DawsonG10}.
This framework is general in that a rule merely consists of ``premises''
and a ``conclusion'', and is independent of whether the things derived
are formulae or sequents, but we will refer to them
as formulae.
{\small
\begin{verbatim}
consts derl, adm :: "'a psc set => 'a psc set"
derrec :: "'a psc set => 'a set => 'a set"
dersl :: "'a psc set => ('a list * 'a list) set"
dersrec :: "'a psc set => 'a set => 'a list set"
\end{verbatim}
}
% dersl :: "'a psc set => ('a list * 'a list) set"
% dercsl :: "'a psc set => ('a list list * 'a list) set"
% dersrec :: "'a psc set => 'a set => 'a list set"
An inference rule \texttt{(ps, c) : 'a psc} is a list of premises \texttt{ps}
and a conclusion \texttt{c}. Then, \texttt{derl rls} is the set of
rules derivable from the rule set \texttt{rls}, and \texttt{derrec rls
prems} is the set of formulae derivable using rules \texttt{rls}
from the set \texttt{prems} of premises.
These were defined as inductive sets,
% using also the functions \texttt{dersl} and \texttt{dersrec}.
using auxiliary functions \texttt{dersl} and \texttt{dersrec},
which concern the derivability of all members of a list.
So to say $\mathtt{(ps, c) \in \derl\ \rls}$ reflects the
shape of a derivation tree: \texttt{ps} is a list of exactly the
premises used, in the correct order, whereas $\mathtt{c \in \derrec\
\rls\ prems}$ holds even for any set of premises \texttt{prems}
containing those required.
% The auxiliary function \texttt{dersrec} represents several formulae,
% all derivable from the premises. The auxiliary function
% \texttt{dersl} represents several derivation trees side by side;
% $\mathtt{(ps, cs) \in dersl~rls}$ when \texttt{ps} is the
% concatenation of their lists of premises, and \texttt{cs} is the list
% of their conclusions. The function \texttt{dercsl} is similar, but it
% shows which premises are part of which tree.
% That is, $\mathtt{(pss, cs) \in \texttt{dercsl}\ rls}$
% implies $\mathtt{(concat\ pss, cs) \in \texttt{dersl}\ rls}$.
% Some proofs about \derl\ are easier using
% \texttt{dercsl} rather than \texttt{dersl} as the auxiliary function.
%% The key clauses for these functions are shown below:
%% \begin{verbatim}
%% dtderI : "[| (ps, concl) : pscrel ; (pss, ps) : dersl pscrel |]
%% ==> (pss, concl) : derl pscrel"
%% derI : "[| (ps, concl) : pscrel ; ps : dersrec pscrel prems |]
%% ==> concl : derrec pscrel prems"
%% \end{verbatim}
%% We obtained the expected results linking \texttt{derl} and \texttt{derrec},
%% and a number of results expressing transitivity of derivation and the
%% results of derivation using derived rules, for example:
%% \begin{verbatim}
%% derl_trans : "[| (?ps, ?c) : derl ?rls; (?x, ?ps) : dersl ?rls |]
%% ==> (?x, ?c) : derl ?rls"
%% derl_deriv_eq : "derl (derl ?rls) = derl ?rls"
%% derrec_trans_eq : "derrec ?rls (derrec ?rls ?prems) = derrec ?rls ?prems"
%% \end{verbatim}
% We show the equivalence of the display calculus systems including
% cut to the categorical semantics, and the equivalence of the
% display calculus systems without cut to the deep nested sequent calculus.
Since we use cut-admissibility for Display Calculi, and also
some rules of $\biillsn$ are \emph{admissible} (not \emph{derivable}) in
$\biilldn$ (see Theorem~\ref{thm:eqshallowdeep}), we
we need to formalise the notion that a rule of one system is
\emph{admissible} in another system:
$(ps, c)$ is admissible iff: if all premises in $ps$
are derivable, then $c$ is derivable:\\
$$(ps, c) \in \adm\ \rls \iff
(set\ ps \subseteq \derrec\ \rls \ \ \Rightarrow \ \ c \in \derrec\ \rls)$$
%% We obtained the following four results, which were surprisingly tricky
%% since \adm\ is not monotonic:
%% \begin{verbatim}
%% "derl ?rls <= adm ?rls" "adm (adm ?rls) = adm ?rls"
%% "adm (derl ?rls) = adm ?rls" "derl (adm ?rls) = adm ?rls"
%% \end{verbatim}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: