\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