\documentclass{beamer}

\usepackage{proof}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
%\usepackage{cmll}
%\usepackage{MnSymbol}
\usepackage{graphicx}
\usepackage{bussproofs}
%\usepackage[all]{xy}
\usepackage{comment}
\usepackage{lscape}

%\newcommand{\excl}{\mathrel{\rotatebox[origin=c]{180}{\ensuremath \multimap}}}

%\usepackage{txfonts}
%\usepackage{amsthm}

%\renewcommand{\labelenumi}{(\roman{enumi})}

\newcommand\bimbo{Bimb\'o~}

\newcommand\hide[1]{}

\definecolor{dkblue}{rgb}{0,0,.7}
\definecolor{dkgreen}{rgb}{0,.5,0}
\definecolor{greyout}{rgb}{0.7,0.7,0.7}
%\newcommand\tc[2]{\textcolor{#1}{#2}}
%\newcommand\tcr[1]{\tc{darkred}{#1}}
\newcommand\tcg[1]{\tc{dkgreen}{#1}}
\newcommand\tcb[1]{\tc{dkblue}{#1}}
\newcommand\tcgy[1]{\tc{greyout}{#1}}
\newcommand\Tcr[1]{\tcr{\textbf{#1}}}
\newcommand\Tcg[1]{\tcg{\textbf{#1}}}
\newcommand\Tcb[1]{\tcb{\textbf{#1}}}

\newcommand{\tblue}[1]{\textcolor{blue}{#1}}
\newcommand{\tgreen}[1]{\textcolor{magenta}{#1}}
\newcommand{\tred}[1]{\textcolor{red}{#1}}
\newcommand{\TextRed}{\tred}

\usepackage{color}
\definecolor{darkred}{cmyk}{0.0,1.0,1.0,0.3}
\newcommand\tc[2]{\textcolor{#1}{#2}}
\newcommand\tcr[1]{\tc{darkred}{#1}}

\theoremstyle{plain}
\newtheorem{proposition}[theorem]{Proposition}

\newcommand\MPL{\ensuremath{\mathtt{pl}}}
\newcommand\MPR{\ensuremath{\mathtt{pr}}}
\newcommand\MCL{\ensuremath{\mathtt{cl}}}
\newcommand\MCR{\ensuremath{\mathtt{cr}}} 
\input{rule-defs}

% the logics in the paper 
\newcommand{\limp}{\to}
\newcommand{\verum}{\ensuremath{\mathbf{t}}}

\newcommand{\rarrow}{\ensuremath{R_{\limp}}}
\newcommand{\rarrowt}{\ensuremath{R_{\limp}^{\verum}}}
\newcommand{\tarrow}{\ensuremath{T_{\limp}}}
\newcommand{\tarrowt}{\ensuremath{T_{\limp}^{\verum}}}

\newcommand{\str}{\ensuremath{Str}}
\newcommand{\astr}[2]{#1\{#2\}}

\newcommand{\seq}{\ensuremath{\vdash}}
\newcommand{\myb}[1]{\ensuremath{[#1]}}
\newcommand{\semic}{\ensuremath{\; ; \;}}
\newcommand{\smsc}{\ensuremath{;}}
\newcommand{\tick}{\checkmark}

\newcommand{\strttleft}{(T\ensuremath{_{\verum}\seq\smsc})}
\newcommand{\strbleft}{(B\ensuremath{\seq\smsc})}
\newcommand{\strbpleft}{(B\ensuremath{'\seq\smsc})}
\newcommand{\strwleft}{(W\ensuremath{\seq\smsc})}

\newcommand{\strktleft}{(K\ensuremath{_{\verum}\seq\smsc})}

\newcommand\merge{\bullet}

\newcommand{\lrarrow}{\ensuremath{LR_{\limp}}}
% \newcommand{\lrarrowstr}{\ensuremath{LR_{\limp\semic}}}
\newcommand{\lrarrowc}{\ensuremath{\myb{LR_{\limp}}}}
\newcommand{\lrarrowt}{\ensuremath{LR_{\limp}^{\verum}}}
\newcommand{\lrarrowtstr}{\ensuremath{LR_{\limp\semic}^{\verum}}}
\newcommand{\lrarrowtc}{\ensuremath{\myb{LR_{\limp}^{\verum}}}}

\newcommand{\ltarrow}{\ensuremath{LT_{\limp}}}
\newcommand{\ltarrowt}{\ensuremath{LT_{\limp}^{\verum}}}
% \newcommand{\ltarrowc}{\ensuremath{\myb{LT_{\limp}^{\verum}}}}
\newcommand{\tcirc}{\ensuremath{\bigcirc\!\!\!\!\verum}}
\newcommand{\ltarrowtcirc}{\ensuremath{LT_{\limp}^{\tcirc\;}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Issues in Machine-checking the Decidability of
  Implicational Ticket Entailment}

\author{ {Jeremy Dawson}, {Rajeev Gor\'e} }

\institute[ANU]{Logic and Computation Group\\
  Research School of Computer Science\\
  The Australian National University\\
  \url{jeremy.dawson@anu.edu.au} }

\date{\today} 

\begin{document}

\frame{\titlepage}

\begin{frame} \frametitle{Overview}

  \begin{description}[M]
  \item[Motivation:] Machine checking the decidability proof of BD
  \item[What:] The logics, and their calculi 
  \item[How:] Encoding sequents, consecutions, derivability and derivations in Isabelle (sample!)
  \item[Machine-checked results:] Admissibility results confirmed
  \item[Various Calculi:] Relations between the calculi
  \item[Issues:] The decidability argument
  \end{description}

\end{frame}

\begin{frame}{Axiomatisations of various logics}
  \centering
\begin{tabular}[l]{|l|@{\extracolsep{3pt}}l|l|l|l|l|}
\hline
Name &  Axioms  & \multicolumn{4}{c|}{Logic}
\\
  &  & \tarrow & \tarrowt & \rarrow & \rarrowt
\\ \hline
(A1) & $A \limp A$
     & \tick & \tick & \tick & \tick
\\ \hline
(A2) & $(A \limp B) \limp (C \limp A) \limp (C \limp B)$
     & \tick & \tick & \tick & \tick
\\ \hline
(A3) & $(A \limp B \limp C) \limp (B \limp A \limp C)$
     & & & \tick & \tick
\\ \hline
(A4) & $(A \limp A \limp B) \limp (A \limp B)$
     & \tick & \tick & \tick & \tick
\\ \hline
(A5) & $(A \limp B) \limp (B \limp C) \limp (A \limp C)$
     & \tick & \tick &  &
\\ \hline
Name & Rules of Inference & \multicolumn{4}{c|}{}
\\ \hline
(R1) & from $A \limp B$ and $A$, deduce $B$
     & \tick & \tick & \tick & \tick
\\ \hline
(R2) & $\vdash A \;//\; \vdash \verum \limp A$
     &  & \tick &  & \tick
\\ \hline
\end{tabular}

\end{frame}

\begin{frame}{(Multiset) Sequent Rules and Calculi}
%{$\lrarrow$, $\lrarrowt$, $\lrarrowc$, and $\lrarrowtc$}

\centering
\begin{tabular}[c]{c@{\extracolsep{-0.2cm}}cc}
\idrule  & \impleftrule  &  \imprightrule
\\[1em]
\wleftrule & \tleftrule  & \trightrule
\\[1em]
& \impcleftrule &
\end{tabular} \\[1em]

In the \impcleft\ rule, $\myb{\Gamma_1, A \limp B, \Gamma_2} \seq C$
means \\ ${\Gamma_1, A \limp B, \Gamma_2} \seq C$, then
\emph{some} contraction \\[1em]

\begin{tabular}[l]{|c|c|c|c|c|c|c|c|c|}
\hline
& \;\id\; & \;\impleft\; & \;\impright\; & \;\wleft\;
          & \;\tleft\; & \;\tright\; & \;\impcleft
\\ \hline
% \ltarrow & & & & & & & 
% \\[1pt] \hline
% \ltarrowt & & & & & & &
% \\[1pt] \hline
\lrarrow & \tick & \tick & \tick & \tick & & &
\\[1pt] \hline
\lrarrowt &  \tick & \tick & \tick & \tick & \tick & \tick &
\\[1pt] \hline\hline
\lrarrowc &  \tick & \tick & \tick &  &  &  & \tick
\\[1pt] \hline
\lrarrowtc &  \tick & \tick & \tick &  & \tick & \tick & \tick
\\[1pt] \hline
\end{tabular}

\end{frame}

\hide{
\begin{frame}
Isabelle code equivalences
\begin{tabular}{cc}
\lrarrow & \texttt{LRi} \\
% not used \lrarrowstr & \texttt{LRisc} \\
\lrarrowc & \texttt{LRisb} \\
\lrarrowt & \texttt{LRit} \\
\lrarrowtstr & \texttt{LRitsc} \\
\lrarrowtc & \texttt{LRitsb} \\

\ltarrow & \ltarrowt \\
\ltarrowt & \texttt{LTit} \\
% not used \ltarrowc & \texttt{LT??} \\
\ltarrowtcirc & \texttt{LTitc}

\end{tabular}

\end{frame}
}

\begin{frame}{(Structure) Consecution Rules and Calculi}
%  $\ltarrowt$, $\lrarrowtstr$ $\ltarrowtcirc$

  \begin{tabular}[c]{|l@{\extracolsep{1cm}}l|}
\hline
\\
   \multicolumn{2}{|c|}{\ltarrowt}
\\
    \stridrule  & \strwleftrule
\\[1.5em]
    \strimpleftrule  &  \strimprightrule
% \\[1.5em]
%     \strcutrule &  %\strtrightrule
\\[1.5em]
    \strbleftrule  &  \strbpleftrule
\\[1.5em]
    \strkitleftrule & \strmtleftrule
\\[1.5em] \hline &
\\
%\multicolumn{2}{|c|}{\lrarrowtstr}
%\\
   % \multicolumn{2}{|c|}{
      % \lrarrowtstr \; := \; \ltarrowt \; + \; \strcleft
                % \; = \; \ltarrowt \; + \; \strcileft
   % }
% \\[1.5em]
   % \strcleftrule &    \strcileftrule
% \\[1.5em] \hline &
% \\
%    \multicolumn{2}{|c|}{\ltarrowtcircstr}
% \\
   \multicolumn{2}{|c|}{
       \ltarrowtcirc \; := \;  \ltarrowt \; + \; \strktleft \; + \;
\strttleft
   }
\\[1em]
    \strktleftrule & \strttrightrule
\\[1em]  \hline
  \end{tabular}

\end{frame}

\begin{frame}{Method of \bimbo and Dunn for decidability of \tarrowt}
  \begin{description}[M]
  \item[\lrarrowtc\ ] sequent calculus for \rarrowt, decidable proof-search 
\item[\ltarrowtcirc\ ] a consecution calculusfor \rarrowt, untamed proof-search
\item[\ltarrowt\ $\subset$ \ltarrowtcirc\ ] consecution calculus for
  \tarrowt, untamed proof search
\item[Given $\varphi$:] ~\\
%\ltarrowtcirc\ is \ltarrowt\ plus two more rules

\begin{itemize}
\item look at all derivations of $\varphi$ in \lrarrowtc
\item translate them to derivations in consecution calculus \ltarrowtcirc
\item if any is in \ltarrowt, then theorem of \tarrowt, else non-theorem
\end{itemize}

  \end{description}
\end{frame}

\begin{frame}[fragile]{Derivability in Isabelle}

\begin{description}[M]
\item[Implicit] derivability of items of type \verb!'a! (sequents or consecutions)

\begin{verbatim}
   'a psc  =  "'a list * 'a" (* single inference *)
    derl   :: "'a psc set => 'a psc set"
    derrec :: "'a psc set => 'a set => 'a set"
\end{verbatim}

\item
\item[Neat example theorems:] given set of rules \verb!rls! and leaves \verb!ps!
\begin{verbatim}
  "derrec ?rls (derrec ?rls ?ps) = derrec ?rls ?ps"
  "derl (derl ?rls) = derl ?rls"
  "derrec (derl ?rls) ?ps = derrec ?rls ?ps"
\end{verbatim}

\item
\item[Explicit:] term witnessing a derivation tree over type \verb!'a!
\begin{verbatim}
 datatype 'a dertree = Der 'a ('a dertree list)
                     | Unf 'a (* unproved leaf *)
\end{verbatim}

\item
\item[Theorem:] to and fro between these implicit and explicit concepts
$c \in $ \texttt{derrec rls \{\}}  iff 
$\exists\ dt.$ \texttt{valid} $dt$ \& \texttt{conclDT} $dt = c$ \\
$c$ \texttt{rls}-derivable iff
  $\exists$ valid derivation tree \texttt{dt} with conclusion $c$
% admissible rules, also neat example theorems
  \end{description}
\end{frame}

\begin{frame}[fragile]{Substitution in a hole in a structure}
\begin{description}[M]
\item[Example rule:] $(~~(X \smsc (Y \smsc Z))~,~(X \smsc Y \smsc Z)~~)\in rls$ 

\item 
\item[Context:] $C$ added around the required subsitution
\begin{verbatim}
inductive "sctxt r"
intrs
  scid "(a, b) : r       ==> (a, b)     : sctxt r" 
  scL  "(a, b) : sctxt r ==> (C;a, C;b) : sctxt r" 
  scR  "(a, b) : sctxt r ==> (a;C, b;C) : sctxt r" 
\end{verbatim}

\item 
\item[Example:] becomes
  $(\astr{U}{X \smsc (Y \smsc Z)}, ~~
  \astr{U}{X \smsc Y \smsc Z}) \in \mathtt{sctxt}\ rls$ 

\item 
\item[One-premise rule with this substitution in antecedent] ~\\
\begin{verbatim}
inductive "lctxt r" intrs
I "(As, Bs):sctxt r ==> ([As |- E], Bs |- E):lctxt r"
\end{verbatim}
 \item 
\item[Example:]
$([\astr{U}{X \smsc (Y \smsc Z)} \vdash E] ~~,~~
  \astr{U}{X \smsc Y \smsc Z} \vdash E) \in \mathtt{lctxt}\ rls$

  \end{description}
% lcB.I RS LTit_lcsub.B RS LTit_lc.sub ;
% lctxt.I RS LTit.lcrules ;
\end{frame}

\begin{frame}[fragile]{The complexity this adds to cut-admissibility proofs}
\begin{description}[M]
\item[Cut-admissibility] require re-ordering of  rule applications

\item[Define $(u,v) \in \mathtt{strrep}\ S$] to mean,
 ``$u$ and $v$ same except may differ at (several) subterms $u'$ and $v'$,
 where $(u', v') \in S$''

\begin{verbatim}
inductive "strrep S"
intrs 
 same "(s, s) : strrep S" 
 repl "p : S  ==> p : strrep S"
 sc   "(u, v) : strrep S ==> (x, y) : strrep S
                         ==> (u; x, v; y) : strrep S"
\end{verbatim}


\item[Lemma:] ``Closing the loop'' if
% strrep_sctxt_ext

$$
\frac{\mathcal C [p] }{\mathcal C [c_A]}
\begin{array}{c}
~ \\ {\stackrel{A \to X}\longrightarrow C_X}
\end{array}
$$

then there exist $\mathcal C'$ and $c_X$ st $C_X = \mathcal C' [c_X]$ where
$$
\frac{\mathcal C [p] \stackrel{A \to X}\longrightarrow \mathcal C' [p]}
  {\mathcal C [c_A] \stackrel{A \to X}\longrightarrow \mathcal C' [c_X]}
\quad
\mathrm{and}
\quad
c_A \stackrel{A \to X}\longrightarrow c_X
$$
\end{description}

\end{frame}

\begin{frame}{Inductive Multi-cut Admissibility via \texttt{gen\_step2}}

Suppose conclusions \texttt{cl} and
\texttt{cr} have respective derivations below:
\begin{center}
\begin{prooftree}
\AxiomC{$\MPL_{1} \;\ldots\; \MPL_{n}$}
\RightLabel{$\rho_l$}
\UnaryInfC{$\MCL$}
\AxiomC{$\MPR_{1} \;\ldots\; \MPR_{m}$}
\RightLabel{$\rho_r$}
\UnaryInfC{$\MCR$}
\RightLabel{(\textit{cut ?})}
\dottedLine
\BinaryInfC{?}
\end{prooftree}
\end{center}
\begin{itemize}
\item
We want to prove an arbitrary
property $P$ of these derivations, 
eg
(multi)cut-admissibility for a cut-formula $A$

\item
Proof is first, by induction on $A$, then on ``stage in the proof''

\item
Induction on ``stage in the proof'' assumes $P$ holds for each 
$\MPL_{i}$ with $\MCR$, and for each $\MPR_{j}$ with  $\MCL$

\item
\texttt{gen\_step2} expresses a single case of the inductive argument
\item
we have a lemma that this is enough for $P$ to hold generally

\end{itemize}
\end{frame}

\hide{
\begin{frame}{\texttt{gen\_step2} definition}
 \texttt{gen\_step2 P A sub (dls, drs) ((psl, cl), psr, cr)} means: \\
 (assuming \texttt{dls} and \texttt{drs} are the set of derivable sequents) \\
 if 
\begin{itemize}
\item \texttt{P~A' (dl, dr)} holds
 for all subformulae (\texttt{sub}) \texttt{A'} of \texttt{A}
 and derivable sequents \texttt{dl} and \texttt{dr} ;
\item for each \texttt{pl} $\in$ \texttt{psl}, \texttt{P A (pl, cr)} holds;
\item for each \texttt{pr} $\in$ \texttt{psr}, \texttt{P A (cl, pr)} holds;
\item (and \texttt{cl} and \texttt{cr} 
  and each \texttt{pl} and \texttt{pr} is derivable);
\end{itemize}
 then \texttt{P A (cl, cr)} holds 

So for example \texttt{P A (cl, cr)} could mean that the result of cutting
\texttt{cl} with \texttt{cr} (cut-formula \texttt{A}) is derivable.

\end{frame}

\begin{frame}{\texttt{gen\_step2} lemma}
\begin{itemize}
\item
Lemma: (assuming \texttt{sub} is well-founded): \\
\begin{itemize}
\item
If,  
for all rules \texttt{(psl, cl)} and \texttt{(psr, cr)}, \\
\texttt{gen\_step2} \ldots (ie, $args~as~above$) holds,
\item
then for all derivable sequents \texttt{seql} and \texttt{seqr}, \\
\texttt{P A (seqa, seqb)} holds
\end{itemize}
\item
This reflects that an inductive cut-admissibility proof 
works by a case analysis:
cases are the last rules on the left and right.
\item
Where these cases are similar for (eg) 
\lrarrow\ and \lrarrowt\
we avoid duplicating effort by proving intermediate lemmas like

\texttt{
     impL <= ?rls ==> \\
  gen\_step2 (mcd ?rls) ?A ?a (derrec ?rls \{\}, ?drsr)
     (([?G |- ?Aa, mins ?B ?H |- ?C], \\
     \hfill mins (?Aa -> ?B) ?G + ?H |- ?C), (?psr, ?cr))
}
\end{itemize}
\end{frame}
}

\begin{frame}{Machine-checked results for {$\lrarrow$, $\lrarrowt$, $\lrarrowc$,
   and $\lrarrowtc$}}

\begin{theorem}
\lrarrow\ and \lrarrowt\ enjoy multi-cut admissibility.
\end{theorem}
% [ mca_LRit, mca_LRi ] ;

\begin{theorem}
\lrarrowc\ and \lrarrowtc\ enjoy contraction admissibility.
\end{theorem}
% [ lctr_adm_LRisb, lca_LRitsb ] ;

\begin{corollary}
\lrarrowc\ and \lrarrowtc\ enjoy multi-cut admissibility.
\end{corollary}

\begin{itemize}
\item
Proved in a different order from the paper
(we couldn't reproduce the proof indicated briefly in B\&D)
\item
OOPS!  We actually needed
\begin{theorem}
\lrarrowc\ and \lrarrowtc\ enjoy height-preserving contraction admissibility.
\end{theorem}
% [ hplctr_LRisb, hplctr_LRitsb ] ;
This one uses the analogue, for concrete derivation trees, of the 
\texttt{gen\_step2} definition and lemmas
\end{itemize}

\end{frame}

\hide{
\begin{frame}{Cut-admissibility of \lrarrowtc}
\begin{description}
\item[Theorem~2.2]
The single cut rule is admissible in \lrarrowt\
\item[Theorem~2.4]
The single cut rule is admissible in \lrarrowtc\
\item[Lemma~2.5]
\ldots \lrarrowt\ and \lrarrowtc\ have the same set of theorems
\end{description}
\begin{itemize}
\item
we couldn't prove Theorem~2.4 in the usual way
\item
we first proved contraction-admissibility of \lrarrowtc\ \\
(giving the part of Lemma~2.5 shown)
\item 
Theorem~2.4 follows
\end{itemize}

\end{frame}
}

\begin{frame}{Multi-cut admissibility for $\ltarrowt$ and $\ltarrowtcirc$}

  \begin{description}[M]
  \item[Sequents:] For (multiset) sequents, ``multi-cut'' meant this:

\[
\AxiomC{$X \seq A$}
\AxiomC{$A^n, Y \seq B$}
\LeftLabel{(multicut)}
\BinaryInfC{$X, Y \seq B$}
\DisplayProof
\]
%$$\frac{X \vdash A \qquad A^n, Y \vdash B}{X, Y \vdash B}$$
\item[ie:] just one `$X$' in the consequent

\item 
\item[(structure) consecutions:] multi-cut means this:
\[
\AxiomC{$X \seq A$}
\AxiomC{$\astr{Y}{A}\astr{}{A}\cdots\astr{}{A} \seq B$}
\LeftLabel{(multicut)}
\BinaryInfC{$\astr{Y}{X}\astr{}{X}\cdots\astr{}{X} \seq B$}
\DisplayProof
\]
\item[ie:] multiple occurrences of `$X$' in the consequent


\item 
\begin{theorem}
\ltarrowt\ and \ltarrowtcirc\ enjoy multi-cut admissibility.
\end{theorem}
\end{description}

\end{frame}

\begin{frame}{Machine-checked Soundness and Completeness}
\begin{theorem}
\ltarrowt\ is complete for \tarrowt\ \\
\ltarrowtcirc\ is complete for \rarrowt\ 
\end{theorem}

\bigskip
For the sequent systems, we have proved
\begin{lemma}
for each rule of \lrarrow\ there is a ``corresponding'' 
proof in \rarrow\ (for some ordering of antecedents)
\end{lemma}

\bigskip
We still need to prove that any re-ordering of antecedents
in $A_1 \to A_2 \to \ldots \to A_n \to B$ is provable in \rarrow\
\end{frame}

\begin{frame}{Linking the sequent and consecution systems}

\begin{theorem}
Given a derivation in \ltarrowtcirc, 
we can, by turning structures into multi-sets,
obtain an ``equivalent'' derivation in \lrarrowt. \\
(``equivalent'' means ``same'' premises and conclusion,
not necessarily same proof steps)
\end{theorem}

\begin{itemize}
\item
This is the transformation $\pi$, which we have not actually defined,
we have just shown it exists.
\item
For the converse (using the $\tau$ transformation),
we need to prove that the rules of \ltarrowtcirc\ permit any
permutation and grouping, into a structure, of any multiset of formulae.
\item
Lemmas 8,9 and 10 do this for up to 3 formulae
(proved in Isabelle, but not in that order!)
\item
Need to extend this to any number of formulae 
(we have worked out argument, not proved)
\end{itemize}

\end{frame}

\begin{frame}{Background to decidability argument}

\begin{itemize}
\item multiset sequent system \lrarrowt\ for \rarrowt,
  includes contraction
\item \lrarrowtc\ incorporates limited contraction into $\limp\vdash$ rule,
  $[\limp\vdash]$ 
\item this gives height-preserving contraction admissibility,
so irredundant derivations, so decidable (Kripke, K\"onig lemmas)
\item likewise \lrarrowt\ and \lrarrowtc\ for $T_\limp^\verum$
\item structure sequent systems \ltarrowtcirc\ for $R_\limp^\verum$,
and \ltarrowt\ for $T_\limp^\verum$
\item proof transformations:
\begin{itemize}
\item $\pi$, \ltarrowtcirc\ to \lrarrowt\ (loses ordering/grouping) 
%Lemma 4
\item $\tau$, \lrarrowt\ to \ltarrowtcirc\ (recreates ordering/grouping)
%pg 227 middle, uses Lemmas 8 to 10
\item difference between $T_\limp^\verum$ and $R_\limp^\verum$
(ie, between \lrarrowt\ and \ltarrowtcirc) is 
(complete) availability of re-ordering 
\item $\tau$ produces several proofs in \ltarrowtcirc\
(choice of ordering/grouping)
\end{itemize}

\end{itemize}
\end{frame}

\begin{frame}{Decidability argument and issues }

\begin{itemize}
\item get all proofs in \lrarrowtc\

\item convert these into proofs in \lrarrowt\

\item transform them, using $\tau$, to proofs in \ltarrowtcirc\

\item examine which of these are proofs in \ltarrowt\
\end{itemize}

Issues arising:

\begin{itemize}
\item $\tau$ involves ``all permutations and groupings'': \\
should this be ``all \emph{proofs of} all permutations and groupings''? \\
(to find proof in \ltarrowt, if any)

\item even so, $\tau$ produces only proofs whose $\vdash\limp$,
$\limp\vdash$ and W$\vdash$ are in the same order as the given proof
in \lrarrowt\ ... is this enough?

\item that is, the algorithm produces only \ltarrowtcirc-proofs 
which contain these rules in the same order as a proof in 
\lrarrowtc\ ... what if the only \ltarrowt-proof contains them
in a different order?

\item note that obtaining an \lrarrowtc-proof from an \lrarrowt-proof
changes the order of these rules!
\end{itemize}

\end{frame}

\begin{frame}{Lemmas supporting $\tau$ transformation}

\begin{itemize}
\item[8]
If $\mathcal C [\mathcal A; \mathcal B] \vdash A$ 
provable in \ltarrowtcirc\
then so is $\mathcal C [t ; (\mathcal B; \mathcal A)] \vdash A$ \\
($\mathcal C$ is any structure with a ``hole'')
\item[9]
If $\mathcal C [\mathcal A_1; \mathcal A_2; \mathcal A_3] \vdash A$ 
provable in \ltarrowtcirc\ then so are 
$\mathcal C [t; \mathcal A_i; \mathcal A_j; \mathcal A_k] \vdash A$ and 
$\mathcal C [t; \mathcal A_i; (\mathcal A_j; \mathcal A_k)] \vdash A$  \\
(for all permutations $i,j,k$ of $1,2,3$)
\item[10]
If $\mathcal C [\mathcal A_1; \mathcal A_2; \mathcal A_3] \vdash A$ 
provable in \ltarrowtcirc\ then so are 
$\mathcal C [t; (\mathcal A_i; \mathcal A_j; \mathcal A_k)] \vdash A$ and 
$\mathcal C [t; (\mathcal A_i; (\mathcal A_j; \mathcal A_k))] \vdash A$ 
\item
The proof we found for 9 actually uses 10, which we proved first:
we didn't find the proof used by B\&D
\item
We also formulated an argument to deal with four or more substructures
\end{itemize}
\end{frame}

\begin{frame}{Do we actually need these lemmas?}
\begin{itemize}
\item
Lemmas 8,9 and 10: used to prove any permutation/grouping of antecedents
is provable in \ltarrowtcirc.

\item
The constructions described translate \lrarrowt-proofs to \ltarrowtcirc\ 

\item
We haven't yet found the result (that there exists an \ltarrowtcirc-proof)
to be necessary.

\item
The constructions may be relevant to an argument that
we will find a proof in \ltarrowt, if one exists; 

\item
BUT: if there is no proof in \ltarrowt, does it matter 
if these is no proof in \ltarrowtcirc\ either?

\item
We noticed this only when putting together the skeleton of a proof
in Isabelle.
\end{itemize}
\end{frame}

\begin{frame}{Proof trees and K\"onig's Lemma}
\begin{itemize}
\item
K\"onig's Lemma: \\ an infinite, finitely branching, 
  tree has an infinite branch

\item
When we build a proof tree, bottom (endsequent) up,
the intermediate stages
% are trees whose nodes are correct applications of the rules, but which 
have leaves yet unproved.

\item
We call these \emph{partial proof trees}.
We represent an ``infinite proof tree''
by an increasing sequence of partial proof trees:

\item
By K\"onig's Lemma, if such a sequence is infinite, then 
there must be a single infinitely increasing branch

\item
Note: finite branching property, because each rule has
finitely many premises

\item
And by Kripke's lemma there is no infinite irredundant branch of a 
(partial) proof tree in \lrarrowtc\

\item
Where does this get us?
\end{itemize}
\end{frame}

\begin{frame}{Proof search trees and K\"onig's Lemma}
Now consider a \emph{proof search tree}: 
\begin{itemize}
\item 
\begin{description}
\item[node:] partial proof tree, 
\item[edge:] extending a partial proof tree by adding one rule.
\end{description}

\item 
This is a different tree!!
This one is finitely branching because % different reason!!
\begin{itemize}
\item a partial proof tree has only finitely many unproved leaves, and
\item at each leaf, only finitely many rules can be applied.
\end{itemize}

\item 
The previous result (``no infinite proof tree'') says
proof search tree has no infinite branch.

\item 
K\"onig's Lemma, again, tells us that the proof search tree is finite,
that is, complete proof search is a finite process

\item 
so this logic is decidable.

\item 
This outline uses K\"onig's Lemma \emph{twice}!  Is this necessary?

\item 
Literature seems to use K\"onig's Lemma just once! \\
and to confuse proof trees with proof search trees
\end{itemize}

\end{frame}

\begin{frame}{Proving decidability}
\begin{itemize}
\item
To really formalise decidability, 
we would need to formalise steps of computation
(very low level)

\item
A finite proof search tree is not enough:
\begin{itemize}
\item
imagine a logic L, and we define a new logic L', by 
\begin{itemize}
\item
Axioms of L': theorems of L
\item
Rules of L': none
\end{itemize}
\item
In L', proof search tree (for given endsequent) is tiny, \\
but L' (may be) not decidable.
\end{itemize}

\item
We need further informal arguments, eg, that at any point it is
straightforward to determine which rules are applicable.
\end{itemize}
\end{frame}

\begin{frame}{Formalisation}

  \begin{description}[M]
  \item[use of Isabelle:] work verified in Isabelle theorem prover
  \item[value of formal verification:]
    detects gaps which may be overlooked in a proof
  \item[value of formalisation without verification:] 
    even preparing for formal verification
      alerts us to problems in a proof
  \item[difficult issues:] 
    K\"onig's lemma: what is an infinite proof tree? \\
    how to formalise branch of it
  \end{description}
\end{frame}

\begin{frame}{Main issue: unable to formalise BD proof of Lemma 11}
\begin{itemize}
\item all \lrarrowt-proofs $\longrightarrow$ all \ltarrowtcirc-proofs
\begin{itemize}
\item well, let's suppose so
\item actually depends on details of 
  ``all \emph{proofs of} all permutations and groupings''
\end{itemize}
\vfill
\item so all \lrarrowt-proofs $\longrightarrow$ (including) 
  all \ltarrowt-proofs
\vfill
\item but we need: all \lrarrowt-proofs from \lrarrowtc-proofs
$\longrightarrow$ at least one \ltarrowt-proof (if such exists)
\vfill
\item Question: are all \lrarrowt-proofs from \lrarrowtc-proofs
sufficiently representative of all \lrarrowt-proofs to ensure this?
\vfill
\item Note: all \lrarrowt-proofs from \lrarrowtc-proofs,
and the resulting \ltarrowtcirc-proofs, have limits on where contractions
can appear
\end{itemize}

\end{frame}

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
