\documentclass[12pt]{beamer}
\usepackage[latin9]{inputenc}
\usepackage{logictheme}
\usefonttheme[onlymath]{serif}

\usecolortheme[rgb={.02,.3,.05}]{structure}
\setbeamercolor{palette secondary}{fg=black!60!averagebackgroundcolor}

\setbeamertemplate{theorems}[ams style]
%\setbeamercolor{titlelike} 
%	       {use={palette primary},fg=black,bg=palette
%		 primary.bg} 

%\input{entete}
%\input{/Users/gburel/asbi/aacs/macros_modified}
%\input{sequents}
%\usepackage{bussproofs}
\usepackage{prooftree}
\usepackage{upgreek}
\usepackage[all]{xy}
\input{natdedmod}
\input{/Users/gburel/cvs/asbi/arith/entete}

%\input{structure}
%\input{sequent}

\providecommand{\R}{\mathcal R}
\providecommand{\inc}{~\upepsilon~}
\providecommand{\inlineinc}{\upepsilon}
\providecommand{\ang}[1]{\langle #1\rangle}
\newcommand{\leadsfrom}{\kern-.1em\rotatebox{180}{$\leadsto$}}
\newcommand{\bigO}{\textup{O}}

\providecommand{\vect}[2][n]{{#2}_1,\ldots,{#2}_{#1}}

\title{Unbounded Proof-Length Speed-up\\ in Deduction Modulo}
\subtitle[CSL 07]{16th EACSL Annual Conference on Computer Science and Logic}
\author{Guillaume Burel}
\date[2007-09-14]{September 14$^{\text{th}}$, 2007}
\institute[UHP/LORIA]{Université Henri Poincaré -- LORIA {\small(INRIA)}}
\setbeamertemplate{caption}[numbered]
\logo{\includegraphics[height=.06\textheight]{loria.jpg}\hspace{.04\textheight}\includegraphics[height=.06\textheight]{logo_uhp.jpg}}

%\includeonlyframes{current}

\newcommand\lvdash[2][]{\mathrel{\rule{.08ex}{1.5ex}\kern-.12em\lower-.08em\hbox{$\frac{\scriptstyle\,#1\hfill}{\scriptstyle~#2\,}$}}}
\newcommand\Hvdash{\lvdash[\textup{\textsf{S}}]}
\newcommand\Nvdash{\lvdash[\textup{\textsf{N}}\!]}
  
\begin{document}


\begin{frame}
\titlepage
\end{frame}
\newcommand{\mytimes}{\cdot}

\section{Motivations}
\subsection{Deduction modulo}

\begin{frame}
 \frametitle{Proving that the square of an even number is even:}
\smallskip\pause

Take a number $x$.
\smallskip\pause

Suppose it is even.
\smallskip\pause

Then it is the double of some number $y$. \hfill($x = 2\mytimes y$)
\smallskip\pause

Then \alert<8>{one can compute} that the square of $x$ is the double of
the double of the square of $y$. \hfill($x^2 = 2\mytimes(2\mytimes y^2)$)
\smallskip\pause

Therefore the square of $x$ is even.
\smallskip\pause

QED.
\end{frame}

\begin{frame}<-21>
\alt<-12>{\small\begin{prooftree}
\[\[\[
\[
\[
\[
\Axiomm<3->{i}{Even(x)}
  \[\Axiomm<7->{def}{\forall x.~Even(x)\imp\exists y.~x=2\mytimes y}
  \AllE<8->
  \onslide<8->{Even(x)\imp\exists y.~x=2\mytimes y}
  \]
\ImpE<9->
\shiftleft60pt
\onslide<9->{\exists y.~x=2\mytimes y}
\]
 \ExE<10->
 \onslide<10->{x=2\mytimes y}
\]
\unknow<12->[??]
  \onslide<11->{x\mytimes x = 2\mytimes (y\mytimes (2\mytimes y))}
\]
\ExI<11->
  \onslide<6->{\exists y.~x\mytimes x = 2\mytimes y}
  \]
\kern-120pt\[
\Axiomm<4->{def}{\forall x.~(\exists y.~x=2\mytimes y)\imp Even(x)}
 \AllE<5->
 \onslide<5->{(\exists y.~x\mytimes x=2\mytimes y)\imp Even(x\mytimes x)}
\]
\ImpE<6->
 \onslide<3->{Even(x\mytimes x)}
\]
\ImpI<3->[\text{(i)}]
 \onslide<2->{Even(x)\imp Even(x\mytimes x)}
\]\AllI<2->
\forall x.~Even(x)\imp Even(x\mytimes x)
\end{prooftree}}%
%
%
%
{
\tiny
\begin{prooftree}
\[\[\[\[
\alt<13,16-18,20->{\onslide<16->{\alert<21>{\pi}}}{\[\Axiomm<14->{ax}{\forall x~y~z.~(x\mytimes y)\mytimes z = x\mytimes (y\mytimes z)}
\AllE<15->[\times 3]
\onslide<15->{(2\mytimes y)\mytimes (2\mytimes y) = 2\mytimes (y\mytimes (2\mytimes y))}
\]}\[\[
\[
\[
\Axiomm<3->{i}{Even(x)}
  \[\Axiomm<7-| alert@21>{def}{\forall x.~Even(x)\imp\exists y.~x=2\mytimes y}
  \AllE<8-| alert@21>
  \onslide<8->{\alert<21>{Even(x)\imp\exists y.~x=2\mytimes y}}
  \]
\ImpE<9-| alert@21>
\shiftleft60pt
\onslide<9->{\alert<21>{\exists y.~x=2\mytimes y}}
\]
\ExE<10-| alert@21>
 \onslide<10->{x=2\mytimes y}
\]
\unknow<20->[??]
\onslide<18->{x\mytimes x = (2\mytimes y)\mytimes (2\mytimes y)}\]
\kern-110pt
\[\Axiomm<16-| alert@21>{ax}{\forall x~y~z.~x  = y\imp y = z \imp x = z}
 \AllE<17-| alert@21>[\times 3]
\onslide<17->{\alert<21>{x\mytimes x = (2\mytimes y)\mytimes (2\mytimes y)\imp 
(2\mytimes y)\mytimes (2\mytimes y) = 2\mytimes (y\mytimes (2\mytimes y)) \imp 
x\mytimes x = 2\mytimes (y\mytimes (2\mytimes y))}}\]
\ImpE<18-| alert@21>
\kern-180pt \onslide<18->{\alert<21>{(2\mytimes y)\mytimes (2\mytimes y) = 2\mytimes (y\mytimes (2\mytimes y)) \imp 
x\mytimes x = 2\mytimes (y\mytimes (2\mytimes y))}}
\]
\ImpE<19-| alert@21>
\shiftleft40pt  \onslide<11->{x\mytimes x = 2\mytimes (y\mytimes (2\mytimes y))}
\]
\ExI<11->
  \onslide<6->{\exists y.~x\mytimes x = 2\mytimes y}
  \]
\kern-200pt\[
\Axiomm<4-| alert@21>{def}{\forall x.~(\exists y.~x=2\mytimes y)\imp Even(x)}
 \AllE<5-| alert@21>
 \onslide<5->{\alert<21>{(\exists y.~x\mytimes x=2\mytimes y)\imp Even(x\mytimes x)}}
\]
\ImpE<6-| alert@21>
 \onslide<3->{Even(x\mytimes x)}
\]
\ImpI<3->[\text{(i)}]
 \onslide<2->{Even(x)\imp Even(x\mytimes x)}
\]\AllI<2->
\forall x.~Even(x)\imp Even(x\mytimes x)
\end{prooftree}}

\end{frame}

\begin{frame}
  \frametitle{Deduction modulo \cite{DHK-TPM-JAR}}

Computational part expressed as a rewrite system over terms and
propositions
\pause

For instance $$
\begin{array}{c}
  s(x)\mytimes y\rightarrow x\mytimes y+ y\\
  Even(x)\rightarrow \exists y.~x=2\mytimes y
\end{array}$$
\pause

Inferences performed modulo this congruence:
$$
\begin{prooftree}
  A \qquad
  \begin{array}[b]{c@{}}
    [B]\\
    \\
    C
  \end{array}
\ExE[A\sRew^*\exists x. D\text{ and }B\sRew^*\subst Dyx]
C
\end{prooftree}
$$

\end{frame}

\begin{frame}
    \begin{prooftree}
\[\[\[
  \Axiomm{i}{Even(x)}
\qquad
  \Axiomm<3->{ii}{x=2\mytimes y}
  \ExE<2->[\text{(ii) }
     \begin{array}{r@{\,}c@{\,}l}
       Even(x)&\sRew^*&\exists y.~x=2\mytimes y\\
\onslide<4->{x=2\mytimes y}&\onslide<4->{\sRew^*}&\onslide<4->{x\mytimes x = 2\mytimes(2\mytimes
       y\mytimes y)}
     \end{array}
     ]
 \onslide<4->{x\mytimes x=2\mytimes(2\mytimes y\mytimes y)}
\]
\ExI<5->[Even(x\mytimes x)\sRew^*\exists y.~x\mytimes x=2\mytimes
     y]
  \onslide{Even(x\mytimes x)}
\]
\ImpI[\text{(i)}]
 \onslide{Even(x)\imp Even(x\mytimes x)}
\]
\AllI
\forall x.~Even(x)\imp Even(x\mytimes x)
   \end{prooftree}

%%   \Axiomm<2->[i]$Even(x)$
%%   \Axiomm[ii]$x=2\mytimes y$
%%   \ExE<2->[(ii) $
%%     \begin{array}{r@{\,}c@{\,}l}
%%       Even(x)&\sRew^*&\exists y.~x=2\mytimes y\\&\sRew^*&\exists y.~x\mytimes x = 2\mytimes(2\mytimes
%%       y\mytimes y)
%%     \end{array}
%%     $]$x\mytimes x=2\mytimes(2\mytimes
%%     y\mytimes y)$
%%   \ExI[$Even(x\mytimes x)\sRew^*\exists y.~x\mytimes x=2\mytimes
%%     y$]$Even(x\mytimes x)$
%%   \ImpI[(i)]$Even(x)\imp Even(x\mytimes x)$
%%   \AllI$\forall x.~Even(x)\imp Even(x\mytimes x)$
%%     \DisplayProof
\end{frame}

\subsection{Proof length in arithmetic}
\begin{frame}
  \frametitle{Arithmetic}
First-order arithmetic: 

$0$, $s$, $+$, $\mytimes$, induction principle
$$P(0)\imp(\forall x.~P(x)\imp P(s(x)))\imp\forall x.~P(x)$$
\medskip\pause

Second-order arithmetic: 

sets of natural numbers, $\in$, comprehension schema:
$$\exists S.~\forall n.~n\in S \Leftrightarrow P(n)$$
\medskip\pause

Possibility to prove stronger principles (e.g. transfinite induction
up to $\epsilon_0$)


\end{frame}

\begin{frame}
  \begin{theorem}[Buss (conjectured by Gödel)]\label{theo:buss}
   Let $i\geq 0$. Then there is an infinite family $\mathcal F$ of
   $\prod_1^0$-formul\ae\ such that 
   \begin{enumerate}
   \item for all $\phi\in\mathcal F$, $Z_i\vdash\phi$
   \item there is a fixed $k\in\mathbb N$ such that for all
     $\phi\in\mathcal F$, $Z_{i+1}\lvdash{k\text{ steps}}\phi$
   \item there is no fixed $k\in\mathbb N$ such that for all
     $\phi\in\mathcal F$, $Z_i\lvdash{k\text{ steps}}\phi$

   \end{enumerate}
  \end{theorem}
\end{frame}

\begin{frame}
\frametitle{Questions}

Same proof length speed-up in deduction modulo ?
\bigskip\pause

Speed-up in arithmetic : due to computation or to deduction ?
\end{frame}

\AtBeginSection[]{
\begin{frame}
\frametitle{Outline} 
\tableofcontents[currentsection] 
\end{frame} 
} 

\section{Speed-up in deduction modulo}

\begin{frame}
 \frametitle{Reducing proof length in deduction modulo}

``Hide'' the computational part in the side conditions

 $\imp$ proofs are smaller
\medskip

Take $s(x)+y\rightarrow x+s(y)$.

$$\lvdash{1\text{ step}} \underline{n} + \underline{n} =
\underline{n+n}\text{ in deduction modulo}$$

$$\forall x~y.~s(x)+y=x+s(y)\lvdash{O(n)\text{ steps}} \underline{n} + \underline{n}=
\underline{n+n}\text{ in pure deduction}$$

$\left(\underline{n} = \underbrace{s(s(\cdots(s}_{n\text{ times}}(0))))\right)$
\end{frame}

\begin{frame}
  \frametitle{Computational vs. deductive complexity}
Do not suppress the complexity of the proofs, but separate it between
deduction and computation.
\bigskip\pause

\begin{tabular}{ccc}
  computation & vs. & deduction\\
$\simeq$ & & $\simeq$\\
verification & vs. & inference
\end{tabular}
\medskip

\emph{Not acceptable:} a rewrite system semi-deciding validity of formul\ae
\medskip

\emph{Here:} finite, terminating, confluent, linear rewrite systems 

\end{frame}


\section{Speed-ups in arithmetic and computation}
\begin{frame}
  \frametitle{Sketch of proof}

\xymatrix{Z_{i+1} \ar[rr]^{\bigO(n)} &&
  Z_i\text{ mod }\R_i\\
  & \ar@{->>}[ul]^{\text{speedup (Buss)}} \ar@{->>}[ur]_{\text{computational speed-up}}Z_i}
\medskip\pause

But: Buss' theorem proved for schematic systems, deduction modulo defined
for natural deduction

\end{frame}


\subsection{Schematic systems}
\begin{frame}
  \frametitle{Schematic systems}
Buss theorem is true if proofs are done in 

schematic systems
\medskip

$\simeq$ Hilbert-type systems
\medskip

$\simeq$ Frege systems
\end{frame}

\begin{frame}
  \frametitle{Metaformul\ae}
  \begin{definition}[Metaformul\ae]
First-order signature +
\begin{itemize}
\item metavariables $\alpha^i$ (substituted by variables)
\item term variables $\tau^i$ (substituted by terms)
\item formula variables $A(\vect x)$ (substituted by formul\ae)
\end{itemize}
  \end{definition}
\end{frame}

\begin{frame}
  \frametitle{Schematic System}
  \begin{definition}[Schematic System]
Set of inference rules $$\vect{\Phi}/\Psi\quad(C)$$
with $\vect{\Phi},\Psi$ metaformul\ae\ and $C$ side-condition of the
form

$\alpha^j$ is not free in $\Phi$

$\tau^j$ is freely substitutable for $\alpha^j$ in $\Phi$

\medskip

A proof consists of a sequence of formul\ae\ where each formula is
derived from earlier formul\ae\ by instantiating an inference
rule.
  \end{definition}
\end{frame}

\begin{frame}
\frametitle{Schematic System for $i^{\text{th}}$-Order Arithmetic}
\begin{itemize}
\item Axiom schemata for classical logic with equality: $\overline{A\imp B\imp
  A}$\hfill $\overline{\forall\alpha^0\beta^0.~\alpha^0=\beta^0\imp A(\alpha^0)\imp A(\beta^0)}$


\item Inference rules for classical logic:\\ Modus Ponens: 
  \begin{prooftree}
    A\imp B~~~~~A
    \justifies
    B
  \end{prooftree}\\
\begin{prooftree}A\imp B(\beta^j)
\justifies
A\imp\forall\alpha^j.~B(\alpha^j)
\end{prooftree}
$(\beta^j$ is not free in $A\imp\forall\alpha^j.~B(\alpha^j))$
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Schematic System for $i^{\text{th}}$-Order Arithmetic (cont.)}
\begin{itemize}
\item Robinson axioms: $\overline{\forall\alpha^0.~0+\alpha^0=\alpha^0}$,
  $\overline{\forall\alpha^0\beta^0.~s(\alpha^0)+\beta^0=s(\alpha^0+\beta^0)}$
\medskip

\item Induction for all formul\ae\ of $Z_i$:
  \alert<2>{$\overline{A(0)\imp\left(\forall\beta^0.~A(\beta^0)\imp
  A(s(\beta^0))\right)\imp \forall \alpha^0.~A(\alpha^0)}$}\medskip

\item Comprehension schema:
  \alert<2>{${\overline{\exists\alpha^{j+1}.~\forall\beta^j.~\beta^j\in\alpha^{j+1}\Leftrightarrow
  A(\beta^j)}}$}
provided $\alpha^{j+1}$ is not free in A, for $j<i$

\end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Notations}

$$Z_i\Hvdash{k}P:$$

$P$ is provable in this schematic system in at most $k$ steps
\smallskip\pause

$$Z_i\Nvdash{k}P:$$

$P$ is provable in natural deduction using as assumptions Robinson
axioms and a finite number of \emph{instances} of Leibniz' equality, Induction and
Comprehension schemata (for $i^{\text{th}}$-order arithmetic)
\smallskip\pause

$$Z_i\Nvdash{k}_\R P:$$

$P$ is provable in natural deduction modulo $\R$ using the same assumptions
\end{frame}



\subsection{Translations}

\begin{frame}
  \frametitle{From $Z_{i}\Hvdash{}$ to $Z_{i}\Nvdash{}$}

  \begin{tabular}{|p{.45\textwidth}|p{.45\textwidth}|}
\hline classical logic & translated as in\\& \cite{gentzen:untersuchungen}
\\\hline
Robinson axioms & kept as assumption\\\hline
Leibniz' equality, induction and comprehension schemata &\emph{instances} kept as
assumptions (finite number in a proof)\\\hline
  \end{tabular}
\bigskip

$$Z_i\Hvdash{k} P\rightsquigarrow Z_i\Nvdash{O(k)}P$$
\end{frame}

\begin{frame}
  \frametitle{From $Z_{i}\Nvdash{}$ to $Z_{i}\Hvdash{}$}
Quite similar to the translation of a $\lambda$-term into a term of
combinatory logic 

For instance $
\begin{prooftree}
\begin{array}{@{}c@{}}
[Q]\\\\P
\end{array}
\ImpI
Q\imp P 
\end{prooftree}
~~~\rightsquigarrow~~~
\begin{prooftree}
  P\quad\[\justifies P\imp Q\imp P\]
  \proofleft{MP}
  \justifies 
  Q\imp P
\end{prooftree}
$

if $Q$ is actually not used as assumption


\bigskip

$$Z_i\Nvdash{k} P\rightsquigarrow Z_i\Hvdash{O(3^k)}P$$
\end{frame}

\begin{frame}
  \frametitle{Simulating $i+1^{\text{st}}$-order using computations}

Work of [F. Kirchner, 2006]:

Metaformula $A(\vect x)$ is replaced by a formula $\langle\vect
x\rangle\inc c$ \bigskip


$c$: some term representing the formula substituted for $A$

For instance: $P = (x=0\vee\exists y.~x \in^0y)~~~~\rightsquigarrow$\\$
{c_P^x~~=~~\doteq(1,S(0))}~\cup~\mathcal P^1\left(\dot{\in}^0(S(1),1)\right)$

\end{frame}

\begin{frame}
\frametitle{Rewriting classes}
Terminating and confluent rewrite system:
$$\kern-10pt\begin{array}{@{}c@{}c}\begin{array}{r@{~\rightarrow~}l}\alert<10>{t[nil]^j}& \alert<11>{t}\\
\alert<6,18,20>{1^j[t::^jl]^j}& \alert<7,19,21>{t}\\
\alert<8,16>{S^j(n)[t::^jl]^j}&\alert<9,17>{n[l]^j}\\
s(n)[l]^0& s(n[l]^0)\\
(t_1+t_2)[l]^0& t_1[l]^0+t_2[l]^0\\
(t_1\times t_2)[l]^0& t_1[l]^0\times t_2[l]^0\\
\alert<4>{l\inc\doteq(t_1,t_2)}& t_1[l]^0 = t_2[l]^0\\
  \end{array}
\end{array}
\begin{array}{cc}\begin{array}{r@{~\rightarrow~}l}\alert<14>{l\inc{\dot{\in}}^j(t_1,t_2)}& \alert<15>{t_1[l]^j \in^j t_2[l]^{j+1}}\\
\alert<2>{l\inc A\cup B}& \alert<3>{l\inc A\vee l\inc B}\\
l\inc A\cap B& l\inc A\wedge l\inc B\\
l\inc A\supset B& l\inc A\imp l\inc B\\
%\end{array}$$$$
%\begin{array}{r@{~\rightarrow~}l}
l\inc \emptyset& \bot\\
\alert<12>{l\inc \mathcal P^j(A)}& \alert<13>{\exists x.~x::^jl\inc A}\\
l\inc \mathcal C^j(A)& \forall x.~x::^jl\inc A
\end{array}
\end{array}
$$ \bigskip

$$\langle t\rangle\inc
c_P^x\alt<1-2>{~~=~~}{\mathop{\longrightarrow}\limits^{*}}\only<1-2>{\langle t\rangle\inc\doteq(1,S(0))~\alert<2>{\cup}~\mathcal
  P^1\left(\dot{\in}^0(S(1),1)\right)}%
\only<3-4>{\langle t\rangle\alert<4>{\inc\doteq}(1,S(0))~\alert<3>{\vee}~\langle t\rangle\inc\mathcal
  P^1\left(\dot{\in}^0(S(1),1)\right)}%
\only<5-6>{\alert<6>{1[t]} \alert<5>{=} S(0)[t]~\vee~\langle t\rangle\inc\mathcal
  P^1\left(\dot{\in}^0(S(1),1)\right)}%
\only<7-8>{\alert<7>{t} = \alert<8>{S(0)[t]}~\vee~\langle t\rangle\inc\mathcal
  P^1\left(\dot{\in}^0(S(1),1)\right)}%
\only<9-10>{t = \alert<9-10>{0[nil]}~\vee~\langle t\rangle\inc\mathcal
  P^1\left(\dot{\in}^0(S(1),1)\right)}%
\only<11-12>{t = \alert<11>{0}~\vee~\langle t\rangle\alert<12>{\inc\mathcal
  P^1}\left(\dot{\in}^0(S(1),1)\right)}
\only<13-14>{t = 0~\vee~\alert<13>{\exists y.}~\langle \alert<13>{y::^1}t\rangle\alert<14>{\inc\dot{\in}^0}(S(1),1)}%
\only<15-16>{t = 0~\vee~\exists y.~\alert<16>{S(1)[y::t]} \alert<15>{\in} 1[y::t]}%
\only<17-18>{t = 0~\vee~\exists y.~\alert<17-18>{1[t]} \in 1[y::t]}%
\only<19-20>{t = 0~\vee~\exists y.~\alert<19>{t} \in \alert<20>{1[y::t]}}%
\only<21-22>{t = 0~\vee~\exists y.~t \in \alert<21>{y}}\onslide<22>{~~=~~\{t/x\}P}{}
$$
\end{frame}

\begin{frame}
  \frametitle{From axiom schemata to axioms}
The instance of the induction schema  
$$P(0)\imp\left(\forall\beta^0.~P(\beta^0)\imp
  P(s(\beta^0))\right)\imp \forall \alpha^0.~P(\alpha^0)$$


becomes\bigskip

\small
~\kern-20pt$
  \begin{prooftree}
    \Axiomm{IA}{\forall \gamma^c.\langle 0\rangle\inc\gamma^c\imp\left(\forall\beta^0.~\langle\beta^0\rangle\inc\gamma^c\imp
      \langle s(\beta^0)\rangle\inc\gamma^c\right)\imp \forall \alpha^0.~\langle\alpha^0\rangle\inc\gamma^c}
    \AllE
    P(0)\imp\left(\forall\beta^0.~P(\beta^0)\imp
    P(s(\beta^0))\right)\imp \forall \alpha^0.~P(\alpha^0)
  \end{prooftree}
  $

\hfill(for all $t$, $\langle t\rangle\inc c_{P(x)}^x\rewrite^*P(t)$)
\bigskip\pause

New axioms $\Gamma$ replacing the axiom schemata for Leibniz' equality,
induction and comprehension

\end{frame}

\begin{frame}
  \frametitle{From $Z_{i+1}\Hvdash{}$ to $Z_{i}\Nvdash{}_{\R_i}$}

Instance of axiom schemata for $i+1^{\text{st}}$-order arithmetic can be simulated
by axioms, using the modulo.
\medskip

$$Z_{i+1}\Hvdash{k} P\rightsquigarrow Z_i,\Gamma\Nvdash{O(k)}_{\R_i}P$$
\bigskip\pause

also for natural deduction:
\begin{theorem}\label{theo:s3}
For all $i\geq 0$, there exists a (finite terminating confluent linear) rewrite system $\R_i$ and a
finite set of axioms $\Gamma$ such that
 for all formul\ae\ $ P$, if ${Z_{i+1}\Nvdash{k} P}$ then 
  $Z_i,\Gamma\Nvdash{O(k)}_{\R_i} P$.
  \end{theorem}
\end{frame}

\subsection{Speed-up}
\begin{frame}
  \frametitle{Adding computation creates a speed-up}

  \begin{theorem}
    For all $i\geq 0$, there is a (finite terminating confluent
    linear) rewrite system $\R_i$ such that    
there is an infinite family $\mathcal F$ such that 
   \begin{enumerate}
   \item for all $ P\in\mathcal F$, $Z_i\Nvdash{\,} P$
   \item there is a fixed $k\in\mathbb N$ such that for all
     $ P\in\mathcal F$, ${Z_i\Nvdash{k\text{ steps}}_{\R_i} P}$
   \item there is no fixed $k\in\mathbb N$ such that for all
     $ P\in\mathcal F$, ${Z_i\Nvdash{k\text{ steps}} P}$
   \end{enumerate}
  \end{theorem}
\end{frame}

  \begin{frame}
    \begin{proof}
$P' = \Gamma\imp P$ 
\pause

     $$
\renewcommand{\arraystretch}{1.5}
  \begin{array}[b]{ccccl}
Z_{i+1}\Hvdash{k} P
& \onslide<3->{\mathop{\leadsto}} 
& \onslide<3->{Z_i,\Gamma\Nvdash{K}_{\R_i} P}  
& \onslide<4->{\leadsto}
& \onslide<4->{Z_i\Nvdash{K+3}_{\R_i} P'} \\

\text{\scriptsize Theo.~\ref{theo:buss}}\updownarrow\\
 
Z_i\Hvdash{\onslide<11->{\not~\not~\not~\not\kern-.9em}\onslide<10->{3^{k+3}}} P
& 
\renewcommand{\arraystretch}{.2}
\begin{array}[B]{c}
\onslide<5->{\leadsto} \\
\onslide<10->{\leadsfrom}
\end{array}
& \onslide<5->{Z_i\only<6->{,\Gamma}\Nvdash{\onslide<12->{\not~\not~\not~\not\kern-.9em}\onslide<9->{k+3}} P}  
& \onslide<7->{\leadsto}
& \onslide<7->{Z_i\Nvdash{\onslide<12->{\not}\onslide<8->{k}} P'} \\
  \end{array}$$
    \end{proof}
  \end{frame}


\section{Conclusion}

\begin{frame}<-3>[label=current]
  Difference between $i+1^{\text{st}}$- and $i^{\text{th}}$-order arithmetic :  expressed
  as a confluent and terminating rewrite system 

  The length of the deductive part of the proofs remains the same
\medskip\pause

\hfill
  \alt<2>{\xymatrix{Z_{i+1} \ar[rr]^{\bigO(n)} &&
      Z_i\text{ mod }\R_i\\\\
      & \ar@{->>}[uul] \ar@{->>}[uur]_{\text{computational speed-up}}Z_i}
  }{\xymatrix{Z_{i+1} \ar[rr]^{\bigO(n)} &&
      Z_i\text{ mod }\R_i\\
      &\ar@{->>}[ul] \ar@{->>}[ur]_{\text{computational speed-up}} Z_i+T_i\\
      & \ar@{->>}[u]^{\text{speedup (Buss)}} Z_i}
  }\hfill\ 




\end{frame}

\begin{frame}
\frametitle{Perspectives}
It is possible to give a full axiomatization of higher-order
arithmetic entirely as a theory modulo
(\url{http://www.loria.fr/~burel/download/hhamod.pdf})
\medskip\pause

Next step: difference between higher-order logic and first-order logic
modulo

\begin{tabular}{c@{~}c@{~}l@{~}l}
HOL&simulated by&HOL-$\lambda\sigma$&\cite{hollambdasigma} \\
every PTS&''&$\lambda\Pi$ modulo&[D. Cousineau et al., 2007] \\
$\lambda\Pi$&''&FOL modulo&[Work in progress]
\end{tabular}


\end{frame}


\bibliographystyle{apalike}
\bibliography{abbrev,burel,protheo}

\end{document}
