\section{Display Logic} \label{dl}

\subsection{Introduction}

A number of different logical systems can be formulated using the
method, or style, of Display Logic \cite{Bel}.
These include several normal modal logics \cite{Wansing},
and intuitionistic logic \cite{ILR}.
Display Logic resembles the Gentzen sequent calculus \textbf{LK},
but with significant differences.
For example, the rule for introducing the connective `$\lor$' 
(on the left) in \textbf{LK} and its counterpart in Display Logic are
\begin{equation} \label{v|-1}
 \frac {\Gamma, A \vdash \Delta \quad \Gamma, B \vdash \Delta }
  {\Gamma, A \lor B \vdash \Delta } (\mbox{\textbf{LK}-}\lor \vdash )
\qquad %\textrm{ and }
\qquad 
 \frac {A \vdash Z \quad B \vdash Z }
  {A \lor B \vdash Z } (\mbox{DL-}\lor \vdash )
\end{equation}
Whereas, in \textbf{LK},
$\Gamma$ and $\Delta$ denote comma-separated lists of formulae,
in Display Logic, $Z$ denotes a Display Logic \emph{structure}.
A {structure} is defined as a formula, %or a structure variable,
or a combination of structures formed using the \emph{structural operators}
(one of which is `,').
%Conventionally we use $X,Y,Z,W,\ldots$ as variables denoting structures.
%which can involve several \emph{structural} operators (one of which is `,').
Informally, \emph{formulae} and \emph{formula} (or \emph{logical})
\emph{operators} are the 
formulae and operators of the logic being displayed, 
whereas the structural operators are additional operators used in
presenting that logic as a display logic. 
(See \cite{dRA} or \cite{thesis}
for a full explanation of \emph{structures} and \emph{formulae}).
In Display Logic, unlike in \textbf{LK},
the introduced formula (here, $A \lor B$) stands by itself
on one side of the turnstile;
this is generally the case with 
Display Logic rules.
%the ``logical introduction rules''
%(ie, the rules which introduce the logical operators,
%eg DL-$\vdash \lor$ above).
However there are also rules (the ``display postulates'')% described below)
which effectively allow moving substructures from one side to the other.
All display postulates are bi-directional (invertible) rules.

In Display Logic,
in terms of backwards proof, the ``logical introduction rules''
eliminate the logical (formula) operators and replace them with corresponding
structural operators.
For example, rules for introducing the $\lor$ operator are shown.
Note that the ($\lor \vdash $) rule shown below is different from the one
above; in some Display Logics they both hold.
\begin{equation} \label{v|-2}
\mbox{\slrule {A \vdash X \quad B \vdash Y }
{A \lor B \vdash X,Y } ($\lor \vdash $)} \qquad\qquad
\mbox{\slrule {Z \vdash A,B } {Z \vdash A \lor B } ($\vdash \lor $)}
\end{equation}

A display logic will also have some ``basic structural rules'',
which are expressed in terms of structural connectives only, and
which capture properties of the logic and its logical operators.
For example, the following rules express the associativity of 
$\land$ and $\lor$
(the double line means the rule is bi-directional).
$$
\mbox{\invrule {X,(Y,Z) \vdash W} {(X,Y),Z \vdash W} ($A \vdash$)} \qquad\qquad
\mbox{\invrule {W \vdash X,(Y,Z) } {W \vdash (X,Y),Z } ($\vdash A$)}
$$

As an alternative to writing a rule with one premise $\mathcal P$ and a
conclusion $\mathcal C$ separated by a horizontal line, we often write 
$\mathcal P \Longrightarrow \mathcal C$, and 
for a bi-directional rule we often write 
$\mathcal P \Longleftrightarrow \mathcal C$.
For a full explanation of Display Logic see, for example, \cite{dRA}.

By way of example,
the Display Logic formulation of classical propositional logic has
structural operators `,' `$*$' `$I$' .
As in \textbf{LK}, `,' is used to stand for either `$\land$' or `$\lor$';
which one it is
depends not only on which side of the `$\vdash$' the `,' appears, 
but also on the number of `*' operators in whose scope the `,' lies. 
This reflects the duality between `$\land$' and `$\lor$',
as expressed by DeMorgan's laws.
Each structural operator stands for one, or two (depending on the position),
formula operators.
Thus `$I$' stands for truth or falsity, 
`$*$' for Boolean negation and `$,$' for `$\land$' or `$\lor$'.
The logical identity
$A \land B \Rightarrow C \iff A \Rightarrow C \lor \lnot B$
(which is an example of ``residuation'', explained below)
becomes an instance of the display postulate 
$ \displaystyle X,Y \vdash Z \iff X \vdash Z, *Y$
and 
$ \lnot A \Rightarrow B \iff \lnot B \Rightarrow A$
becomes an instance of 
$ \displaystyle  * X \vdash Y \iff * Y \vdash X$.

\comment{
The logical identities
$$A \land B \Rightarrow C \iff A \Rightarrow C \lor \lnot B
\qquad \qquad 
 \lnot A \Rightarrow B \iff \lnot B \Rightarrow A$$
become the display postulates
$$ \displaystyle A,B \vdash C \iff A \vdash C, *B
\qquad \qquad 
 \displaystyle  * A \vdash B \iff * B \vdash A$$
These are examples of ``residuation''.
}

\subsection{Residuation} \label{DL-resid}

As noted in \S\ref{intl}, 
Display Logic does not have equalities or inverses;
the fact that any chosen substructure can be displayed
depends on the notion of \emph{residuation}.

Consider a partially ordered set, with binary functions $s$, $f$ and $g$.
To say that $f$ and $g$ are \emph{residuals} of $s$ means
that the following hold (for all $a$, $b$ and $c$)
$$s(a,b) \leq c \iff a \leq f(c,b)$$
$$s(a,b) \leq c \iff b \leq g(a,c)$$
(see \cite{Dunn}, \S6, or \cite{sdpr})
These equivalences have the effect of ``displaying'' $a$ and $b$ respectively.
When all the connectives used in a proposition have residuals, 
any subterm can be displayed.
If we then have a rule which partly instantiates to 
$a \leq X \Longrightarrow a' \leq X$,
we can form a proof as follows.
\begin{center}
\vpf
\bpf
\A "$s(a,b) \leq c$"
\U "$a \leq f(c,b)$"
\U "$a' \leq f(c,b)$"
\U "$s(a',b) \leq c$"
\epf
\end{center}
We have in effect rewritten the subterm $a$ (located in an arbitrary position)
to $a'$.
This is the manner in which we rewrite arbitrarily chosen substructures
in Display Logic.

Note that for the proof above, we required  
only $a \leq X \Longrightarrow a' \leq X$,
not $a \leq X \Longleftrightarrow a' \leq X$.
That is, $a'$ may be a strictly stronger proposition than $a$.
Effectively, doing subterm rewrites this way also allows a subterm to be
replaced by one that is logically either
stronger or weaker, according to the subterm's position.

\subsection{Rewriting} \label{DL-rewr}

It will be noted that among the examples above, 
both the basic structural rules ($A \vdash$)
and ($\vdash A$), and the logical introduction rule ($\vdash \lor$)
have on one side a single structural variable 
(which can stand for any structure,
including any formula) which remains unchanged;
the expression being ``rewritten'' appears on the other side.
This is typical of many rules.
In some other cases, rules of this form can be derived.
For example, if the rule for ($\lor \vdash $) given in the logic
is that shown at (\ref{v|-2}),
it may be possible to derive the version given at (\ref{v|-1}).

The following example shows this rule being used.
The first (bottom) step is to display the disjunction $A \lor C$
(``dp'' denotes ``display postulate(s)'');
then the ($\lor \vdash $) rule is applied (which splits the branch of the
proof tree).
Finally, the display postulate(s) which were used to display $A \lor C$
are reversed (in both branches).
This last step relies on the fact that the ($\lor \vdash $) rule 
leaves the term on the right of the `$\vdash$' unchanged.
Notice that the required display postulates move $A \lor C$
to the left, so the introduction rule needed is that for 
introducing $\lor$ on the \emph{left}.

\vpf
\begin{center}
\bpf
\A "$D \vdash * A, B$"
\U "$A \vdash * (D, * B)$" "(dp)"
\A "$D \vdash * C, B$"
\U "$C \vdash * (D, * B)$" "(dp)"
\B [2em] "$A \lor C \vdash * (D, * B)$" "($\lor \vdash $)"
\U "$D \vdash * (A \lor C), B$" "(dp)"
\epf
\end{center}

An example of several steps of this form follows.
The rules used are %(from bottom up)
the logical introduction rules 
($\vdash \to $), ($\to \vdash $), ($\land \vdash $) and ($\lnot \vdash $),
distribution of `$*$' over `,' (ie, DeMorgan's law),
and double negation elimination.
\vpf
\begin{center}
\bpf
\A "$* C \vdash * C, A, B$"
\U "$* C \vdash * C, * * A, B$" "($\vdash **$)"
\U "$* C \vdash * C, * \lnot A, B$" "($\lnot \vdash $)"
\U "$* C \vdash * (\lnot A, C), B$" "($\vdash$*-,-dist)"
\U "$* C \vdash * (\lnot A \land C), B$" "($\land \vdash $)"

\A "$A \vdash * C, A, B$"
\U "$A \vdash * C, * * A, B$" "($\vdash **$)"
\U "$A \vdash * C, * \lnot A, B$" "($\lnot \vdash $)"
\U "$A \vdash * (\lnot A, C), B$" "($\vdash$*-,-dist)"
\U "$A \vdash * (\lnot A \land C), B$" "($\land \vdash $)"
\B [2em] "$C \to A \vdash * (\lnot A \land C), B$" "($\to \vdash $)"
\U "$C \to A \vdash \lnot A \land C \to B$" "($\vdash \to $)"

\epf
\end{center}

The tactics can be programmed to perform the above steps one at a time,
or all in one step; observe that if a proof rule splits a branch of the proof
tree, the search-and-rewrite process continues on each branch independently. 
We now describe how this is implemented in Isabelle.

\subsection{Implementation in Isabelle} \label{DL-impl}

The implementation of Display Logic in Isabelle is described
generally in \cite{thesis},
and the implementation of the rewriting procedure is described in Appendix 
\ref{app:DL-impl}.