\documentclass[runningheads]{llncs}

\usepackage[latin9]{inputenc}
\usepackage{amsfonts,amssymb,amsmath}

% from the sample file typeinst.tex
\setcounter{tocdepth}{3}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\usepackage{url}

\usepackage{upgreek}
\usepackage{graphicx}
\usepackage{bussproofs}

%% begin macros
\newcommand{\rewrite}{\mathop{\longrightarrow}\limits}
\newcommand{\sRew}{\mathop{\longleftrightarrow}\limits}
\newcommand{\terms}[2]{\mathcal T(#1,#2)}
\providecommand{\Def}[1]{{\em #1}}
\providecommand{\df}{~~~\mathop{=}\limits^!~~~}
\providecommand{\inlinedf}{\mathop{=}\limits^!}
\newcommand{\vect}[2][n]{#2_{1},\ldots,#2_{#1}}
\newcommand{\subst}[3]{\{#2/#3\}#1}
\newcommand{\subterm}[2]{{#1}_{|#2}}
\newcommand{\replacement}[3]{{#1}[#2]_{#3}}
\def\fCenter{\vdash}
\def\Tndd$#1${\AxiomC{}\LeftLabel{\emph{classical}}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\Tnda[#1]$#2${\AxiomC{}\LeftLabel{\emph{classical}}\RightLabel{\scriptsize#1}
\UnaryInfC{$#2$}}
\def\ImpId$#1${\LeftLabel{$\imp$-i}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\ImpIa[#1]$#2${\RightLabel{\scriptsize#1}\ImpI$#2$}
\def\ImpEd$#1${\LeftLabel{$\imp$-e}%\RightLabel{\scriptsize#1}
\BinaryInfC{$#1$}}
\def\ImpEa[#1]$#2${\RightLabel{\scriptsize#1}\ImpE$#2$}
\def\AndId$#1${\LeftLabel{$\wedge$-i}%\RightLabel{\scriptsize#1}
\BinaryInfC{$#1$}}
\def\AndIa[#1]$#2${\RightLabel{\scriptsize#1}\AndI$#2$}
\def\AndEd$#1${\LeftLabel{$\wedge$-e}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\AndEa[#1]$#2${\RightLabel{\scriptsize#1}\AndE$#2$}
\def\OrId$#1${\LeftLabel{$\vee$-i}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\OrIa[#1]$#2${\RightLabel{\scriptsize#1}\OrI$#2$}
\def\OrEd$#1${\LeftLabel{$\vee$-e}%\RightLabel{\scriptsize#1}
\TrinaryInfC{$#1$}}
\def\OrEa[#1]$#2${\RightLabel{\scriptsize#1}\OrE$#2$}
\def\AllId$#1${\LeftLabel{$\forall$-i}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\AllIa[#1]$#2${\RightLabel{\scriptsize#1}\AllI$#2$}
\def\AllEd$#1${\LeftLabel{$\forall$-e}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\AllEa[#1]$#2${\RightLabel{\scriptsize#1}\AllE$#2$}
\def\ExId$#1${\LeftLabel{$\exists$-i}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\ExIa[#1]$#2${\RightLabel{\scriptsize#1}\ExI$#2$}
\def\ExEd$#1${\LeftLabel{$\exists$-e}%\RightLabel{\scriptsize#1}
\BinaryInfC{$#1$}}
\def\ExEa[#1]$#2${\RightLabel{\scriptsize#1}\ExE$#2$}
\def\BotEd$#1${\LeftLabel{$\bot$-e}%\RightLabel{\scriptsize#1}
\UnaryInfC{$#1$}}
\def\BotEa[#1]$#2${\RightLabel{\scriptsize#1}\BotE$#2$}
\def\atocd$#1$$#2${\AxiomC{[$#1$]}\noLine\UnaryInfC{$#2$}}
\def\atoca[#1]$#2$$#3${\AxiomC{[$#2$]}\noLine\LeftLabel{$#1$\{}\UnaryInfC{$#3$}}
\def\Axiomm[#1]$#2${\AxiomC{$#2${ \scriptsize (#1)}}}
\makeatletter
\def\Tnd{\@ifnextchar[{\Tnda}{\Tndd}}
\def\ImpI{\@ifnextchar[{\ImpIa}{\ImpId}}
\def\AndI{\@ifnextchar[{\AndIa}{\AndId}}
\def\OrI{\@ifnextchar[{\OrIa}{\OrId}}
\def\AllI{\@ifnextchar[{\AllIa}{\AllId}}
\def\ExI{\@ifnextchar[{\ExIa}{\ExId}}
\def\ImpE{\@ifnextchar[{\ImpEa}{\ImpEd}}
\def\AndE{\@ifnextchar[{\AndEa}{\AndEd}}
\def\OrE{\@ifnextchar[{\OrEa}{\OrEd}}
\def\AllE{\@ifnextchar[{\AllEa}{\AllEd}}
\def\ExE{\@ifnextchar[{\ExEa}{\ExEd}}
\def\BotE{\@ifnextchar[{\BotEa}{\BotEd}}
\def\atoc{\@ifnextchar[{\atoca}{\atocd}}
\makeatother
\newcommand{\leadsfrom}{\kern-.1em\rotatebox{180}{$\leadsto$}}
\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}}\!]}
\providecommand{\imp}{\Rightarrow}
\providecommand{\ra}{\rightarrow}
\newcommand{\R}{\mathcal R}
\newcommand{\bigO}{O}
\newcommand{\mysubsubsection}[1]{\noindent\textbf{#1}}
%% end macros


\begin{document}

\mainmatter % start of an individual contribution

\title{Unbounded Proof-Length Speed-up in Deduction Modulo}

\author{Guillaume Burel\inst{1}}
%
\authorrunning{G. Burel}   % abbreviated author list (for running head)
%
%%%% modified list of authors for the TOC (add the affiliations)
\tocauthor{Guillaume Burel (UHP \& LORIA)}
%
\institute{%
Université Henri Poincaré \& LORIA\inst{2}
\\Campus scientifique BP 239 --- 54506 Vand\oe uvre-lès-Nancy Cedex France
\\\email{guillaume.burel@ens-lyon.org}
\and{\scriptsize UMR 7503 CNRS-INPL-INRIA-Nancy2-UHP}
}

\maketitle

\begin{abstract}
In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37
years before: there exist arithmetical
formul\ae\ that are provable in first order arithmetic, but whose
shorter proof in second order arithmetic is arbitrarily smaller than
any proof in first order. On the other hand, resolution for higher
order logic can be simulated step by step in a first order narrowing
and resolution method based on deduction modulo, whose paradigm is to
separate deduction and computation to make proofs clearer and shorter.

We prove that $i+1$-th order arithmetic can be linearly simulated into
$i$-th order arithmetic modulo some confluent and terminating rewrite
system. We also show that there exists a speed-up between $i$-th order
arithmetic modulo this system and $i$-th order arithmetic without
modulo.  All this allows us to prove that the speed-up conjectured by
Gödel does not come from the deductive part of the proofs, but can be
expressed as simple computation, therefore justifying the use of
deduction modulo as an efficient first order setting simulating higher
order.

\keywords{proof theory, rewriting, higher order logic, arithmetic}
\end{abstract}

\section{Introduction}

Even if two logical systems are shown to be expressively equivalent,
i.e. they can prove exactly the same formul\ae, they can lead to very
different proofs, in particular in terms of length. For instance, it
is shown that Frege systems have an exponential speed-up over
resolution for propositional logic~\cite{buss87pigeonhole}. However in
mechanized theorem proving, the length of proofs has an importance:
First, computers have limited capacities, and this can lead to a
difference between the practical expressiveness of theoretically
equivalent systems. Even if computing power is always increasing, so
that one is no longer afraid to use SAT-solvers within verification
tools (mainly because worst cases do not often occur in practice), it
is not conceivable to build an automated theorem prover that produces
proofs of non-elementary length. Second, the length of a proof is one
(among others) criterion for defining the quality of a proof. Indeed,
a smaller proof is often more readable and, in the case for instance
of software certification and proof engineering, more communicable and
often also more maintainable. In~\cite{acp,aci}, this notion of ``good
proofs'' is translated through a proof ordering, which of course may
correspond to the comparison of proof lengths.  

Obtaining a speed-up can also have a theoretical interest, because, as
remarked by Parikh in the introductory paragraph of \cite{Godel:86},
``the celebrated P=NP? question can itself be thought of as a speed-up
question.'' (See \cite{cook79relative}.)
All this explains the
research for new formalisms whose deductive systems provide smaller
proofs, such as for instance the calculus of structures
w.r.t. the sequent calculus~\cite{guglielmi04exponential}.

In this
paper, the length of a proof will correspond to its number of steps
(sometimes called lines), whatever the actual size of
the formul\ae\ appearing in them is. Considering only the minimal length of
proofs, the definition of a speed-up is the following:
given some function $h$ over natural numbers, a system
has a speed-up for $h$ over another one, if there exists an infinite set
of formul\ae\ provable in both of them, such that, if  the
length of the proofs in the first system is $l$ and the length in the
second system is $k$, then $k>h(l)$.
\medskip

In 1936, Gödel~\cite{Godel:86} conjectured that there exists
such a speed-up for all recursive functions between $i$-th order and
$i+1$-th order arithmetic, no matter the formal system actually
used. In other words, he stated that for all recursive functions $h$,
it is possible to find an infinite set of formul\ae\ such that, for
each of them, denoted by $P$, if $k$ is the minimal number of steps
in the proofs of $P$ in the $i$-th order arithmetic ($k$ is assumed
to exist, so that $P$ is provable in it), and $l$ is the minimal
number of steps in the proofs of $P$ in the $i+1$-th order
arithmetic, then $k>h(l)$.

This result was proved for first-order arithmetic by
Parikh~\cite{parikh73length}, who actually proved a stronger theorem:
this proof-length speed-up exists in fact also for non-recursive
functions. This was generalized to all orders by Krají\v cek , and was
proved for the true language of arithmetic by Buss~\cite{buss94goedel}
(the former results used an axiomatization of arithmetic using ternary
predicates to represent addition and multiplication). The theorem
proved by Buss is stated as follow:
  \begin{theorem}[{\cite[Theorem 3]{buss94goedel}}]\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 $P\in\mathcal F$, $Z_i\vdash P$
   \item there is a fixed $k\in\mathbb N$ such that for all
     $ P\in\mathcal F$, $Z_{i+1}\lvdash{k\text{ steps}} P$
   \item there is no fixed $k\in\mathbb N$ such that for all
     $ P\in\mathcal F$, ${Z_i\lvdash{k\text{ steps}} P}$.
   \end{enumerate}
  \end{theorem}
\noindent $Z_i$ corresponds to the $i+1$-th order arithmetic (so $Z_0$
is in fact first order arithmetic), and ${Z_i\lvdash{k\text{
      steps}}P}$ means that $P$ can be proved in at most $k$ steps
within a schematic system ---i.e. a Hilbert-type (or Frege) system
with a finite number of axiom schemata and inference rules--- for
$i+1$-th order arithmetic. (In fact, Buss proved this theorem also for
weakly schematic systems, i.e. schematic systems in which every
tautology can be used as an axiom, as well as generalizations of
axioms, but we will not use this fact here.)

Because this theorem is concerned in arithmetic, an intuitive notion
of computation take place in the proofs. Indeed, as remarked by
Poincaré, establishing that $2+2=4$ using the definition of the
addition is just a verification, and not a demonstration, so that in a
proof occur in fact not only pure deduction but also
computation. Therefore, the question arises whether this speed-up
comes from the deductive or the computational part of the proofs, or
both of them. Of course, the difference between computation and
deduction cannot be clearly determined. Because of the Curry-Howard
correspondence, the whole content of the proofs could be considered as
computation.  Here, this difference must be thought of as the
distinction between what is straightforward (at least decidable), and
what must be reasoned out.
\medskip

Deduction modulo \cite{DHK-TPM-JAR} is a presentation of a given logic
---and the formalisms associated with it--- identifying what
corresponds to computation. The computational part of a proof is put
in a congruence between formul\ae\ modulo whom the application of the
deduction rules takes place. This leads to the sequent calculus
modulo and the natural deduction modulo. The congruence is better
represented as a set of rewrite rules that can rewrite terms but also
\emph{atomic propositions}: indeed, one wants for instance to consider
the definition of the addition or multiplication using rewrite rules
over terms as part of the computation, but also the following rewrite
rule:

\noindent$\hfill x\times y = 0~\ra~ x = 0\vee y = 0\hfill$
\smallskip

\noindent which rewrites an atomic
proposition to a formula, so that the following simple proof of
$t\times t = 0$ can be deduced from a proof $\pi$ of $t=0$:
\begin{prooftree}
  \AxiomC{$\pi$}
  \noLine\UnaryInfC{$t=0$}
  \OrI[$t\times t=0~\rewrite~ t = 0\vee t = 0$]$t\times t=0$
\end{prooftree}

Deduction modulo is logically equivalent to the considered
logic~\cite[Proposition 1.8]{DHK-TPM-JAR}, but proofs are often
considered as simpler, because the computation is hidden, letting the
deduction clearly appear. Proofs are also claimed to be smaller for
the same reason. Nevertheless, this fact was never quantified. This
paper answers this issue. Of course, if there are no restriction on
the rewrite rules that are used (for instance if it is allowed to use
a rewrite system semi-deciding the validity of formul\ae), it is not
surprising that the length of the proofs can be unboundedly
reduced. Notwithstanding, we will consider in this paper only very
simple rewrite systems: they will be finite, terminating, confluent
(i.e. deterministic) and linear (variables in the left-hand side only
appear once).

Besides, it is possible, in deduction modulo, to build proofs of
Higher Order Logic using a first order
system~\cite{hollambdasigma}. Using this, a step of higher order
resolution is completely simulated by a step of ENAR, the resolution
and narrowing method based on deduction modulo. Therefore, it seems
reasonable to think that deduction modulo is able to give the same
proof-length speed-ups as the ones occurring between $i+1$-th and
$i$-th order arithmetic. This paper therefore investigates how to
relate proof-length speed-ups in arithmetic with the computational
content of the proofs.
\medskip

To prove that the speed-up theorem of Buss comes from the
computational part of the proofs, we first define a linear translation
between proofs in \mbox{$i$+1-th} order arithmetic and $i$-th order
arithmetic modulo some rewrite system $\R_i$. Second, using this
translation and Buss' theorem, we prove that there is no proof-length
speed-up between $i+1$-th order arithmetic and $i$-th order arithmetic
modulo, whereas there exists such a speed-up between $i$-th order
arithmetic modulo and $i$-th order arithmetic without
modulo. Therefore, we conclude that the speed-up between $i+1$-th
order arithmetic and $i$-th order arithmetic lies in the modulo,
i.e. the computational part of the proofs.
\medskip

In the next section, we will recall the definition of a schematic
system, and we will present such a system for $i$-th order arithmetic.
The section~\ref{sec:dedmod} will define formally what deduction
modulo, and in particular natural deduction modulo consists of. In
Section \ref{sec:trans} we will give the exact translations between a
proof in the schematic system for $i$-th order arithmetic and a proof
in natural deduction, modulo or not, as well as the simulation in
natural deduction of $i+1$-th order arithmetic in $i$-th order
arithmetic modulo. An upper bound of the increase in the length of the
proofs due to these translations will be given. Finally, in Section
\ref{sec:demo} we will use these translations to determine the origin
of the speed-up in arithmetic, and we will conclude about the interest
of working within a first-order system modulo to simulate higher
order. All the details can be found in the full version of this
paper~\cite{burel07unbounded}.

\section{A Schematic System for $i$-th Order Arithmetic}
\subsection{Schematic Systems}

We recall here, using Buss' terminology~\cite{buss94goedel}, what a
schematic system consists in. It is essentially an Hilbert-type (or
Frege) proof system, i.e. valid formul\ae\ are derived from a finite
number of axiom schemata using a finite number of inference
rules. Theorem \ref{theo:buss} is true on condition that proofs are
performed using a schematic system. \medskip

First, we recall how to build many-sorted first order formul\ae,
mainly to introduce the notations we will use.  A (first order)
many-sorted signature consists in a set of function symbols and a set
of predicates, all of them with their arity (and co-arity for function
symbols).  We denote by $\terms\Sigma V$ the set of \Def{terms} built
from a signature $\Sigma$ and a set of variables $V$. An \Def{atomic
  proposition} is given by a predicate symbol $A$ of arity $[\vect i]$
and by $n$ terms $\vect t\in\terms\Sigma V$ with matching sorts. It is
denoted $A(\vect t)$.  \Def{Formul\ae} can be built using the
following grammar\footnote{$\inlinedf$ is used for definitions.}:
$$\mathcal P~\df~\bot~|~A~|~\mathcal P\wedge \mathcal P~|~\mathcal
P\vee \mathcal P~|~\mathcal P\imp \mathcal P~|~\forall x.~\mathcal
P~|~\exists x.~\mathcal P$$ where $A$ ranges over atomic propositions
and $x$ over variables.  $P\Leftrightarrow Q$ will be used as a
syntactic sugar for ${(P\imp Q)\wedge(Q\imp P)}$.  Positions in a term or a formula, free variables
and substitutions are defined as usual (see~\cite{allThat}). The
replacement of a variable $x$ by a term $t$ in a formula $P$ is
denoted by $\subst Ptx$, the restriction of a term or proposition $t$
at the position $\mathfrak p$ by $\subterm t{\mathfrak p}$, and its
replacement in $t$ by a term or proposition $s$ by $\replacement
ts{\mathfrak p}$.
\medskip

Then, given a many-sorted signature of first order logic, we can
consider infinite sets of \Def{metavariables} $\alpha^i$ for each sort
$i$ (which will be substituted by variables), of \Def{term variables}
$\tau^i$ for each sort $i$ (which will be substituted by terms) and
\Def{proposition variables} $A(\vect x)$ for each arity $[\vect i]$
(which will be substituted by formul\ae).

Metaterms are built like terms, except that they can contain
metavariables and term variables. Metaformul\ae\ are built like
formul\ae, except that they can contain proposition variables (which
play the same role as predicates) and\linebreak metaterms.

A \Def{schematic system} is a finite set of inference rules, where an
inference rule is a triple of a finite set of metaformul\ae\ (the \Def{premises}), a
metaformul\ae\ (the \Def{conclusion}), and a set of side conditions of the forms
\emph{$\alpha^j$ is not free in $\Phi$} or \emph{$s$ is freely
  substitutable for $\alpha^j$ in $\Phi$} where $\Phi$ is a
metaformula and $s$ a metaterm of sort $j$. It is denoted by 
\\\AxiomC{$\Phi_1$} \AxiomC{$\cdots$} \AxiomC{$\Phi_n$}
\LeftLabel{\hspace{.3\textwidth}}\RightLabel{$(R)$}
\TrinaryInfC{$\Psi$}\DisplayProof
\\
An inference with an empty set of premises will be called an \Def{axiom schema}.

\subsection{$i$-th Order Arithmetic}


$i$-th order arithmetic ($Z_{i-1}$) is a many-sorted theory with the sorts
$0,\ldots,i-1$ and the signature $$\begin{array}{r@{~:~}l@{~~~~~~~}r@{~:~}l@{~~~~~~~}r@{~:~}l}
0 & 0&
+ & [0; 0]\ra 0&
= & [0;0]\\
s & [0]\ra 0&
\times & [0; 0]\ra 0&
\in^j & [j; j+1]
\end{array}\enspace.$$

The schematic system we use can be found in its totality in the full
version~\cite{burel07unbounded}. The most representative inference
rules are given here as examples:
\medskip

\mysubsubsection{$\mathbf{14+2\times i}$ axiom schemata of classical logic.} We take the one used by
Gentzen~\cite[Chapter 5]{gentzen:untersuchungen} to prove the equivalence of his formalisms with an
Hilbert-type proof system:
\begin{eqnarray}%% \label{eq:I}
%% &A\imp A
%% \\
%% &\bel{eq:K}
%% A\imp B\imp A
%% \\
&\label{eq:Co}(A\imp A\imp B) \imp A \imp B
%% \\&\label{eq:C}
%% (A\imp B\imp C) \imp B\imp A\imp C
\\&\label{eq:T}(A\imp B) \imp (B \imp C) \imp A \imp C
\\&\label{eq:AndLL}(A\wedge B) \imp A
%% \\&\label{eq:AndLR}
%% (A\wedge B) \imp B
%% \\&\label{eq:AndR}
%% (A\imp B) \imp (A\imp C)\imp A \imp (B\wedge C)
%% \\&\label{eq:OrRL}
%% A\imp (A\vee B)
%% \\&\label{eq:OrRR}
%% B\imp (A\vee B)
%% \\&\label{eq:OrL}
%% (A\imp C) \imp (B\imp C) \imp (A\vee B) \imp C
%% \\&\label{eq:AllL}
%% \begin{array}{c}
%% (\forall \alpha^j.~A(\alpha^j)) \imp A(\tau^j)\\
%% \left(\tau^j\text{ is freely substitutable for }\alpha^j\text{ in
%% }A(\alpha^j)\right)
%% \end{array}
\\&\label{eq:ExR}A(\tau^j) \imp \exists \alpha^j.~A(\alpha^j)
&\kern-.7cm\left(\tau^j\text{ is freely substitutable for }\alpha^j\text{ in
}A(\alpha^j)\right)
\\&\label{eq:tnd}A\vee (A\imp\bot)
\end{eqnarray}

\mysubsubsection{$\mathbf{1+2\times i}$ inference rules of classical logic.} Again, we consider
the one of~\cite{gentzen:untersuchungen}:
\begin{equation}\label{eq:mp}
\text{\AxiomC{$A$} \AxiomC{$A\imp B$}
\BinaryInfC{$B$}
\DisplayProof}
\end{equation}
\begin{equation}\label{eq:part}
\text{\AxiomC{$B(\beta^j)\imp A$}
\RightLabel{($\beta^j$ is not free in $(\exists\alpha^j.~B(\alpha^j))\imp A$)}
 \UnaryInfC{$(\exists\alpha^j.~B(\alpha^j))\imp A$}
\DisplayProof}
\end{equation}

\subsubsection{7 identity axiom schemata.} They define the particular relation $=$:
\begin{eqnarray}\label{eq:refl}
&\forall\alpha^0.~ \alpha^0 = \alpha^0
%% \\&\label{eq:cong_s}
%% \forall\alpha^0\beta^0.~\alpha^0=\beta^0\imp s(\alpha^0)=s(\beta^0)
\\&\label{eq:cong_plusl}
\forall\alpha^0\beta^0\gamma^0.~\alpha^0=\beta^0\imp \alpha^0 + \gamma^0=\beta^0+\gamma^0
%% \\&\label{eq:cong_plusr}
%% \forall\alpha^0\beta^0\gamma^0.~\alpha^0=\beta^0\imp \gamma^0+\alpha^0=\gamma^0+\beta^0
%% \\&\label{eq:cong_multl}
%% \forall\alpha^0\beta^0\gamma^0.~\alpha^0=\beta^0\imp \alpha^0 \times \gamma^0=\beta^0\times\gamma^0
%% \\&\label{eq:cong_multr}
%% \forall\alpha^0\beta^0\gamma^0.~\alpha^0=\beta^0\imp \gamma^0\times\alpha^0=\gamma^0\times\beta^0
\\&\label{eq:cong_p}
\forall\alpha^0\beta^0.~\alpha^0=\beta^0\imp A(\alpha^0)\imp A(\beta^0)
\end{eqnarray}

\subsubsection{7 Robinson's axioms.} They are the axioms defining the
function symbols of arithmetic~\cite{tarski53undecidable}:
\begin{eqnarray}%% \label{eq:s_inj}
%% &\forall\alpha^0.~\neg~s(\alpha^0) = 0
%% \\
&\label{eq:s_inv}
\forall\alpha^0\beta^0.~s(\alpha^0)=s(\beta^0)\imp\alpha^0=\beta^0
%% \\&\label{eq:s_surj}
%% \forall\alpha^0.~(\neg~\alpha^0=0)\imp\exists\beta^0.~\alpha^0=s(\beta^0)
%% \\&\label{eq:plus_0}
%% \forall\alpha^0.~\alpha^0+0=\alpha^0
%% \\&\label{eq:plus_s}
%% \forall\alpha^0\beta^0.~\alpha^0+s(\beta^0)=s(\alpha^0+\beta^0)
\\&\label{eq:mult_0}
\forall\alpha^0.~\alpha^0\times 0=0
\\&\label{eq:mult_s}
\forall\alpha^0\beta^0.~\alpha^0\times
s(\beta^0)=\alpha^0\times\beta^0 + \alpha^0
\end{eqnarray}

\subsubsection{$i+1$ induction and comprehension axiom schemata.} 

\begin{equation}\label{eq:ind}
  A(0)\imp\left(\forall\beta^0.~A(\beta^0)\imp
  A(s(\beta^0))\right)\imp \forall \alpha^0.~A(\alpha^0)
\end{equation}
For all $0\leq j<i-1$,
\begin{equation}\label{eq:comp}
\exists\alpha^{j+1}.~\forall\beta^j.~
\beta^j\in^j\alpha^{j+1}\Leftrightarrow A(\beta^j)
\quad(\alpha^{j+1}\text{ is not free in }A)
\end{equation}

From this point on, we will denote by $Z_{i-1}\Hvdash{k} P$ the fact
that there exists a proof of $ P$ of length at most $k$ in this
schematic system, i.e. $P$ can be derived using at most $k$ instances
of these inference rules.

\section{Deduction Modulo}\label{sec:dedmod}

\subsection{Rewriting Formul\ae}
In this section, we recall the definition of deduction modulo, as can
be found in \cite{DHK-TPM-JAR,normalization}.  In deduction modulo,
formul\ae\ are considered modulo some congruence defined by some rules
that rewrite not only terms but also formul\ae. We use standard
definitions, as can be found in \cite{allThat}, and extend them to
proposition rewriting \cite{DHK-TPM-JAR}.

A \Def{term rewrite rule} is the pair of terms $l,r$ such that all
free variables of $r$ appear in $l$. It is denoted $l\rightarrow r$. A
\Def{term rewrite system} is a set of term rewrite rules.  A term $s$
can be rewritten to a term $t$ by a term rewrite rule $l\rightarrow r$
if there exists some substitution $\sigma$ and some position
$\mathfrak p$ in $s$ such that $\sigma l=\subterm s{\mathfrak p}$ and
$t = \replacement s{\sigma r}{\mathfrak p}$.  An atomic proposition
$A(s_1,\ldots,s_i,\ldots,s_n)$ can be rewritten to the atomic
proposition $A(s_1,\ldots,t_i,\ldots,s_n)$ by a term rewrite rule
$l\rightarrow r$ if $s_i$ can be rewritten to $t_i$ by $l\rightarrow
r$. This relation is extended by congruence to all formul\ae.

A \Def{proposition rewrite rule} is the pair of an atomic proposition
$A$ and a formula $P$, such that all free variables of $P$ appear in
$A$. It is denoted $A\rightarrow P$. A \Def{proposition rewrite
  system} is a set of proposition rewrite rules.  A formula $Q$ can be
rewritten to a formula $R$ by a proposition rewrite rule $A\rightarrow
P$ if there exists some substitution $\sigma$ and some position
$\mathfrak p$ in $Q$ such that $\sigma A=\subterm Q{\mathfrak p}$ and
$R =\replacement Q{\sigma P}{\mathfrak p}$. Semantically, this
proposition rewrite relation must be seen as a logical equivalence
between formul\ae.

A \Def{rewrite system} is the union of a term rewrite system and a
proposition rewrite system. The fact that $P$ can be rewritten to $Q$
either by a term or by a proposition rewrite rule of a rewrite system
$\R$ will be denoted by $A\rewrite_\R P$. The transitive
(resp. reflexive transitive) closure of this relation will be denoted
by $\rewrite^*_\R$ (resp. $\sRew^*_\R$).

\subsection{Natural Deduction Modulo}
Using some equivalence $\sRew^*_\R$ defined by a rewrite system $\R$,
we can define natural deduction modulo as in~\cite{normalization}. Its
inference rules are represented in Fig.~\ref{fig:natmod}. They are
the same as the one introduced by
Gentzen~\cite{gentzen:untersuchungen}, except that we work modulo the
rewrite relation. Leaves of a proof that are not introduced by some
inference rules (contrary to $A$ in $\imp$-i for instance) are the
assumptions of the proof. Note that if we do not work modulo, $\imp$-e
is exactly the same as (\ref{eq:mp}).

\begin{figure}[t]
\def\fCenter{\vdash_\R}
\begin{center}
  \begin{tabular*}{\textwidth}{c@{\extracolsep{\fill}}c}
    \atoc$A$$B$
    \ImpI[if $C\sRew_\R^*A\imp B$]$C$
    \DisplayProof
    &
    \AxiomC{$A$}
    \AxiomC{$C$}
    \ImpE[if $C\sRew_\R^*A\imp B$]$B$
    \DisplayProof
    \\\\
    \AxiomC{$A$}
    \AxiomC{$B$}
    \AndI[if $C\sRew_\R^*A\wedge B$]$C$
    \DisplayProof
    &
    \AxiomC{$C$}
    \AndE[if $C\sRew_\R^*A\wedge B$ or $C\sRew_\R^*B\wedge A$]$A$
    \DisplayProof
    \\\\
    \AxiomC{$ A$}
    \OrI[if $C\sRew_\R^*A\vee B$ or $C\sRew_\R^*B\vee A$]$ C$
    \DisplayProof
    &
    \AxiomC{$ C$}
    \atoc$A$$D$
    \atoc$B$$D$
    \OrE[if $C\sRew_\R^*A\vee B$]$ D$
    \DisplayProof
    \\\\
    \AxiomC{$\subst Ayx$}
    \AllI[\parbox{3.5cm}{if $B\sRew_\R^*\forall x.~A$ and $y$ is not
        free in $A$ nor in the
      assumptions of the proof above}]$ B$
    \DisplayProof
    &
    \AxiomC{$ A$}
    \AllE[if $A\sRew_\R^*\forall x.~C$ and $B\sRew_\R^*\subst Ctx$]$ B$
    \DisplayProof
    \\\\
    \AxiomC{$ B$}
    \ExI[if $A\sRew_\R^*\exists x.~C$ and $B\sRew_\R^*\subst Ctx$]$ A$
    \DisplayProof
    &
    \AxiomC{$ B$}
    \atoc$\subst Ayx$$C$
    \ExE[~~~~\lower-1cm\hbox{\parbox{3.cm}{if $B\sRew_\R^*\exists x.~A$ and $y$ is not free in $C$ nor
      in the assumption of the proof above except $\subst Ayx$}}]$ C$
    \DisplayProof
    \\\\    \Tnd[if $A\sRew_\R^*B\vee(B\imp\bot)$]$B$
    \DisplayProof
&
    \AxiomC{$ A$}
    \BotE[if $A\sRew_\R^*\bot$]$ B$
    \DisplayProof
  \end{tabular*}
\end{center}
\caption{Inference Rules of Natural Deduction Modulo.}\label{fig:natmod}
\end{figure}

The length of a proof is the number of inferences used in it. We will
denote by $\mathcal T\Nvdash{k}_\R P$ the fact that there exists a
proof of $ P$ of length at most $k$ using a finite subset of $\mathcal
T$ ($\mathcal T$ can be infinite) as assumptions. In the case where
$\R=\emptyset$, we are back to pure natural deduction, and we will use
$\mathcal T\Nvdash{k} P$. Abusing notations, we will write
$Z_i\Nvdash{k}_\R P$ to say that there is a proof of $ P$ of length at
most $k$ using as assumptions a finite subset of instances of the
axiom schemata~(\ref{eq:refl}) to~(\ref{eq:comp}).

\section{Translations}\label{sec:trans}
\subsection{From $Z_i\Hvdash{}$ to $Z_i\Nvdash{\,}$}\label{sec:HtoN}
We want to translate a proof in the schematic system of $Z_i$ into a
proof in pure natural deduction using as assumptions instances of the
axiom schemata~(\ref{eq:refl}) to~(\ref{eq:comp}).

For the axiom schemata and inference rules of classical logic, we use
the same translation as Gentzen, for instance the axiom schema
(\ref{eq:ExR}) is translated into the natural deduction proof
\\\mbox{}\hspace{4.5cm}
  \Axiomm[i]$A(\tau^j)$
  \ExI$\exists \alpha^j.~A(\alpha^j)$
  \ImpI[(i)]$A(\tau^j)\imp\exists \alpha^j.~A(\alpha^j)$
\DisplayProof\\
and the inference rule (\ref{eq:part}) into 
\\\mbox{}\hfill
  \Axiomm[i]$\exists\alpha^j.~B(\alpha^j)$
  \Axiomm[ii]$B(\beta^j)$
  \AxiomC{$B(\beta^j)\imp A$}
  \ImpE$A$
  \ExE[(ii)]$A$
  \ImpI[(i)]$\exists\alpha^j.~B(\alpha^j)\imp A$
\DisplayProof\hfill\mbox{}

\noindent
 (note that the side condition ensures that it is
possible to consider that what will be substituted for $\beta^j$ is free in
$A$ and the assumptions of the proof above $B(\beta^j)\imp A$).
All these inference rules have a translation whose length does
not depend on the formul\ae\ finally substituted in the proof.

In a schematic system proof, there is also a finite number of
instances of the axioms schemata for identity, Robinson's axioms and
induction and comprehension schemata. We keep these instances as
assumptions in natural deduction, so that we obtain a proof in
natural deduction using as assumptions a finite subset of instances of the
axiom schemata~(\ref{eq:refl}) to~(\ref{eq:comp}), and whose length
is linear compared to the schematic system proof:
\begin{proposition}\label{prop:HtoN}
  It is possible to translate a proof of length $n$ in the schematic
  system for $Z_i$ into a proof of length $\bigO(n)$ in (pure) natural
  deduction using assumptions in $Z_i$.
$$Z_i\Hvdash{k} P~~\leadsto~~Z_i\Nvdash{\bigO(k)} P$$
\end{proposition}

\subsection{From $Z_i\Nvdash{\,}$ to $Z_i\Hvdash{}$}\label{sec:NtoH}
In this section, we consider a proof of $P$ in natural deduction,
using as assumption finite instances of (\ref{eq:refl})
to~(\ref{eq:comp}) in the language of $Z_i$. We translate it into a
proof in the schematic system for $Z_i$.

\newcommand{\T}[2][]{T$_{#1}\left(\text{#2}\right)$}
\newcommand{\MP}{\LeftLabel{(\ref{eq:mp})}\BinaryInfC}


This is essentially a generalization of the translation from the
$\lambda$-calculus to combinatory logic (see
\cite{Curry-et-al-58}). We define mutually recursively two functions
by induction on the inference rules: T transforms a proof of $ P$ in
natural deduction using assumptions $\Gamma$ into a proof of $ P$ in
the schematic system (\ref{eq:Co}) to (\ref{eq:part}) plus
$\Gamma$. T$_A$ transform a proof of $ P$ in natural deduction using
assumptions $\Gamma, A$ into a proof of $A\imp P$ in the schematic
system (\ref{eq:Co}) to (\ref{eq:part}) plus $\Gamma$.

Due to lack of space, the definition of T and T$_A$ is given here only
for the existential quantifier, but can be entirely found in the full version of this paper~\cite{burel07unbounded}.\smallskip

 {\noindent\small\begin{tabular}{@{}r@{}c@{}l@{}}
\T{\AxiomC{$\pi$}
    \noLine\UnaryInfC{$\subst Atx$} \ExI$\exists x.~A$ \DisplayProof}
  &$\df$& \AxiomC{\T{$\pi$}} \noLine\UnaryInfC{$\subst Atx$}
  \Axiomm[\ref{eq:ExR}]$\subst Atx\imp\exists x.~A$ \MP{$\exists
    x.~A$} \DisplayProof\\\\

  \T{\AxiomC{$\pi_1$}
    \noLine\UnaryInfC{$\exists x.~A$}
    \atoc[\pi_2]$\subst Ayx$$B$
    \ExE$B$
    \DisplayProof}&$\df$&
  \AxiomC{\T{$\pi_1$}}
  \noLine\UnaryInfC{$\exists x.~A$}
  \AxiomC{\T[A]{$\pi_2$}}
  \noLine\UnaryInfC{$\subst Ayx\imp B$}
  \LeftLabel{(\ref{eq:part})}
  \UnaryInfC{$(\exists x.~A)\imp B$}
  \MP{$B$}
  \DisplayProof\\\\
  \T[A]{
    \atoc[\pi]$A$$\subst Btx$
    \ExI$\exists x.~B$
    \DisplayProof}&$\df$\\
\multicolumn{3}{r@{}}{\Axiomm[\ref{eq:ExR}]$\subst Btx\imp \exists x.~B$
  \AxiomC{\T[A]{$\pi$}}
  \noLine\UnaryInfC{$A\imp \subst Btx$}
  \Axiomm[\ref{eq:T}]$\cdots%(A\imp \subst Btx)\imp(\subst Btx\imp\exists
  %    x.~B)\imp A\imp \exists x.~B
  $
  \MP{$(\subst Btx\imp \exists x.~B)\imp A\imp \exists x.~B$}
  \MP{$A\imp \exists x.~B$}
  \DisplayProof}\\\\%
  \multicolumn{3}{@{}l}{\T[A]{\atoc[\pi_1]$A$$\exists x.~B$
    \atoc[\pi_2]$A,\subst Byx$$C$
    \ExE$C$
   \DisplayProof}$\df$}\\\multicolumn{3}{r@{}}{
   \AxiomC{\T[\subst Byx]{\begin{tabular}{c}
        \T[A]{$\pi_2$}\\
        $A\imp C$
  \end{tabular}}}
  \noLine\UnaryInfC{$\subst Byx\imp A\imp C$}
  \LeftLabel{(\ref{eq:part})}\UnaryInfC{$\exists x.~B\imp A\imp C$}
  \AxiomC{\T[A]{$\pi_1$}}
  \noLine\UnaryInfC{$A\imp \exists x.~B$}
  \Axiomm[\ref{eq:T}]$\cdots%(A\imp \exists x.~B)\imp (\exists x.~B\imp A\imp C)\imp
  % A\imp A\imp C
  $   
  \MP{$(\exists x.~B\imp A\imp C)\imp
    A\imp A\imp C$}
  \MP{$A\imp A\imp C$}
  \Axiomm[\ref{eq:Co}]$\cdots%(A\imp A\imp C)\imp A\imp C
  $
  \MP{$A\imp C$}
  \DisplayProof}\\\\
\end{tabular}}

It can be verified that this definition transforms a proof of size $n$
into a proof of size $\bigO(3^n)$. Due to 
\cite[Corollary~3.4]{cook79relative}, we could have found, at least for the
propositional part, a polynomial translation. Nevertheless all we need
in this paper is the fact that the increase of the
proof length in the translation is bounded.

\begin{proposition}\label{prop:NtoH}
  It is possible to translate a proof of length $n$ in the (pure) natural
  deduction using assumptions in $Z_i$ into a proof of length $\bigO(3^n)$ in the schematic
  system for $Z_i$.
$$Z_i\Nvdash{k} P~~\leadsto~~Z_i\Hvdash{\bigO(3^k)} P$$
\end{proposition}

\subsection{From $Z_{i+1}\Hvdash{}$ and $Z_{i+1}\Nvdash{}$ to $Z_i\Nvdash{\,}_{\R_i}$}\label{sec:HtoNRi}
This time, we translate a proof in the schematic system for $Z_{i+1}$
into a proof in natural deduction modulo using as assumption instances
of the axiom schemata (\ref{eq:refl}) to~(\ref{eq:comp}), but in the
language of $Z_i$. The point is that, using modulo, it is possible to
downshift an order.

\newcommand{\inc}{~\upepsilon~}
\newcommand{\inlineinc}{\upepsilon}
 We follow the translation of
Section~\ref{sec:HtoN}, except for the axiom schemata
(\ref{eq:cong_p}), (\ref{eq:ind}) and (\ref{eq:comp}) that are
instantiated by formul\ae\ that are in the language of $Z_{i+1}$ but
not in the language of $Z_i$. To translate these schemata, we will use
the work of F. Kirchner~\cite{fk:classes06} which permits to express
first-order theories using a finite number of axioms. The idea is to
transform some metaformula $A(\vect t)$ used in an axiom schema into a
formula of the form $\langle\vect t\rangle\inc\gamma$ where $\gamma$
will be some term representing what formula will be actually
substituted for $A$.

Following F. Kirchner's method, we add new sorts $\ell$ for lists and
$c$ for classes, as well as new function symbols and predicate 
\begin{center}
$\begin{array}{r@{~:~}l}
    1^j & j\\
    S^j & [j]\ra j\\
    \cdot[\cdot]^j & [j; \ell]\ra j\\
  \end{array}\hfill
  \begin{array}{r@{~:~}l}nil & \ell\\
::^j & [j;\ell]\ra\ell\\
    \doteq & [0;0]\ra c\\
    \dot{\in}^j & [j;j+1]\ra c\\
  \end{array}\hfill
  \begin{array}{r@{~:~}l}\cup & [c;c]\ra c\\
    \cap & [c;c]\ra c\\
    \supset & [c;c]\ra c\\
  \end{array}\hfill
  \begin{array}{r@{~:~}l}\emptyset & c\\
    \mathcal P^j & [c]\ra c\\
    \mathcal C^j & [c]\ra c\\
    \inlineinc & [\ell;c]
  \end{array}\enspace.$
\end{center}
$\langle\vect\alpha\rangle$ will be syntactic
sugar for ${\alpha_1::^{j_1}\cdots::\alpha_n::^{j_n}nil}$
for the appropriate $j_m$. We change the axiom schemata
(\ref{eq:cong_p}), (\ref{eq:ind}) and (\ref{eq:comp}) into the
following \emph{axioms}:
\begin{eqnarray}\label{eq:cong_p_c}&
\forall\gamma^c.~\forall\alpha^0\beta^0.~\alpha^0=\beta^0\imp \langle\alpha^0\rangle\inc\gamma^c\imp\langle\beta^0\rangle\inc\gamma^c
\\&\label{eq:ind_c}
    \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
\end{eqnarray}
For all $0\leq j<i$,
\begin{equation}\label{eq:comp_c}
\forall\gamma^c.~\exists\alpha^{j+1}.~\forall\beta^j.~
\beta^j\in^j\alpha^{j+1}\Leftrightarrow \langle\beta^j\rangle\inc\gamma^c
\end{equation}

The rewrite system $\R_i$ is then the following:
\begin{center}
 $\hfill \begin{array}{r@{~\ra~}l}t[nil]^j& t\\
    1^j[t::^jl]^j& t\\
    S^j(n)[t::^jl]^j& 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\\
    l\inc\doteq(t_1,t_2)& t_1[l]^0 = t_2[l]^0\\
  \end{array}\hfill\hfill
  \begin{array}{r@{~\ra~}l}
    l\inc{\dot{\in}}^j(t_1,t_2)& t_1[l]^j \in^j t_2[l]^{j+1}\\
    l\inc A\cup B& 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\\
    l\inc \emptyset& \bot\\
    l\inc \mathcal P^j(A)& \exists x.~x::^jl\inc A\\
    l\inc \mathcal C^j(A)& \forall x.~x::^jl\inc A
  \end{array}\hfill$
\end{center}
Note that this system is finite, terminating
(either the size of a list decreases, or else a $\cdot[\cdot]$ or an
$\inlineinc$ goes more inside or disappears), confluent (the only
critical pairs, of the form: $f(\vect
t)\mathop{\longleftarrow}\limits_{\R_i} f(\vect t)[nil]\rewrite_{\R_i}
f(t_1[nil],\ldots,t_n[nil])$, are easily joinable), and linear
(variables appears only once in the left hand side of the rewrite
rules).

Proposition 2 of \cite{fk:classes06} says that it is possible, for any
formula $P$ of the language of $i$-th order arithmetic, to
prove $\exists E.~\forall x_1\cdots x_n.~\langle\vect x\rangle\inc
E\Leftrightarrow P$. Moreover, the proof of this proposition shows us
how to construct the witness $E$. We will denote it by $E_P^{\vect
  x}$. Then, one can prove that $\langle \vect t\rangle\inc E_P^{\vect
  x}\linebreak\rewrite_{\R_i}^*\{t_1/x_1,\ldots, t_n/x_n\}P$. For instance, consider
the formula ${x = 0\vee\exists y.~x \in^0y}$, which will be denoted by
$P$. Then $E_P^x$ equals
$\doteq(1,S(0))~\cup~\mathcal P^1\left(\dot{\in}^0(S(1),1)\right)$ and
$\langle t\rangle\inc
E_P^x$ can be rewritten to $t = 0\vee\exists x.~t\in^0x$.

Consequently, the axiom schemata (\ref{eq:cong_p}), (\ref{eq:ind}) and
(\ref{eq:comp}) for formul\ae\ of the language of $Z_{i+1}$ but not in
the language of $Z_i$ are replaced by the proofs in
Fig.~\ref{fig:transc}.  In these translations, we need to
instantiate $\gamma^c$ with some $E_A^x$. It is well-known that the
instantiations are the most problematic rules in deductive systems, at
least for automated provers (e.g. they are what leads to
nondeterminism and/or nontermination of tableaux methods for first
order logic), because the instantiated term must be somehow
guessed. Nevertheless, the instantiation here is entirely and
automatically determined by the formula used in the schema, so that no
harm is done.

\begin{figure}[t]
\def\fCenter{\vdash_{\R_i}}
  \begin{prooftree}
    \Axiomm[\ref{eq:cong_p_c}]$\forall\gamma^c.~\forall\alpha^0\beta^0.~\alpha^0=\beta^0\imp \langle\alpha^0\rangle\inc\gamma^c\imp\langle\beta^0\rangle\inc\gamma^c$
    \AllE[$
      \begin{array}{l}
        \langle\alpha^0\rangle\inc
        E_A^{x}\imp\langle\beta^0\rangle\inc
        E_A^{x}\\\rewrite_{\R_i}^*A(\alpha^0)\imp A(\beta^0)
      \end{array}
      $]$\forall\alpha^0\beta^0.~\alpha^0=\beta^0\imp
    A(\alpha^0)\imp A(\beta^0)$
  \end{prooftree}

  \begin{prooftree}
    \Axiomm[\ref{eq:ind_c}]$\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[$\begin{array}{l}
      \text{for all $t$, }\\\langle t\rangle\inc E_A^x\\\rewrite_{\R_i}^*A(t)
      \end{array}
      $]$A(0)\imp\left(\forall\beta^0.~A(\beta^0)\imp
    A(s(\beta^0))\right)\imp \forall \alpha^0.~A(\alpha^0)$
  \end{prooftree}

  \begin{prooftree}
    \Axiomm[\ref{eq:comp_c}]$\forall\gamma^c.~\exists\alpha^{j+1}.~\forall\beta^j.~
    \beta^j\in^j\alpha^{j+1}\Leftrightarrow \langle\beta^j\rangle\inc\gamma^c$
    \AllE[$\langle\beta^j\rangle\inc E_A^x\rewrite_{\R_i}^*A(\beta^j)$]$\exists\alpha^{j+1}.~\forall\beta^j.~
    \beta^j\in^j\alpha^{j+1}\Leftrightarrow A(\beta^j)$
  \end{prooftree}
\caption{Translations of the axiom schemata (\ref{eq:cong_p}), (\ref{eq:ind}) and
(\ref{eq:comp}).}\label{fig:transc} 
\end{figure}

Using this, a proof in the schematic system for $Z_{i+1}$ can be
translated into a proof of $P$ in natural deduction modulo $\R_i$
using as assumptions the axioms (\ref{eq:cong_p}), (\ref{eq:ind}) and
(\ref{eq:comp}) as well as a finite subset of instances the axiom
schemata~(\ref{eq:refl}) to~(\ref{eq:comp}) for $i$-th order
arithmetic, and whose length is linear compared to the schematic
system proof:
\begin{proposition}\label{prop:HtoNRi}
  It is possible to translate a proof of length $n$ in the schematic
  system for $Z_{i+1}$ into a proof of length $\bigO(n)$ in the natural
  deduction modulo $\R_i$ using assumptions in
  $Z_i$, (\ref{eq:cong_p_c}), (\ref{eq:ind_c}) and (\ref{eq:comp_c}).
$$Z_{i+1}\Hvdash{k}P~~\leadsto~~Z_i,(\ref{eq:cong_p_c}),(\ref{eq:ind_c}),(\ref{eq:comp_c})\Nvdash{\bigO(k)}_{\R_i}P$$
\end{proposition}

This result can also be stated entirely in natural deduction
\begin{theorem}\label{theo:s3}
For all $i\geq 0$, there exists a (finite) 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{\bigO(k)}_{\R_i} P$.
  \end{theorem}
\begin{proof}
  Let $\Gamma$ be
  $\{(\ref{eq:cong_p_c}),(\ref{eq:ind_c}),(\ref{eq:comp_c})\}$.  We
  replace the instance of the axiom schemata (\ref{eq:cong_p}),
  (\ref{eq:ind}) and (\ref{eq:comp}) by the axioms
  (\ref{eq:cong_p_c}), (\ref{eq:ind_c}) and(\ref{eq:comp_c}) as
  indicated in Fig.~\ref{fig:transc}.\qed
\end{proof}

Note that, contrarily to HOL-$\lambda\sigma$ which permits to simulate
Higher Order Logic, the rewrite system purposed here is finite and
terminating.

The fact to add the finite set of axioms $\Gamma$ could be seen as
some deceit, because we do not work really in $Z_i$, but in a theory
strictly stronger. By the way, due to Theorem~\ref{theo:s3}, it is
possible to prove the consistency of $Z_i$ in $Z_i,\Gamma$ modulo
$\R_i$. Nevertheless, the point here is that it is possible, by
working modulo $\R_i$, to simulate $Z_{i+1}$ using a finite set of
axioms, and not axiom schemata, without exploding the length of the
proofs.  If we were not working modulo this rewrite system, but using
a finite theory compatible with it (i.e. proving exactly the same
formul\ae), then it would not be possible to give a bound to
the translation:
\begin{proposition}
For all $i\geq 0$, for all finite theories $T_i$ compatible with $\R_i$,
there is an infinite family $\mathcal F$ such that 
   \begin{enumerate}
   \item for all $ P\in\mathcal F$, $Z_i,\Gamma,T_i\Hvdash{\,} P$
   \item there is a fixed $k\in\mathbb N$ such that for all
     $ P\in\mathcal F$, ${Z_{i+1}\Hvdash{k\text{ steps}} P}$
   \item there is no fixed $k\in\mathbb N$ such that for all
     $ P\in\mathcal F$, ${Z_i,\Gamma,T_i\Hvdash{k\text{ steps}} P}$.
   \end{enumerate}
\end{proposition}


It could also have been possible to translate the formul\ae\ that one
wants to prove, as is done in~\cite{arith}, where a formula of first
order arithmetic is transformed by adding the information that some
variable $n$ is an integer using some predicate $N(n)$ which can be
rewritten into an axiom corresponding to the induction schema for
first order arithmetic. Here, $P$ could be translated into
$(\ref{eq:cong_p_c})\imp(\ref{eq:ind_c})\imp(\ref{eq:comp_c})\imp P$. 


\section{Application to Speed-ups in Arithmetic}\label{sec:demo}

\subsection{Bypassing Buss' Speed-up using Modulo}\label{sec:demo3}
The goal of this section is to prove that one can work in $Z_i$
modulo some rewrite system $\R_i$ to be able to build proof as small
as the one of $Z_{i+1}$. Indeed, Theorem~\ref{theo:s3} permits to show
that G\"odel's
theorem does not extend if one works modulo $\R_i$ (what is formulated here in
a positive way):
  \begin{corollary}[of Theorem~\ref{theo:s3}]%
\label{theo:3}
For all $i\geq 0$, there exists a (finite) rewrite system $\R_i$ and a
finite set of axioms $\Gamma$ such that
for all infinite family $\mathcal F$ of
   $\prod_1^0$-formul\ae, if
\begin{itemize}
\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+1}\Nvdash{k\text{ steps}} P$
\end{itemize}
then there is a fixed $k'\in\mathbb N$ such that for all
  $ P\in\mathcal F$, $Z_i,\Gamma\Nvdash{k'\text{ steps}}_{\R_i} P$.
  \end{corollary}



\subsection{Speed-up Due to Computation}\label{sec:demo2}
On the contrary, we want to show that it is possible to achieve the
same speed-up as the one between $i$-th order and $i+1$-th order
arithmetic just by working modulo some rewrite system in $i$-th order
arithmetic:

\begin{theorem}\label{theo:2}For all $i\geq 0$, there is a 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}
\begin{proof}
  The rewrite system $\R_i$ is the one defined in
  Section~\ref{sec:HtoNRi}. Let $\mathcal F$ be the family of
  formul\ae\ obtained by Theorem~\ref{theo:buss}. Let
  $\mathcal F' \df
 \{{(\ref{eq:cong_p_c})\imp(\ref{eq:ind_c})\imp(\ref{eq:comp_c})\imp P}~:
 P\in\mathcal F\}$. Then:
  \begin{enumerate}
  \item For all $ P'\in\mathcal F'$, $Z_i\Nvdash{\,} P'$: we know that
    $Z_i\Hvdash{} P$, therefore using Proposition~\ref{prop:HtoN},
    $Z_i\Nvdash{\,} P$ and, adding to this proof $2+i$ times $\imp$-i,
    $Z_i\Nvdash{\,} P'$.
  \item There is a $k$ such that for all $ P'\in\mathcal F'$, $Z_i\Nvdash{k}_{\R_i} P'$:
    there exists some
  $k$ such that for all $ P\in\mathcal F$,
  $Z_{i+1}\Hvdash{k} P$. Using Proposition~\ref{prop:HtoNRi}, there exists
  some $K$ such that for all $ {P\in\mathcal F}$, we have
  $Z_i,(\ref{eq:cong_p_c}),(\ref{eq:ind_c}),(\ref{eq:comp_c})\Hvdash{K}_{\R_i}P$
  and one can add $2+i$ times $\imp$-i to
    obtain a proof of $ P'$.
  \item There is no $k$ such that for all $ P'\in\mathcal F'$,
    $Z_i\Nvdash{k} P'$: Suppose by contradiction that there is a $k$
    such that for all $ P'\in\mathcal F'$, $Z_i\Nvdash{k} P'$,
    then using $2+i$ times $\imp$-e, we have
    $Z_i,(\ref{eq:cong_p_c}),(\ref{eq:ind_c}),(\ref{eq:comp_c})\Nvdash{k+2+i} P$. But
    (\ref{eq:cong_p_c}), (\ref{eq:ind_c}) and (\ref{eq:comp_c}) use
    function symbols not appearing in $ P$ nor $Z_i$ (for instance
    $\inlineinc$). Therefore they cannot be used in a proof of $ P$ in
    $Z_i$, so that in fact $Z_i\Nvdash{k+2+i} P$. Then, using
    Proposition~\ref{prop:NtoH}, $Z_i\Hvdash{\bigO(3^k)} P$, and that
    will be in contradiction with the fact that there is no $K$ such
    that for all $ P$, $Z_i\Hvdash{K} P$.
  \end{enumerate}
Schematically, 
$$
\renewcommand{\arraystretch}{1.5}
  \begin{array}[b]{ccccl}
Z_{i+1}\Hvdash{k} P
& \mathop{\leadsto}\limits^{\text{Prop.~\ref{prop:HtoNRi}}} 
& Z_i,(\ref{eq:cong_p_c}),(\ref{eq:ind_c}),(\ref{eq:comp_c})\Nvdash{K}_{\R_i} P  
& \leadsto
& Z_i\Nvdash{K+2+i}_{\R_i} P' \\

\text{\scriptsize Theo.~\ref{theo:buss}}\updownarrow\\
 
Z_i\Hvdash{\not{3^k}} P
& 
\renewcommand{\arraystretch}{.2}
\begin{array}[t]{c}
\mathop{\leadsto}\limits^{\text{Prop.~\ref{prop:HtoN}}} \\
\mathop{\leadsfrom}\limits_{\text{Prop.~\ref{prop:NtoH}}} \\
\end{array}
& Z_i,(\ref{eq:cong_p_c}),(\ref{eq:ind_c}),(\ref{eq:comp_c})\Nvdash{\not k} P  
& \leadsto
& Z_i\Nvdash{\not k} P' \\
  \end{array}~~~~~~~~~~\qed$$
\end{proof}

Note that it is possible to get speed-ups in deduction modulo w.r.t
pure natural deduction with
systems much more simpler than for higher order arithmetic. (Take for
instance the rule $s(x)+y\ra x+s(y)$ and consider the
formul\ae\ $\underline n
+\underline n = \underline{n+n}$ where $\underline{n}$ denotes the
usual representation of the natural number $n$ using $0$ and $s$, for
all natural numbers $n$.)\@ Our last result however, combined with
Corollary~\ref{theo:3}, permits to conclude that proof-length
speed-ups \emph{in arithmetic} result from the computational part of the
proofs, which is expressed by the rewrite systems $\R_i$.

\section{Conclusion and Perspectives}

We have first proved that it is possible to use some rewrite system to
simulate the difference between $i$-th and $i+1$-th order arithmetic
at the condition to add three extra axioms which replace the missing
axiom schemata. This simulation is linear in terms of proof length,
which permits to prove that there is no proof-length speed-up between
$i+1$-th order arithmetic and its simulation, on the contrary to
without modulo as it is expressed in Buss' theorem.
Furthermore, this simulation allows to get the same proof speed-up for
deduction modulo over non modulo systems than the one of Buss'
theorem. Together with the first result, this proves that the gap
between $i$-th and $i+1$-th order arithmetic is in fact due to the
computational part of the proofs. In this particular case, we also
clearly identify the computation occurring in the proofs with a
finite, terminating and confluent (so, in a sense, deterministic)
rewrite system. This is not surprising, because, if one looks
carefully, the proof of Theorem~\ref{theo:buss} given by Buss in
\cite{buss94goedel} deeply relies on the fact that it is possible to
define some truth predicate for the formul\ae\ of the preceding
order. Therefore, in a sense, it is possible, in $i+1$-th order
arithmetic, to compute the validity of a formula in $i$-th order
arithmetic.\medskip

Speed-ups in deduction modulo must not be
considered as cheating, by hiding part of the proofs in the
congruence. This must be thought of as a way to separate what is
deduced and what is computed. To find a proof, both parts need to be
built. To check the proof however, only the deductive part is
necessary, because the rest can be effectively computed during the
verification (hence the need to have a decidable congruence, even
better if it is determined by simple deterministic algorithm). This can be
applied to automated and interactive theorem proving, as well as in
representation of proofs in natural language (where all computational
details are often implicitly left the reader).

These results are encouraging indicators that it is as good to work
directly in higher order logics, as is done in the current interactive
theorem provers, such as Coq~\cite{Coq} or
Isabelle/HOL~\cite{Nipkow-Paulson-Wenzel:2002}, or using a first order
implementation of these logics, as could be done in a proof assistant
based on deduction modulo (or on its sequel named
superdeduction, see~\cite{BraunerHK07}). This paper gives clues to answer
positively this question, although we were interested in the step
between $i$-th order and $i+1$-th order arithmetic, and not between
first order and higher order logic. The fact that higher order
resolution can be simulated step by step by ENAR~\cite{hollambdasigma}
is not a solution, because there may exist some other higher order
proof system that produce proofs that cannot be conveniently
translated in a first order system modulo. So, our next challenge will
be, starting from the current results, to investigate how exactly
higher order logic prevails or not over first order logic, by studying
more closely the simulation of higher order logic.

A first direction to do so will be to prove that it is possible to
apply transitivity between the simulation of $Z_{i+1}$ in $Z_i$ and
the one of $Z_{i+2}$ in $Z_{i+1}$, in order to get a simulation of
$Z_{i+2}$ in $Z_i$, for instance by combining $\R_i$ and
$\R_{i+1}$. In addition to the expression of first order arithmetic as
a theory modulo~\cite{arith}, this would lead to the linear simulation of
higher order arithmetic entirely as a theory modulo. It should however
be noted that one of the main advantage of our rewrite systems
w.r.t. HOL-$\lambda\sigma$, i.e. its finiteness, will be lost because
of the need for a rule to decompose ${\dot{\in}}^i$ for all orders $i$.

Another direction would be to look directly at the difference of the
lengths of proofs in the expression of HOL in the sequent calculus
modulo~\cite{hollambdasigma}, or of every PTS in $\lambda\Pi$
modulo~\cite{CousineauDowek}.

\subsubsection{Acknowledgments.} The author wishes to thank
  G.~Dowek, T.~Hardin, C.~Kir\-chner and the anonymous referees for many
  discussions and comments about this paper.

\begin{thebibliography}{10}

\bibitem{allThat}
Baader, F., Nipkow, T.:
\newblock Term \emph{Re}writing and \emph{all That\/}.
\newblock CUP (1998)

\bibitem{aci}
Bonacina, M.P., Dershowitz, N.:
\newblock Abstract canonical inference.
\newblock ACM Trans. Comput. Logic \textbf{8} (2007)

\bibitem{BraunerHK07}
Brauner, P., Houtmann, C., Kirchner, C.:
\newblock Principles of superdeduction.
\newblock In: LICS. IEEE Computer Society (2007) To appear.

\bibitem{burel07unbounded}
Burel, G.:
\newblock Unbounded proof-length speed-up in deduction modulo.
\newblock Research report (2007) Available at
  \url{http://hal.inria.fr/inria-00138195}.

\bibitem{buss87pigeonhole}
Buss, S.R.:
\newblock Polynomial size proofs of the propositional pigeonhole principle.
\newblock The Journal of Symbolic Logic \textbf{52} (1987)  916--927

\bibitem{buss94goedel}
Buss, S.R.:
\newblock On {G\"o}del's theorems on lengths of proofs {I}: Number of lines and
  speedup for arithmetics.
\newblock The Journal of Symbolic Logic \textbf{59} (1994)  737--756

\bibitem{cook79relative}
Cook, S.A., Reckhow, R.A.:
\newblock The relative efficiency of propositional proof systems.
\newblock The Journal of Symbolic Logic \textbf{44} (1979)  36--50

\bibitem{CousineauDowek}
Cousineau, D., Dowek, G.:
\newblock Embedding pure type systems in the lambda-pi-calculus modulo.
\newblock In: TLCA. (2007) To appear.

\bibitem{Curry-et-al-58}
Curry, H.B., Feys, R., Craig, W.:
\newblock Combinatory Logic. Vol.~1.
\newblock Elsevier Science Publishers B. V. (North-Holland), Amsterdam (1958)

\bibitem{acp}
Dershowitz, N., Kirchner, C.:
\newblock Abstract {C}anonical {P}resentations.
\newblock Theoretical Computer Science \textbf{357} (2006)  53--69

\bibitem{hollambdasigma}
Dowek, G., Hardin, T., Kirchner, C.:
\newblock {HOL-$\lambda \sigma$} an intentional first-order expression of
  higher-order logic.
\newblock Math. Structures Comput. Sci. \textbf{11} (2001)  1--25

\bibitem{DHK-TPM-JAR}
Dowek, G., Hardin, T., Kirchner, C.:
\newblock Theorem proving modulo.
\newblock Journal of Automated Reasoning \textbf{31} (2003)  33--72

\bibitem{normalization}
Dowek, G., Werner, B.:
\newblock Proof normalization modulo.
\newblock The Journal of Symbolic Logic \textbf{68} (2003)  1289--1316

\bibitem{arith}
Dowek, G., Werner, B.:
\newblock Arithmetic as a theory modulo.
\newblock In: Giesl, J. (ed.): RTA. Lecture Notes in Computer Science, Vol.
  3467. Springer-Verlag (2005)  423--437

\bibitem{gentzen:untersuchungen}
Gentzen, G.:
\newblock Untersuchungen {{\"u}ber} das logische {Schliessen}.
\newblock Mathematische Zeitschrift \textbf{39} (1934)  176--210, 405--431
  Translated in: Szabo, M.E. (ed.): {\em The Collected Papers of Gerhard
  Gentzen} as ``Investigations into Logical Deduction''.

\bibitem{Godel:86}
G{\"o}del, K.:
\newblock On the length of proofs.
\newblock In: Feferman, S.,  et~al. (eds.): Kurt G{\"o}del: Collected Works.
  Vol.~1.
\newblock Oxford University Press, Oxford (1986)  396--399

\bibitem{guglielmi04exponential}
Guglielmi, A.:
\newblock Polynomial size deep-inference proofs instead of exponential size
  shallow-inference proofs.
\newblock Av. at {\url{http://cs.bath.ac.uk/ag/p/AG12.pdf}} (2004)

\bibitem{fk:classes06}
Kirchner, F.:
\newblock A finite first-order theory of classes.
\newblock Available at
  {\url{http://www.lix.polytechnique.fr/Labo/Florent.Kirchner/doc/fotc2006.pdf%
  }} (2006)

\bibitem{tarski53undecidable}
Mostowski, A., Robinson, R.M., Tarski, A.:
\newblock Undecidable Theories.
\newblock Studies in Logic and the Foundations of Mathematics. North-Holland,
  Amsterdam (1953)

\bibitem{Nipkow-Paulson-Wenzel:2002}
Nipkow, T., Paulson, L.C., Wenzel, M.:
\newblock Isabelle/HOL --- A Proof Assistant for Higher-Order Logic. LNCS, Vol.
  2283.
\newblock Springer (2002)

\bibitem{parikh73length}
Parikh, R.J.:
\newblock Some results on the length of proofs.
\newblock Transactions of the ACM \textbf{177} (1973)  29--36

\bibitem{Coq}
{The {Coq} Development Team}:
\newblock The {Coq} Proof Assistant Reference Manual.
\newblock INRIA. (2006) Version 8.0, available at
  {\url{http://coq.inria.fr/doc/main.html}}.

\end{thebibliography}

\end{document}
