
\section{Dynamic Topological Logic: the system S4C} \label{s-s4c}

This section describes Isabelle proofs of the
cut admissibility of the logic S4C described in \cite{mints-jaegerfest}

This system has two ``modal'' operators, $\Box$ and $\circ$.
The $S4$-axioms hold for $\Box$, $\circ$ commutes with the boolean operators,
and the following are given:
\begin{align*}
\circ (A \to B) & \leftrightarrow (\circ A \to \circ B) \\
\circ \bot & \leftrightarrow \bot \\
\circ \Box A & \to \Box \circ A
\end{align*}

The following sequent rules are given for S4C
$$
\frac{\circ^k A, \Gamma \vdash \Delta, \circ^k B}
  {\Gamma \vdash \Delta, \circ^k (A \to B)}(\vdash\to)
\qquad
\frac{\Gamma \vdash \Delta, \circ^k A \quad \circ^k B, \Gamma \vdash \Delta}
  {\circ^k (A \to B), \Gamma \vdash \Delta}(\to\vdash)
$$
$$
\frac{\circ^k A, \Gamma \vdash \Delta}
  {\circ^k \Box A, \Gamma \vdash \Delta}(\Box\vdash)
\qquad
\frac{\Gamma \vdash \Delta}
  {\circ \Gamma \vdash \circ \Delta}(\circ)
\qquad
\frac{\mathcal B \vdash A}{\mathcal B \vdash \Box A}(\vdash\Box)
$$

In the $(\vdash\Box)$ rule, $\mathcal B$ must consist of 
``$\Box$-formulae'', that is, formulae of the form $\circ^k \Box A$.

As this presentation omits the other logical operators, 
we include, for them, the usual logical introduction rules
with the principal and side formulae preceded by $\circ^k$ just 
as with the $(\vdash\to)$ and $(\to\vdash)$ rules shown above.

The property we will prove inductively is mix (rather than cut) admissibility.
In fact the presence of the $\circ$ rule adds to the complexity of the proof
and is dealt with in a rather similarly to how we dealt with contraction in
proving cut admissibility for GTD.

We now describe how we formalised the system.
First we define the rules which can be extended by an arbitrary context.
Without the context, these rules form the set \texttt{s4cnne}.

Applying \texttt{nkmap} $k$ to a rule applies $\circ^k$ to each formula
appearing in that rule.

\begin{verbatim}
inductive "s4cnne"
  intros
    id : "psc : idrls ==> psc : s4cnne"
    wk : "psc : wkrls ==> psc : s4cnne"
    ctr : "psc : ctrrls A ==> psc : s4cnne"
    circ_il : "rl : lksil ==> nkmap k rl : s4cnne"
    circ_ir : "rl : lksir ==> nkmap k rl : s4cnne"
    circ_T : "rl : Tsnc ==> nkmap k rl : s4cnne"

inductive "Tsnc" (* simpler T rule with no context *)
  intros
    I : "([{#A#} |- {#}], {#Box A#} |- {#}) : Tsnc"

defs
  nkmap_def : "nkmap k == pscmap (seqmap (funpow Circ k))"

inductive "s4cn"
  intros
    extI : "rl : s4cnne ==> pscmap (extend (U |- V)) rl : s4cn"
    circI : "([seq], seqmap Circ seq) : s4cn"
    boxI : "M : msboxfmls ==> ([M |- {#A#}], M |- {#Box A#}) : s4cn"

inductive "boxfmls"
  intros
    I : "funpow Circ k (Box B) : boxfmls"

inductive "msboxfmls"
  intros
    I : "ALL f. f :# M --> f : boxfmls ==> M : msboxfmls"
\end{verbatim}

To prove mix admissibility, the basic method is to look for the last rule
application on each side of a rule other than the $\circ$ rule.
This resembles the proof described in \S\ref{s-cut-gtd}, where we looked for
the last rule on each side which is not contraction on the cut-formula.
For this we use the theorem \texttt{top\_circ}.
We also need the fact that in some cases we need the fact that if the bottom
rule is not $\circ$, then the tree asserted to exist is actually the original
one.
The function \texttt{forget} exists simply to prevent automatic case splitting
of its argument: logically it does nothing.

\begin{verbatim}
top_circ: "valid ?rls ?dt ==> EX dtn k.
   botRule dtn ~: circrules & valid ?rls dtn &
   conclDT ?dt = seqmap (funpow Circ k) (conclDT dtn) &
   heightDT ?dt = heightDT dtn + k &
   forget ((k = 0) = 
     (botRule ?dt ~: circrules) & (k = 0) = (dtn = ?dt))"

forget_def: "forget ?f == ?f"
\end{verbatim}

But one easy case is where the last rule on \emph{both} sides is the $\circ$
rule: then we can apply mix (on a smaller formula) to the premises of the
$\circ$ rules, and then apply the $\circ$ rule.
So when we look at the $\circ$ rules on both sides immediately preceding the
mix, we need only bother about the case where the number of those $\circ$ rules
is zero on one side.

First, the case where both rules are the $(\vdash\Box)$ rule.
Then there must be zero $\circ$ rules on the right side (because if there are 
zero $\circ$ rules on the left, then the cut-formula must be $\Box A$, whence
there would also be zero $\circ$ rules on the right.

\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\AxiomC{$\circ^k \Box A, \M' \vdash B$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\circ^k \Box A, \M' \vdash \Box B$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$\circ^k \M, \M' \vdash \Box B$}
\end{prooftree}
\end{center}

Here we do the mix, by induction, before the $(\vdash\Box)$ rule on the right, 
then we apply the $(\vdash\Box)$ rule.

\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{$(\circ^*)$}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\AxiomC{$\circ^k \Box A, \M' \vdash B$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k \M, \M' \vdash B$}
\RightLabel{$(\vdash\Box)$}
\UnaryInfC{$\circ^k \M, \M' \vdash \Box B$}
\end{prooftree}
\end{center}

For the other cases, we first consider the ``parametric'' cases,
where the last rule above the $\circ$ rules is an extension $\rho'$
of a rule $\rho$ in \texttt{s4cnne},
and the principal formula of $\rho$ is not the ``de-circled'' cut-formula $A$.

\begin{center}
\begin{prooftree}
\AxiomC{$X' \vdash Y', A^n$}
\RightLabel{($\rho'$)}
\UnaryInfC{$X \vdash Y, A^n$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^k Y, \circ^k A^n$}
\AxiomC{$\circ^k A^m, U \vdash V$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$\circ^k X, U \vdash \circ^k Y, V$}
\end{prooftree}
\end{center}

Here we must apply the $\circ$ rule the requisite number of times 
to the premise(s) of $\rho'$,
then apply (using the inductive hypothesis) mix on $\circ^k A$ to each of
them, and finally apply $\rho''$ which we get by applying
$\circ^k$ to $\rho$, and then extending it appropriately.

This uses the result that if a rule is in \texttt{s4cnne}
then so is the result of applying $\circ^k$ to all formulae in its premises and
conclusion.

\begin{verbatim}
s4cnne_nkmap: "?r : s4cnne ==> nkmap ?k ?r : s4cnne"
\end{verbatim}

\begin{center}
\begin{prooftree}
\AxiomC{$X' \vdash Y', A^n$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X' \vdash \circ^k Y', \circ^k A^n$}
\AxiomC{$\circ^k A^m, U \vdash V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k X', U \vdash \circ^k Y', V$}
\RightLabel{($\rho''$)}
\UnaryInfC{$\circ^k X, U \vdash \circ^k Y, V$}
\end{prooftree}
\end{center}

Next we consider the cases of weakening or contraction on the 
``de-circled'' cut-formula.

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash Y, A^{n'}$}
\RightLabel{(\textit{wk/ctr})}
\UnaryInfC{$X \vdash Y, A^n$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^k Y, \circ^k A^n$}
\AxiomC{$\circ^k A^m, U \vdash V$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$\circ^k X, U \vdash \circ^k Y, V$}
\end{prooftree}
\end{center}

Here we must apply the $\circ$ rule the requisite number of times 
to the premise of the weakening or contraction, and then
apply (using the inductive hypothesis) mix on $\circ^k A$ to each of them.

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash Y, A^{n'}$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^k Y, \circ^k A^{n'}$}
\AxiomC{$\circ^k A^m, U \vdash V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k X, U \vdash \circ^k Y, V$}
\end{prooftree}
\end{center}

It is similar for the parametric, weakening or contraction cases on the right.
The axiom rule is trivial in all cases.

For the $(\vdash \Box)$ rule on the left, where the rule on the right 
is an extension of rule $\rho$ whose principal formula is the ``de-circled''
cut-formula, the only case remaining is where $\rho$ is $(\Box \vdash)$.

\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{$(\vdash \Box)$}
\UnaryInfC{$\M \vdash \Box A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\AxiomC{$\circ^{k''} A, U \vdash V$}
\RightLabel{$(\Box \vdash)$}
\UnaryInfC{$\circ^{k''} \Box A, U \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^{k' + k''} \Box A, \circ^{k'} U \vdash \circ^{k'} V$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$\circ^k \M, \circ^{k'} U' \vdash \circ^{k'} V$}
\end{prooftree}
\end{center}

Here $k' + k'' = k$, but since we also have that $k = 0$ or $k' = 0$,
this means that $k' = 0$ and $k'' = k$.
Here is is more complicated than it would be for a single mix, 
since we have to perform inductive mixes on formulae first with, then without,
$\Box$: here $U$ may contain further occurrences of $\circ^k \Box A$,
and $U'$ represents $U$ with these deleted.

\begin{center}
\begin{prooftree}
\AxiomC{$\M \vdash A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k \M \vdash \circ^k A$}
\AxiomC{$\M \vdash \Box A$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k \M \vdash \circ^k \Box A$}
\AxiomC{$\circ^k A, U \vdash V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k \M, \circ^k A, U' \vdash V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k \M, \circ^k \M, U' \vdash V$}
\RightLabel{(\textit{ctr})}
\UnaryInfC{$\circ^k \M, U' \vdash V$}
\end{prooftree}
\end{center}

Next we look at the case of the $(\vdash \Box)$ rule on the right,
but for this, since the cut-formula must be a $\Box$-formula,
all cases have already been dealt with.

Finally, there is the case where the last rules (above the final sequence of
$\circ$-rules) on both sides are extensions of rules in \texttt{s4cnne}. 
Most of these cases have been covered, ie,
\begin{itemize}
\item the ``parametric'' cases, where the ``de-circled'' cut-formula 
is not the principal formula of the rule
\item axiom, weakening, and contraction rules
\end{itemize}
So there remain the cases where the rules on either side are the logical
introduction rules.
For these, the proofs are essentially the same as for other logics generally,
except that we need to allow for a number of circles.
Conceptually it is easiest to imagine that in each case the final $\circ$ rules
are moved upwards to precede the final logical introduction rules,
although we didn't actually prove it this way.

We proved that the usual logical introduction rules,
with $\circ^k$ applied to principal and side formulae (as used in S4C),
satisfy the property \texttt{c8ger\_prop} mentioned in \S\ref{s-induction}.
Recall that this means that assuming (single-)cut admissibility on smaller
formulae, you have cut admissibility of a more complex formula where the last
rule on either side is a logical introduction rule.

\begin{verbatim}
s4cn_c8: "c8ger_prop (circrel ipsubfml) s4cn ?A 
    (nkmap ?k ` (lksil Un lksir))"
\end{verbatim}

The following diagrams show an example.
Again, doing mix-admissibility makes it more complicated because we have to do
inductive applications of mix (for the original cut-formula) as well as
applications of cut on smaller formulae.
We let $t = k + k' = l + l'$, and we let 
$Y'$ be $Y$ with copies of $\circ^{k'}(A \land B)$ deleted, and 
$U'$ be $U$ with copies of $\circ^{l'}(A \land B)$ deleted.
In this case we do not make use of the fact that either $k$ or $l$ must be
zero.

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} A, Y$}
\AxiomC{$X \vdash \circ^{k'} B, Y$}
\RightLabel{($\vdash \land$)}
\BinaryInfC{$X \vdash \circ^{k'} (A \land B), Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t (A \land B), \circ^k Y$}
\AxiomC{$U, \circ^{l'} A, \circ^{l'} B \vdash V$}
\RightLabel{($\land \vdash$)}
\UnaryInfC{$U, \circ^{l'} (A \land B) \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^l U, \circ^t (A \land B) \vdash \circ^l V$}
\RightLabel{(\textit{mix ?})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U' \vdash \circ^k Y', \circ^l V$}
\end{prooftree}
\end{center}

This is replaced by

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} A, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t A, \circ^k Y$}
\AxiomC{$\circ^l U, \circ^t (A \land B) \vdash \circ^l V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U' \vdash \circ^t A, \circ^k Y', \circ^l V$}
\dottedLine
\UnaryInfC{\large (A)}
\end{prooftree}
\end{center}

\begin{center}
\begin{prooftree}
\AxiomC{$X \vdash \circ^{k'} B, Y$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^k X \vdash \circ^t B, \circ^k Y$}
\AxiomC{$\circ^l U, \circ^t (A \land B) \vdash \circ^l V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U' \vdash \circ^t B, \circ^k Y', \circ^l V$}
\dottedLine
\UnaryInfC{\large (B)}
\end{prooftree}
\end{center}

\begin{center}
\begin{prooftree}
\AxiomC{$\circ^k X \vdash \circ^t (A \land B), \circ^k Y$}
\AxiomC{$U, \circ^{l'} A, \circ^{l'} B \vdash V$}
\RightLabel{($\circ^*$)}
\UnaryInfC{$\circ^l U, \circ^t A, \circ^t B \vdash \circ^l V$}
\RightLabel{(\textit{inductive mix})}
\dottedLine
\BinaryInfC{$\circ^k X, \circ^l U', \circ^t A, \circ^t B \vdash 
  \circ^k Y', \circ^l V$}
\dottedLine
\UnaryInfC{\large (C)}
\end{prooftree}
\end{center}

Then (A), (B) and (C) are combined using inductive cuts on the smaller
cut-formulae $\circ^t A$ and $\circ^t B$, and the necessary contractions, to
derive the required sequent
{$\circ^k X, \circ^l U' \vdash \circ^k Y', \circ^l V$}.

Finally we combine these results to get the mix admissibility result,
in terms of explicit derivation trees, and then in terms of derivability.

\begin{verbatim}
s4cn_masdt: "(?dta, ?dtb) : masdt s4cn ?A" 
s4cn_mas: "(?cl, ?cr) : mas s4cn ?A"
\end{verbatim}

