1–LABEL:LastPageApr. 07, 2017Apr. 13, 2018

# Some observations on the logical foundations of inductive theorem proving

Stefan Hetzl  Institute of Discrete Mathematics and Geometry
Vienna University of Technology
Wiedner Hauptstraße 8–10
AT-1040 Vienna
Austria<EMAIL_ADDRESS>and  Tin Lok Wong  Kurt Gödel Research
Center for Mathematical Logic
University of Vienna
Währinger Straße 25
AT-1090 Vienna
Austria<EMAIL_ADDRESS>
###### Abstract.

In this paper we study the logical foundations of automated inductive theorem
proving. To that aim we first develop a theoretical model that is centered
around the difficulty of finding induction axioms which are sufficient for
proving a goal.

Based on this model, we then analyze the following aspects: the choice of a
proof shape, the choice of an induction rule and the language of the induction
formula. In particular, using model-theoretic techniques, we clarify the
relationship between notions of inductiveness that have been considered in the
literature on automated inductive theorem proving.

This is a corrected version of the paper https://arxiv.org/abs/1704.01930v5
published originally on Nov. 16, 2017.

###### Key words and phrases:

inductive theorem proving, arithmetical theories, proof theory

Supported by the Vienna Science and Technology Fund (WWTF) project VRG12-004

Supported by Austrian Science Fund (FWF) project P24654-N25

##  1\. Introduction

Theories of (natural number) arithmetic have been of great interest to
mathematical logicians since the beginning of the 20th century. At that time,
work was mainly devoted to questions of consistency. Deep connections that
link the definability-theoretic aspects of arithmetic and theories of
computation were later discovered and fruitfully developed. In the 1970s and
80s, relevant model-theoretic techniques became mature enough for establishing
mathematically interesting unprovability results. While the model theory of
arithmetic evolved into a subject of its own, the connections with theories of
computation found their way down to the complexity-theoretic level. Nowadays,
theories of arithmetic have penetrated almost every branch of mathematical
logic, including mathematical philosophy.

Rather independently of this work, the subject of inductive theorem proving
developed in computer science. In this tradition, the central aim is to
develop algorithms that find proofs by induction and to implement these
algorithms efficiently. This subject is characterized by a great variety of
different methods (and systems implementing these methods), for example,
rippling [BBHI05], theory exploration [CJRS13], integration into a
superposition prover [KP13, Cru15, WW], recursion analysis [BM79, Ste88,
BvHH+89], proof by consistency [Com01], and cyclic proofs [BS11, BGP12].
Recently, a benchmark suite for inductive theorem proving has been presented
[CJRS15].

The aim of our work is to apply methods and results from the former tradition
in mathematical logic to the tradition in computer science. The main advantage
of this combination is that it is possible to obtain unprovability results (by
model-theoretic means) where previously in the literature on inductive theorem
proving only empirical observations could be made based on the failure of a
specific algorithm to find a proof.

A first obstacle in realizing such an application is that the above mentioned
approaches to inductive theorem proving are quite different. This makes it
difficult to provide a common theoretical basis. However, the final result is
typically, in one way or another, explicitly or implicitly, a proof of the
goal from instances of an induction scheme and basic axioms from a background
theory. We take this observation as a guiding principle for the development of
a theoretical model of inductive theorem proving in Section 2. This is the
main conceptual contribution of this paper.

In terms of technical contributions we analyze the following aspects of
methods for inductive theorem proving: (a) the choice of a proof shape, (b)
the choice of the induction rule, and (c) the language of the induction
formula. Despite the differences between the existing methods for inductive
theorem proving, these aspects play a role in most of them. Mathematically,
the technical contributions of this paper are: we show that the equivalence
proof shape for inductive proofs (see Section 3) is complete but that the
uniform proof shape is not. We show that Walther’s method for comparing
induction axioms [Wal92] is not complete (Section 4.3). We make the (possibly
surprising) observation that the weakest induction axiom for proving an
induction axiom may not be that induction axiom itself (Proposition 21). We
establish the strictness of the implications between several frequently used
notions of inductiveness (Section 7). We also include the result, due to Kaye,
that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
proves the least number principle in the language of rings (Theorem 28).

This paper is structured as follows: after developing our model of inductive
theorem proving in Section 2, we study the completeness of proof shapes in
Section 3. In Section 4 we describe different formulations of induction and
study their equivalence in both a general and a quantifier-free context. In
Section 5 we establish non-closure properties of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$-cuts
that will be used in the rest of the paper. In Section 6 we investigate two
ways of comparing different induction formulas that prove the same theorem. In
Section 7, which is central to this paper, we compare different notions of
inductiveness. (A formula is called inductive in the sense of a particular
induction rule if it satisfies the hypotheses of this rule provably in the
base theory.) In Section 8 we study the effect of the choice of the language
for the induction formula using an example involving the $<$-relation.

This is a corrected version of the paper https://arxiv.org/abs/1704.01930v5
published originally on Nov. 16, 2017. As Emil Jeřábek pointed out, two
questions posed in the original version already had answers in the literature,
and Shepherdson almost proved the main result of Section 8. The answers to
these questions are incorporated in this paper as Theorem 16 and Theorem 29,
and we added attribution to Shepherdson’s work in Section 8.

##  2\. A theoretical model of inductive theorem proving

This section is devoted to developing a theoretical model of inductive theorem
proving. This is necessary in order to provide a conceptually and formally
clear basis for relating mathematical results to algorithms in automated
deduction.

###  2.1. First-order theories of the natural numbers

In this paper we restrict our attention to first-order theories of the natural
numbers (as opposed to, e.g., general inductive data types which is a more
common choice in inductive theorem proving). This is a pragmatic choice which
is motivated by the following reasons: (1) the mathematical study of these
theories is very well developed, and (2) the central problems of inductive
theorem proving also surface in this restricted setting. To the mathematical
logician this may not seem a restriction since coding allows us to describe an
arbitrary inductive data type as a set of natural numbers. However, the
increase of the syntactic complexity of formulas and proofs based on coding
renders this approach unfit for practical applications, where bounded
quantifiers are usually as costly as unbounded quantifiers.

Throughout this paper, we work over the base theory
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
It is finitely axiomatized, induction-free, and a fragment of Peano arithmetic
($\mathrm{PA}$). Robinson’s $Q$ is another commonly used base theory for
arithmetic. There are two main reasons for choosing
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
instead of $Q$ as the base theory in this paper. First, if one adopts $Q$ as
the base theory, then even a slight change in the definitions can make a
significant difference in the results. This is due to the fact that many
simple arithmetic properties, for example,

$\forall{x,y}\ {(x<y+1\leftrightarrow x\leqslant y)},$

are not provable in $Q$; cf. Lemma 12. We do not want such details to distract
us. Second, we can extract useful information about notions of inductiveness
in Section 7 over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
On the contrary, Robinson’s $Q$ is too weak to prove any non-trivial
implication between our notions of inductiveness. More specifically,
Proposition 22(e) and (f) become false if one changes the base theory to $Q$.
Nevertheless, many other results in this paper, for example, Theorem 8,
Proposition 9 and Lemma 19, remain true over $Q$. Denote the language
$\\{0,1,{+},{\times},{<}\\}$ for ordered rings by
_$\mathscr{L}_{\mathrm{OR}}$_. Abusing notation, if $n\in\mathbb{N}$, then we
denote the closed $\mathscr{L}_{\mathrm{OR}}$ term

$(\cdots((0+\underbrace{1)+1)+\dots+1)}_{\text{$n$-many $1$'s}}$

by $n$. Let
_$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$_
denote the theory of the non-negative parts of discretely ordered rings. We
axiomatize
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
by the following.

  1. (P1)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {\bigl{(}(x+y)+z=x+(y+z)\bigr{)}}}}$.

  2. (P2)

$\forall{x}\ {\forall{y}\ {(x+y=y+x)}}$.

  3. (P3)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {\bigl{(}(x\times y)\times
z=x\times(y\times z)\bigr{)}}}}$.

  4. (P4)

$\forall{x}\ {\forall{y}\ {(x\times y=y\times x)}}$.

  5. (P5)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {(x\times(y+z)=(x\times y)+(x\times
z))}}}$.

  6. (P6)

$\forall{x}\ {(x+0=x)}$.

  7. (P7)

$\forall{x}\ {(x\times 0=0)}$.

  8. (P8)

$\forall{x}\ {(x\times 1=x)}$.

  9. (P9)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {(x<y\wedge y<z\rightarrow x<z)}}}$.

  10. (P10)

$\forall{x}\ {\neg x<x}$.

  11. (P11)

$\forall{x}\ {\forall{y}\ {(x<y\vee x=y\vee x>y)}}$.

  12. (P12)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {(x<y\rightarrow x+z<y+z)}}}$.

  13. (P13)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {(z\not=0\wedge x<y\rightarrow x\times
z<y\times z)}}}$.

  14. (P14)

$\forall{x}\ {\forall{y}\ {(x<y\leftrightarrow\exists{z}\ {((x+z)+1=y)})}}$.

  15. (P15)

$0<1\wedge\forall{x}\ {(x>0\rightarrow x\geqslant 1)}$.

  16. (P16)

$\forall{x}\ {(x\geqslant 0)}$.

Here _$x\leqslant y$_ is an abbreviation for $x<y\vee x=y$.

If $\theta(x,\bar{z})$ is an $\mathscr{L}_{\mathrm{OR}}$ formula, then the
_induction axiom for $\theta$_ with respect to the variable $x$, denoted by
_$\mathrm{I}_{x}\theta$_ or simply _$\mathrm{I}\theta$_ , is the sentence

$\forall{\bar{z}}\ {\bigl{(}\theta(0,\bar{z})\wedge\forall{x}\
{\bigl{(}\theta(x,\bar{z})\rightarrow\theta(x+1,\bar{z})\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\bigr{)}}.$

Define

$\displaystyle\mathrm{I}\mathrm{Open}$
$\displaystyle=\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is a quantifier-free $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\},$
$\displaystyle\mathrm{I}\Sigma_{k}$
$\displaystyle=\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is an $\mathscr{L}_{\mathrm{OR}}$~{}formula of complexity $\Sigma_{k}$}\\},\
\text{and}$ $\displaystyle\mathrm{PA}$
$\displaystyle=\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is an $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}.$

###  2.2. The necessity of non-analyticity

It has often been observed in the literature on inductive theorem proving that
“within first-order theories that include induction, the cut rule cannot be
eliminated” [BBHI05, p. 55]. This observation will provide a crucial
foundation for the justification of our model of inductive theorem proving.
Therefore we would like to discuss it here and, in the process, make it more
precise and show how to prove it.

Since we want to speak about cut-elimination we need to speak about the
sequent calculus. Which variant of the sequent calculus we use is not of
importance for the points discussed here; for the sake of precision let us fix
it to be the calculus LK of [Bus98a]. A sequent is denoted as
$\Gamma\longrightarrow\Delta$. For a theory $T$ and a formula $\varphi$,
$T\vdash\varphi$ if and only if there is a finite set $T_{0}\subseteq T$ and
an LK-proof of the sequent $T_{0}\longrightarrow\varphi$. Gentzen’s cut-
elimination theorem states that:

######  Theorem 1.

If there is an LK-proof of a sequent $\Gamma\longrightarrow\Delta$, then there
is a cut-free LK-proof of $\Gamma\longrightarrow\Delta$.

An important feature of cut-free proofs is that they have the subformula
property. In the context of first-order logic this means that every formula
that occurs in a cut-free proof of the sequent $\Gamma\longrightarrow\Delta$
is an _instance_ of a subformula of a formula that occurs in
$\Gamma\longrightarrow\Delta$. A proof that has the subformula property is
also called analytic.

Since the cut-elimination theorem considers arbitrary first-order sequents, it
can also be applied to theories containing induction axioms:

######  Corollary 2.

If $\mathrm{PA}\vdash\varphi$ then there is a finite
$A_{0}\subseteq\mathrm{PA}$ and a cut-free LK-proof of the sequent
$A_{0}\longrightarrow\varphi$.

So we see that in the sense of the above corollary, inductive theories do
allow cut-elimination. However, $A_{0}$ may contain induction axioms on
induction formulas which are not instances of subformulas of $\varphi$, i.e.,
non-analytic induction formulas.

The necessity of non-analytic induction formulas follows, for example, from
Gödel’s second incompleteness theorem: recall that, by arithmetizing the
syntax of formulas and proofs, one can formulate the consistency of a
recursive arithmetical theory as an $\mathscr{L}_{\mathrm{OR}}$ sentence. More
specifically, for all $k\in\mathbb{N}$ there is a $\Pi_{1}$ sentence
$\mbox{\rm Con}(\mathrm{I}\Sigma_{k})$ expressing the consistency of
$\mathrm{I}\Sigma_{k}$, see for example [Bus98b]. We then have:

######  Theorem 3.

For all $k\in\mathbb{N}$: $\mathrm{PA}\vdash\mbox{\rm
Con}(\mathrm{I}\Sigma_{k})$ but $\mathrm{I}\Sigma_{k}\nvdash\mbox{\rm
Con}(\mathrm{I}\Sigma_{k})$.

Note that this result embodies a very strong non-analyticity requirement:
given any $k\geqslant 1$, in order to prove $\mbox{\rm
Con}(\mathrm{I}\Sigma_{k})$ not only do we need a non-analytic induction
formula, but we need one with more than $k$ quantifier alternations even
though $\mbox{\rm Con}(\mathrm{I}\Sigma_{k})$ is only a $\Pi_{1}$ sentence.

This theorem entails the necessity of cut in the following sense. First,
formulate induction as the inference rule

$\Gamma\longrightarrow\Delta,\forall
x\,\psi(x)\lx@proof@logical@and\Gamma\longrightarrow\Delta,\psi(0)\Gamma,\psi(x)\longrightarrow\Delta,\psi(s(x))$

with the usual side condition and $\psi$ being an arbitrary formula. Observe
that $\mathrm{PA}\vdash\varphi$ if and only if there is an $\mbox{\rm
LK}+\mbox{\rm Ind}$-proof of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\longrightarrow\varphi$.
Now, in contrast to LK, the calculus $\mbox{\rm LK}+\mbox{\rm Ind}$ does not
have cut-elimination:

######  Corollary 4.

There is a formula $\varphi$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\longrightarrow\varphi$
has an $\mbox{\rm LK}+\mbox{\rm Ind}$-proof but no cut-free $\mbox{\rm
LK}+\mbox{\rm Ind}$-proof.

######  Proof 2.1.

Let $\varphi=\mbox{\rm Con}(\mathrm{I}\Sigma_{k})$ for any $k\geqslant 3$.
Then, by Theorem 3, $\mathrm{PA}\vdash\mbox{\rm Con}(\mathrm{I}\Sigma_{k})$
and consequently there is an $\mbox{\rm LK}+\mbox{\rm Ind}$-proof of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\longrightarrow\mbox{\rm
Con}(\mathrm{I}\Sigma_{k})$. On the other hand, suppose there would be a cut-
free $\mbox{\rm LK}+\mbox{\rm Ind}$-proof of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\longrightarrow\mbox{\rm
Con}(\mathrm{I}\Sigma_{k})$. Then, due to the subformula property, all
formulas, and in particular: all induction formulas, in this proof would be
$\Sigma_{3}$ thus contradicting Theorem 3.

These considerations show that the observation formulated at the beginning of
this section can be stated more precisely, and without mentioning the cut
rule, as: inductive theorem proving requires the use of non-analytic induction
axioms.

Remember that the notion of analyticity is to be understood in the sense of
first-order logic here. If we would move to second- or even higher-order
logic, for example by formulating the theorem-proving problem in terms of the
second-order induction axiom, then, in the presence of second-order
quantifiers, the meaning of the subformula property, and with it that of
analyticity, changes. Indeed, the non-analytic induction axioms of a
$\mathrm{PA}$-proof translate to instances (in the sense of second-order
logic) of the second-order induction axiom. Thus a $\mathrm{PA}$-proof
translates into a proof which is analytic in the sense of second-order logic.
But this is merely a change in terminology, not in substance and therefore we
will not consider this option.

###  2.3. A computational observation

In this section we take a closer look at the practice of inductive theorem
proving and, in particular, at the aspect of non-analytic induction axioms as
described above.

The set of sentences which are realistic as input to an inductive theorem
prover in practice is naturally fuzzy and we cannot claim to make it precise
here. What we have in mind are goals such as those of the TIP library
[CJRS15]. They typically consist of a universally quantified atomic formula to
be proved from some background axioms consisting also of universally
quantified atomic formulas. They have a size between a few dozen to several
hundred symbols and proofs with a symbolic complexity of one or two orders of
magnitude that of the goal. In comparison to arbitrary arithmetical sentences,
this is a quite restricted class. Its consideration is justified on the one
hand by the practical interest in goals of this form and, on the other hand,
by the difficulty of the inductive theorem proving problem in general. We also
restrict our attention to input sentences $\sigma$ such that
$\mathrm{PA}\vdash\sigma$. The recognition of non-theorems as such, while
clearly of high practical value, is a different topic which we do not consider
in this paper.

Now, given a realistic input sentence $\sigma$, there are, in theory, the
following options for generating (non-analytic) induction axioms which suffice
to prove $\sigma$. (1) One can use coding, for example as in the proof of the
finite axiomatizability of $\mathrm{I}\Sigma_{k}$ in [HP93, Theorem I.2.52].
Thus one can formulate the theorem-proving problem in $\mathrm{I}\Sigma_{k}$
(for a $k$ sufficiently high for practical purposes) as a theorem-proving
problem in pure first-order logic, thereby eliminating the need of generating
further induction axioms. However, coding introduces an overhead which,
although constant, is so high that it dominates the complexity of all
practically relevant instances to such an extent that this approach is not
useful in practice. (2) Similar to but even simpler than (1), one can just fix
a $k$, sufficiently high for practical purposes, so that we are interested
only in finding proofs whose induction axioms contain at most $k$ symbols.
Since there are only a finite number of such induction axioms, the theorem-
proving problem, again, becomes a pure first-order problem. Just as in (1),
although this avoids the need of generating further induction axioms, it
introduces a syntactic overhead which renders this approach useless in
practice (even though coding does not play a role here).

So, in practice, these brute force methods are not an option. Instead, one
typically tries to find simple induction axioms, tailored to the goal, and a
proof of the goal based on them. Again, we cannot claim to make this notion
precise here but we refer to typical solutions of the TIP problems as listed,
e.g., in [IB96]. We can now make the following computational observation:

######  Computational Observation.

For sentences $\sigma$ which are input to an inductive theorem prover: if it
is feasible to find simple formulas $\theta_{1},\ldots,\theta_{n}$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}\theta_{1},\ldots,\mathrm{I}\theta_{n}\\}\vdash\sigma$,
then it is feasible to find a proof in pure first-order logic of $\sigma$ from
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}\theta_{1},\ldots,\mathrm{I}\theta_{n}\\}$.

It is important to note here that the input sentence $\sigma$ and the
induction formulas $\theta_{i}$ are restricted as discussed above. The word
“feasible” is to be understood in the sense of the possibility of an
implementation which solves the task successfully on contemporary hardware in
a reasonable amount of time.

The observation is based on the following grounds. First, automated theorem
proving in pure first-order logic is a subject that has undergone continuous
progress for decades and has reached a quite mature state. The regular CASC-
competition [Sut16] is a testament to that as is the widespread use of first-
order theorem provers in external tools, e.g., Sledgehammer [PB12]. Inductive
theorem proving, and in particular the generation of simple non-analytic
induction invariants, does not enjoy a comparable level of stability and
maturity (yet?). Secondly, and in terms of concrete evidence, we have
considered 53 proofs of problems from the TIP-library. These proofs have been
manually entered in the GAPT-system [EHR+16] by a student of the first author
(for another purpose). Of these 53 proofs, GAPT’s built-in first-order prover
Escargot, which is a quite simple superposition prover, could re-prove 48
based on the induction axioms alone within a timeout of $1$ minute per proof
using, on average, $3.3$ seconds per proof on standard PC hardware.

Another way to put this computational observation is the following: as
described in Section 2.2, the search space in inductive theorem proving has
two dimensions: (1) the search for instances of the induction scheme which
prove the goal, and (2) the search for a proof in pure first-order logic of
the goal from these instances. The above computational observation then states
that, for input sentences and induction formulas considered in practice, the
search space extends so much more in the first dimension than in the second
that we can afford to disregard the second. This observation forms an
important basis for our theoretical model of inductive theorem proving.

###  2.4. One induction axiom is enough

As a final step towards our model of inductive theorem proving, we will see in
this section that we can restrict our attention to the use of a single
induction axiom. An $\mathscr{L}_{\mathrm{OR}}$ formula $\varphi(x)$ is called
_inductive_ if
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\varphi(0)$
and
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{(\varphi(x)\rightarrow\varphi(x+1))}$. If $\varphi(x)$ is an inductive
formula, then $\forall{x}\ {\varphi(x)}$ is trivially equivalent over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
to the induction axiom

$\varphi(0)\wedge\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\varphi(x+1)\bigr{)}}\rightarrow\forall{x}\
{\varphi(x)}.$

Therefore, sentences of the form $\forall{x}\ {\varphi(x)}$, where
$\varphi(x)$ is inductive, can be viewed as particular instances of parameter-
free induction axioms. Conversely, as Lemma 5 below shows, every induction
axiom is equivalent over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
to an induction axiom of this form. As a result, every induction axiom
corresponds to an inductive formula, and the full induction scheme is
equivalent to its parameter-free counterpart. The argument is presumably well
known, cf. Kaye [Kay91, Exercise 8.3].

######  Lemma 5.

Let $\theta(x,\bar{z})$ be an $\mathscr{L}_{\mathrm{OR}}$ formula. Define
$\varphi(x)$ to be

$\forall{\bar{z}}\ {\bigl{(}\theta(0,\bar{z})\wedge\forall{y}\
{\bigl{(}\theta(y,\bar{z})\rightarrow\theta(y+1,\bar{z})\bigr{)}}\rightarrow\theta(x,\bar{z})\bigr{)}}.$

Then $\varphi(x)$ is inductive and
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\mathrm{I}_{x}\theta\leftrightarrow\forall{x}\
{\varphi(x)}$.

######  Proof 2.2.

Let us first verify that $\varphi(x)$ is inductive. Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
We have $\varphi(0)$ trivially. Suppose $x_{0}$ is such that $\varphi(x_{0})$
holds, and take $\bar{z}$ such that the hypothesis in $\varphi(x_{0}+1)$
holds, i.e.,

$\theta(0,\bar{z})\wedge\forall{y}\
{\bigl{(}\theta(y,\bar{z})\rightarrow\theta(y+1,\bar{z})\bigr{)}}.$

Then $\theta(x_{0},\bar{z})$ must be true since $\varphi(x_{0})$, and thus
$\theta(x_{0}+1,\bar{z})$ is also true by the second conjunct displayed above.
This shows $\varphi(x_{0}+1)$.

Next, we verify that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\mathrm{I}_{x}\theta\leftrightarrow\forall{x}\
{\varphi(x)}$. Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
again. Suppose $\forall{x}\ {\varphi(x)}$. Take $\bar{z}$ such that

$\theta(0,\bar{z})\wedge\forall{y}\
{\bigl{(}\theta(y,\bar{z})\rightarrow\theta(y+1,\bar{z})\bigr{)}}.$

We want $\forall{x}\ {\theta(x,\bar{z})}$. So pick any $x_{0}$. We know
$\varphi(x_{0})$ holds by hypothesis. Thus $\theta(x_{0},\bar{z})$ by the
definition of $\varphi(x)$, as required.

Conversely, assume $\mathrm{I}_{x}\theta$ holds, i.e.,

$\forall{\bar{z}}\ {\bigl{(}\theta(0,\bar{z})\wedge\forall{y}\
{\bigl{(}\theta(y,\bar{z})\rightarrow\theta(y+1,\bar{z})\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\bigr{)}}.$

Let $x_{0}$ be arbitrary. We want $\varphi(x_{0})$. So take any $\bar{z}$ such
that $\theta(0,\bar{z})\wedge\forall{y}\
{\bigl{(}\theta(y,\bar{z})\rightarrow\theta(y+1,\bar{z})\bigr{)}}$. Then our
assumption implies $\theta(x_{0},\bar{z})$, which is what we want.

The key idea behind the lemma above is that inductive formulas are, in a
sense, closed under definable conjunction. In particular, any two induction
axioms are implied by a third over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.

######  Proposition 6 (Gentzen [Gen54]).

For all $\mathscr{L}_{\mathrm{OR}}$ formulas $\theta_{0},\theta_{1}$, there is
an inductive formula $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\rightarrow\mathrm{I}\theta_{0}\wedge\mathrm{I}\theta_{1}$.

######  Proof 2.3.

Apply Lemma 5 to find inductive formulas $\psi_{0}(x)$ and $\psi_{1}(x)$ such
that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\mathrm{I}\theta_{i}\leftrightarrow\forall{x}\
{\psi_{i}(x)}$ for each $i<2$. Define
$\varphi(x)=\psi_{0}(x)\wedge\psi_{1}(x)$. As $\psi_{0}(x)$ and $\psi_{1}(x)$
are both inductive, it is easy to see that $\varphi(x)$ is inductive too.
Moreover, the sentence $\forall{x}\ {\varphi(x)}$ implies $\forall{x}\
{\psi_{0}(x)}\wedge\forall{x}\ {\psi_{1}(x)}$ and thus also
$\mathrm{I}\theta_{0}\wedge\mathrm{I}\theta_{1}$ over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.

The above proof straightforwardly generalizes to an arbitrary number of
$\mathscr{L}_{\mathrm{OR}}$ formulas $\theta_{1},\ldots,\theta_{n}$ and so we
obtain:

######  Corollary 7.

Let $\sigma$ be an $\mathscr{L}_{\mathrm{OR}}$ sentence. Then
$\mathrm{PA}\vdash\sigma$ if and only if there is an inductive formula
$\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\rightarrow\sigma$. ∎

Since we only use simple syntactic operations (conjunction in Corollary 7 and
the definition in the statement of Lemma 5) to combine many induction axioms
into one, the computational observation is preserved even when restricted to a
single induction axiom. Our theoretical model for inductive theorem proving is
now the following computational problem.

ITP Input: A sentence $\sigma$ provable in $\mathrm{PA}$ Output: An inductive
formula $\varphi(x)$ s.t.
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\rightarrow\sigma$

Formally this just defines a binary relation (between $\sigma$ and
$\varphi(x)$). But of course, implicitly, we take the perspective of wanting
to compute such a $\varphi(x)$ from a given $\sigma$. We claim that this
computational problem is a suitable theoretical model of the practice of
inductive theorem proving. This claim rests on the computational observation
made in Section 2.3 and sharpened in this section. In the rest of this paper
we will study this problem, in particular by relating it to several of its
variants.

##  3\. Variations of the proof shape

The ITP problem as defined above induces a natural proof shape: the
combination of (i) a
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$-proof
of the induction base, (ii) a
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$-proof
of the induction step, and (iii) a
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$-proof
of $\forall{x}\ {\varphi(x)}\rightarrow\sigma$. As long as we use ordinary
successor induction, there is no freedom in the first two proof obligations,
there is however in the third. In this section we will consider two variants
of ITP which are obtained by modifying (iii).

The sharp-eyed reader may have noticed that the inductive formula $\varphi(x)$
in our proof of Proposition 6 actually makes
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\leftrightarrow\mathrm{I}\theta_{0}\wedge\mathrm{I}\theta_{1}$. We
can use this to obtain

######  Theorem 8.

Let $\sigma$ be an $\mathscr{L}_{\mathrm{OR}}$ sentence. Then
$\mathrm{PA}\vdash\sigma$ if and only if there is an inductive formula
$\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\leftrightarrow\sigma$.

######  Proof 3.1.

The “if” direction is clear from the definition of inductive formulas. For the
“only if” direction, apply Proposition 6 to find an inductive formula
$\psi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\psi(x)}\rightarrow\sigma$. We verify that

$\varphi(x)\quad=\quad\neg\sigma\rightarrow\psi(x)$

has the properties we want. First, it is clear that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\sigma\rightarrow\forall{x}\
{\varphi(x)}$. Second, work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$,
and suppose $\neg\sigma$. Since
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\psi(x)}\rightarrow\sigma$, this implies $\exists{x}\ {\neg\psi(x)}$. If
$x_{0}$ is such that $\neg\psi(x_{0})$, then $\neg\sigma\wedge\neg\psi(x_{0})$
and so $\neg\varphi(x_{0})$. We can thus conclude
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\neg\sigma\rightarrow\neg\forall{x}\
{\varphi(x)}$. Finally, the formula $\varphi(x)$ is inductive because it is
equivalent to either $x=x$ or $\psi(x)$ depending on whether $\sigma$ holds or
not, and both $x=x$ and $\psi(x)$ are inductive.

This is a particular case of a more general phenomenon. As a normal form
theorem in a very broad sense, it is perhaps reminiscent of the
Friedman–Goldfarb–Harrington Theorem and its generalizations [Vis05, Joo15],
which assert that over a sufficiently strong base theory, every
$\mathscr{L}_{\mathrm{OR}}$ sentence is equivalent to a consistency statement.
This result motivates the consideration of the equivalence version of ITP:

$\textsc{ITP}_{\textsc{Eq}}$ Input: A sentence $\sigma$ provable in
$\mathrm{PA}$ Output: An inductive formula $\varphi(x)$ s.t.
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\leftrightarrow\sigma$

Theorem 8 ensures that, just as ITP, also $\textsc{ITP}_{\textsc{Eq}}$ is a
total relation in the sense that for every input there is an output as
required. However, for a fixed $\sigma$ the $\varphi(x)$’s permitted in
$\textsc{ITP}_{\textsc{Eq}}$ are a strongly restricted subset of those
permitted in ITP. This leads to a significant reduction of the search space.
Typically, restrictions of the search space play a crucial role for automated
theorem proving in practice. We are not aware of a technique that would
exploit this reduction of ITP to $\textsc{ITP}_{\textsc{Eq}}$. In how far this
restriction to equivalent formulas is useful in practice therefore remains
unclear for the time being.

Another modification of the proof shape of ITP consists of considering a
universally quantified $\sigma$, i.e., $\sigma=\forall{x}\ {\psi(x)}$, and
seeking an inductive formula $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\psi(x)\bigr{)}}$. This is of relevance to
computer science since it corresponds to the treatment of loops in correctness
proofs for imperative programs by loop invariants as in the Hoare calculus
[AdBO09, BM07]. As one may expect, this method does not work for all
$\mathrm{PA}$-provable formulas.

######  Proposition 9.

There is an $\mathscr{L}_{\mathrm{OR}}$ formula $\psi(x)$ such that
$\mathrm{PA}\vdash\forall{x}\ {\psi(x)}$ but no inductive formula $\varphi(x)$
makes
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\psi(x)\bigr{)}}$.

######  Proof 3.2.

Pick an $\mathscr{L}_{\mathrm{OR}}$ sentence $\sigma$ that is provable in
$\mathrm{PA}$ but not in
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
Consider the $\mathscr{L}_{\mathrm{OR}}$ formula $\psi(x)$, which is defined
to be

$\sigma\lor x\not=0.$

Then $\mathrm{PA}\vdash\forall{x}\ {\psi(x)}$ because
$\mathrm{PA}\vdash\sigma$. Let
$M\models\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\neg\sigma$,
which exists since
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\sigma$.
Then $M\models\neg\psi(0)$ by the definition of $\psi(x)$. Therefore, for _no_
formula $\varphi(x)$ can

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{(\varphi(x)\rightarrow\psi(x))}\wedge\varphi(0).$

As a result, the following uniform version of ITP

$\textsc{ITP}_{\textsc{U}}$ Input: A sentence $\forall{x}\ {\psi(x)}$ provable
in $\mathrm{PA}$ Output: An inductive formula $\varphi(x)$ s.t.
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{(\varphi(x)\rightarrow\psi(x))}$

is not a total relation. Nevertheless, some weak form of completeness is still
possible if we restrict ourselves to simple enough $\mathscr{L}_{\mathrm{OR}}$
sentences provable in a sufficiently weak fragment of $\mathrm{PA}$, as the
following theorem shows.

An $\mathscr{L}_{\mathrm{OR}}$ formula is _bounded_ if all the quantifiers it
contains are of the form $\forall{x{<}{t}}{}$ or $\exists{x{<}{t}}{}$, where
$t$ is a term in $\mathscr{L}_{\mathrm{OR}}$ that does not involve the
variable $x$. Bounded formulas are also called _$\Delta_{0}$ formulas_. The
theory _$\mathrm{I}\Delta_{0}$_ is

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is a bounded $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}.$

Fix a bounded formula $y=2^{x}$ such that

$\mathrm{I}\Delta_{0}\vdash\begin{aligned} &\forall{x,y,y^{\prime}}\
{(y=2^{x}\wedge y^{\prime}=2^{x}\rightarrow y=y^{\prime})}\\\ &\wedge
2^{0}=1\wedge\forall{x,y}\ {(y=2^{x}\leftrightarrow
2y=2^{x+1})}.\end{aligned}$

Let _$\exp$_ be the axiom $\forall{x}\ {\exists{y}\ {(y=2^{x})}}$. See Section
V.3(c) in Hájek–Pudlák [HP93], for example, for a construction of the formula
$y=2^{x}$.

######  Theorem 10 (Wilkie–Paris).

The following are equivalent for a bounded formula $\psi(x)$.

  1. (i)

$\mathrm{I}\Delta_{0}+\exp\vdash\forall{x}\ {\psi(x)}$.

  2. (ii)

There is an inductive formula $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{(\varphi(x)\rightarrow\psi(x))}$.

######  Proof 3.3.

See Corollary 8.7 in Wilkie–Paris [WP87] or Theorem V.5.26 in Hájek–Pudlák
[HP93].

##  4\. Different forms of induction

In our definition of ITP we have fixed the induction scheme to the ordinary
successor induction. This is by no means the only choice. It is well known
that the induction scheme has many equivalent formulations. In this section we
will introduce those alternative formulations that we treat in this paper, and
start to study their relationship, both in the general and in the quantifier-
free setting. Our interest in the quantifier-free setting is motivated by the
fact that some methods for inductive theorem proving restrict themselves to
quantifier-free induction formulas, see, e.g. [BM79].

###  4.1. Different induction schemes

Let $\theta(x,\bar{z})$ be an $\mathscr{L}_{\mathrm{OR}}$ formula. We define
the following induction axioms:

  * •

The _$ <$-induction axiom_ $\mathrm{I}^{<}_{x}\theta$ is

$\forall{\bar{z}}\ {\Bigl{(}\forall{y}\ {\bigl{(}\forall{x{<}{y}}\
{\theta(x,\bar{z})\rightarrow\theta(y,\bar{z})}\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\Bigr{)}}.$

  * •

Let $n\in\mathbb{N}$. The _$(n+1)$ -step induction axiom_
$\mathrm{I}^{\text{$(n+1)$-step}}_{x}\theta$ is

$\forall{\bar{z}}\
{\Bigl{(}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\theta(k,\bar{z})\wedge\forall{x}\
{\bigl{(}\theta(x,\bar{z})\rightarrow\theta(x+n+1,\bar{z})\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\Bigr{)}}.$

  * •

Let $n\in\mathbb{N}$. The _$(n+1)$ -induction axiom_
$\mathrm{I}^{n+1}_{x}\theta$ is

$\forall{\bar{z}}\
{\Bigl{(}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\theta(k,\bar{z})\wedge\forall{x}\
{\Bigl{(}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\theta(x+k,\bar{z})\rightarrow\theta(x+n+1,\bar{z})\Bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\Bigr{)}}.$

  * •

The _polynomial induction axiom_ $\mathrm{I}^{\text{\mbox{\rm p}}}_{x}\theta$
is

$\forall{\bar{z}}\ {\Bigl{(}\theta(0,\bar{z})\wedge\forall{x}\
{\bigl{(}\theta(x,\bar{z})\rightarrow\theta(2x,\bar{z})\wedge\theta(2x+1,\bar{z})\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\Bigr{)}}.$

Each of these schemes naturally induces a notion of inductiveness. Let
$\varphi(x)$ be an $\mathscr{L}_{\mathrm{OR}}$ formula with precisely one free
variable $x$.

  * •

$\varphi(x)$ is _$ <$-inductive_ if
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{y}\
{\bigl{(}\forall{x{<}{y}}\ {\varphi(x)\rightarrow\varphi(y)}\bigr{)}}$.

  * •

Let $n\in\mathbb{N}$. We say $\varphi(x)$ is _$(n+1)$ -step inductive_ if

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\varphi(k)\wedge\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\varphi(x+n+1)\bigr{)}}.$

  * •

Let $n\in\mathbb{N}$. We say $\varphi(x)$ is _$(n+1)$ -inductive_ if

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\varphi(k)\wedge\forall{x}\
{\Bigl{(}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\varphi(x+k)\rightarrow\varphi(x+n+1)\Bigr{)}}.$

  * •

$\varphi(x)$ is _polynomially inductive_ , or simply _p -inductive_, if

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\varphi(0)\wedge\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\varphi(2x)\wedge\varphi(2x+1)\bigr{)}}.$

The first of the above formulations, $<$-induction, is also known as strong
induction and is commonly used in mathematics. The consideration of
$(n+1)$-step induction is motivated by its use in [BBHI05]. The $k$-induction
scheme has become popular in computer-aided verification, see, e.g., [SSS00,
DKR11]. Polynomial induction has been introduced by Buss in [Bus86] for the
study of weak arithmetical theories and their relation to computational
complexity classes. In this paper, we restrict ourselves to the base-2
polynomial induction scheme in order to keep the exposition sufficiently
simple; see Remark 26 for some extra information about other bases.

######  Proposition 11.

The following are equivalent for every $n\in\mathbb{N}$:

  1. (i)

$\mathrm{PA}=\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is an $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$;

  2. (ii)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{<}_{x}\theta:\text{$\theta(x,\bar{z})$
is an $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$;

  3. (iii)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{\text{\rm$(n+1)$-step}}_{x}\theta:\text{$\theta(x,\bar{z})$
is an $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$;

  4. (iv)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{n+1}_{x}\theta:\text{$\theta(x,\bar{z})$
is an $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$;

  5. (v)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{\text{\mbox{\rm
p}}}_{x}\theta:\text{$\theta(x,\bar{z})$ is an
$\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$.

The proof of Proposition 11 is a straightforward exercise. So instead of
showing it here, we show its quantifier-free counterpart, Theorem 13.
Everything carries over _except_ the arguments for
$\eqref{item:altPA/PA}\Rightarrow\eqref{item:altPA/'}$ and
$\eqref{item:altPA/p}\Rightarrow\eqref{item:altPA/PA}$. The former of these
implications was shown to remain true by a more substantial argument in
Shepherdson [She64]. First we gather a few statements easily provable in
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
that will be useful at several occasions.

######  Lemma 12.

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
proves

  1. (a)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {(x+z<y+z\rightarrow x<y)}}}$,

  2. (b)

$\forall{x}\ {\forall{y}\ {\forall{z}\ {(x\times z<y\times z\rightarrow
x<y)}}}$,

  3. (c)

$\forall{x}\ {\forall{y}\ {(x<y\rightarrow x+1\leqslant y)}}$,

  4. (d)

$\forall{x}\ {\bigl{(}x\leqslant
n\rightarrow\operatorname*{\mathchoice{\bigvee\mkern-16.5mu\bigvee}{\bigvee\mkern-12.0mu\bigvee}{\bigvee\mkern-13.0mu\bigvee}{\bigvee\mkern-11.0mu\bigvee}}_{k\leqslant
n}x=k\bigr{)}}$ for every $n\in\mathbb{N}$,

  5. (e)

$\forall{x}\ {(x<x+1)}$, and

  6. (f)

$\forall{x}\ {(x\not=0\rightarrow\exists{y}\ {(x=y+1)})}$.

######  Proof 4.1.

For (a) and (b), see the top of page 18 in Kaye [Kay91]. For (c) and (d), see
Proposition 2.1 and Lemma 2.6 in Kaye [Kay91] respectively.

For (e), we see that $x+1=(x+0)+1$ by axiom P6. So we are done by axiom P14.

For (f), work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
If $x\not=0$, then axiom P16 implies $x>0$, and so we get the $y$ we want by
P14.

######  Theorem 13 (mostly Shepherdson).

The following are equivalent for all $n\in\mathbb{N}$:

  1. (i)

$\mathrm{I}\mathrm{Open}=\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is a quantifier-free $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$;

  2. (ii)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{<}_{x}\theta:\text{$\theta(x,\bar{z})$
is a quantifier-free $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$;

  3. (iii)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{\text{\rm$(n+1)$-step}}_{x}\theta:\text{$\theta(x,\bar{z})$
is a quantifier-free $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$;

  4. (iv)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{n+1}_{x}\theta:\text{$\theta(x,\bar{z})$
is a quantifier-free $\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$.

######  Proof 4.2.

We refer the reader to the original Shepherdson paper [She64] for a proof of
$\eqref{item:IOpen/IOpen}\Rightarrow\eqref{item:IOpen/'}$. We do not include a
proof here because it would be too distracting for the present paper to set up
all the algebraic materials for the argument. Nevertheless, some of the ideas
can be found in Section 8.

Consider $\eqref{item:IOpen/'}\Rightarrow\eqref{item:IOpen/step}$. Work over
(ii). Fix $\bar{z}$ and let $\theta(x,\bar{z})$ be a quantifier-free
$\mathscr{L}_{\mathrm{OR}}$ formula such that $\exists{x}\
{\neg\theta(x,\bar{z})}$. Use (ii) to find $x_{0}=(\min
x)(\neg\theta(x,\bar{z}))$. If $x_{0}<n+1$, then
$\operatorname*{\mathchoice{\bigvee\mkern-16.5mu\bigvee}{\bigvee\mkern-12.0mu\bigvee}{\bigvee\mkern-13.0mu\bigvee}{\bigvee\mkern-11.0mu\bigvee}}_{k<n+1}\neg\theta(k,\bar{z})$
by Lemma 12(d). So suppose $x_{0}\geqslant n+1$. Then $x_{0}>n$ by (the
contrapositive of) Lemma 12(c). Apply axiom P14 to find $w_{0}$ such that
$x_{0}=n+w_{0}+1>w_{0}$. Then $\theta(w_{0},\bar{z})$ holds by the minimality
of $x_{0}$, but $\neg\theta(w_{0}+n+1,\bar{z})$, as required.

The implication $\eqref{item:IOpen/step}\Rightarrow\eqref{item:IOpen/n}$ is
clear.

Consider $\eqref{item:IOpen/n}\Rightarrow\eqref{item:IOpen/IOpen}$. Work over
(iv). Fix $\bar{z}$ and let $\theta(x,\bar{z})$ be a quantifier-free
$\mathscr{L}_{\mathrm{OR}}$ formula such that
$\theta(0,\bar{z})\wedge\forall{x}\
{\bigl{(}\theta(x,\bar{z})\rightarrow\theta(x+1,\bar{z})\bigr{)}}$. Then

$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\theta(k,\bar{z})\wedge\forall{x}\
{\Bigl{(}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\theta(x,\bar{z})\rightarrow\theta(x+n+1,\bar{z})\Bigr{)}},$

and so we are done by (iv).

The following small lemma will be handy when proving the quantifier-free
analogue of $\eqref{item:altPA/PA}\Rightarrow\eqref{item:altPA/p}$ of
Proposition 11.

######  Lemma 14.

  1. (a)

$\mathrm{I}\mathrm{Open}\vdash\forall{x,d}\ {\exists{q,r}\
{(d\not=0\rightarrow x=qd+r\wedge r<d)}}$, but

  2. (b)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\forall{x}\
{\exists{y}\ {(x=2y\vee x=2y+1)}}$.

######  Proof 4.3.

For the provability part, we follow Kaye [Kay90, page 5]. Work over
$\mathrm{I}\mathrm{Open}$. Take any $x,d$ with $d\not=0$. Using the axioms of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
and Lemma 12(f), one can routinely verify that $0d\leqslant x<(x+1)d$. Apply
induction on $q$ for the atomic formula $qd\leqslant x$ to find $q$ which
satisfies $qd\leqslant x<(q+1)d=qd+d$. Then setting $r=x-qd<qd+d-qd=d$ gives
us what we want.

For the unprovability part, consider the set $\mathbb{Z}[X]^{+}$ of all
elements of the polynomial ring $\mathbb{Z}[X]$ that either are zero or have
positive leading coefficients. It is naturally a model of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$,
as the reader can verify [Kay91, Section 2.1]. Clearly,

$\mathbb{Z}[X]^{+}\models\neg\exists{y}\ {(X=2y\vee X=2y+1)}.$

######  Proposition 15.

$\mathrm{I}\mathrm{Open}$ proves

$\forall{\bar{z}}\ {\bigl{(}\theta(0,\bar{z})\wedge\forall{x}\
{\bigl{(}\theta(x,\bar{z})\rightarrow\theta(2x,\bar{z})\wedge\theta(2x+1,\bar{z})\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\bigr{)}}$

for every quantifier-free $\mathscr{L}_{\mathrm{OR}}$ formula
$\theta(x,\bar{z})$.

######  Proof 4.4.

Work over $\mathrm{I}\mathrm{Open}$. Let $\theta(x,\bar{z})$ be a quantifier-
free $\mathscr{L}_{\mathrm{OR}}$ formula and $\bar{z}$ be parameters such that
$\exists{x}\ {\neg\theta(x,\bar{z})}$. By Proposition 13(ii), this has a least
witness, say $x_{0}$. If $x_{0}=0$, then $\neg\theta(0,\bar{z})$. So suppose
$x_{0}\not=0$. Using Lemma 14, find $y_{0}$ such that $x_{0}=2y_{0}$ or
$x_{0}=2y_{0}+1$. Since $x_{0}\not=0$, we know $y_{0}<x_{0}$ by Lemma 12(f)
and axiom P14. So $\theta(y_{0},\bar{z})$ by the minimality of $x_{0}$. We are
thus done because
$\neg\theta(2y_{0},\bar{z})\vee\neg\theta(2y_{0}+1,\bar{z})$.

Following the proof of Theorem V.4.6 in Hájek–Pudlák [HP93], one can prove
$\mathrm{I}\mathrm{Open}$ from
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
plus the polynomial induction scheme for formulas of the form
$\forall{y{<}{t}}\ {\eta(x,y,\bar{z})}$ where $\eta(x,y,\bar{z})$ is a
quantifier-free $\mathscr{L}_{\mathrm{OR}}$ formula and $t$ is an
$\mathscr{L}_{\mathrm{OR}}$ term not involving $y$. The use of this extra
bounded quantifier cannot be eliminated.

######  Theorem 16 (Johannsen).

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}^{\text{\mbox{\rm
p}}}_{x}\theta:\text{$\theta(x,\bar{z})$ is a quantifier-free
$\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}$ does not prove $\forall{x}\
{\exists{y}\ {(x=3y\vee x=3y+1\vee x=3y+2)}}$. Consequently, it is strictly
weaker than $\mathrm{I}\mathrm{Open}$.

######  Proof 4.5.

This follows from Theorem 2 in Johannsen [Joh93].

###  4.2. Variations of induction scheme and proof shape

All results of Section 3, with the possible exception of Theorem 10, actually
remain true when the induction scheme is replaced by another scheme in
Proposition 11. The proofs are straightforward modifications of what we
presented there, and hence are left to the reader. In this section we abstract
one part that may be of independent interest. This stems from the observation
that, in a sense, Proposition 6 is the only property of $\mathrm{PA}$ one
needs in establishing Theorem 8.

Let $\mathscr{L}$ be a language. Denote by _$\mathscr{L}(\mathsf{X})$_ the
language obtained from $\mathscr{L}$ by adding one new unary predicate symbol
$\mathsf{X}$. Let $S$ be a sentence in $\mathscr{L}(\mathsf{X})$. If
$\varphi(x,\bar{z})$ is an $\mathscr{L}$ formula, then define _$S\varphi$_ to
be the universal closure of the $\mathscr{L}$ formula obtained from $S$ by
replacing each occurrence of $\mathsf{X}(\dots)$ by $\varphi(\dots,\bar{z})$.
The _scheme determined by $S$_, denoted _$S\mathscr{L}$_ , is defined to be
$\\{S\varphi:\varphi\in\mathscr{L}\\}$. The scheme $S\mathscr{L}$ is
_mergeable_ over an $\mathscr{L}$ theory $B$ if for all $\mathscr{L}$ formulas
$\psi_{0},\psi_{1}$, there is an $\mathscr{L}$ formula $\varphi$ such that
$B+S\varphi\vdash S\psi_{0}\wedge S\psi_{1}$.

Proposition 6 demonstrates the mergeability of the successor induction scheme
over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
A very similar proof shows that all other schemes in Proposition 11 are also
mergeable over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
Another example is the comprehension scheme in second-order arithmetic, which
is mergeable over rather weak base theories.

######  Theorem 17.

Fix a language $\mathscr{L}$. Let $S\mathscr{L}$ be a scheme and $B$ be an
$\mathscr{L}$ theory such that $B\vdash S\top$. The following are equivalent.

  1. (i)

$S\mathscr{L}$ is mergeable over $B$.

  2. (ii)

For every $\mathscr{L}$ sentence $\sigma$ provable from $B+S\mathscr{L}$,
there exists an $\mathscr{L}$ formula $\varphi(x,\bar{z})$ such that $B\vdash
S\varphi\leftrightarrow\sigma$.

######  Proof 4.6.

For $\eqref{cond:merge/merge}\Rightarrow\eqref{cond:merge/rev}$, imitate the
proof of Theorem 8. Conversely, suppose (ii) holds. Pick arbitrary
$\mathscr{L}$ formulas $\psi_{0}$ and $\psi_{1}$. Define
$\sigma=S\psi_{0}\wedge S\psi_{1}$. Then $B+S\mathscr{L}\vdash\sigma$
trivially. By (ii), we get an $\mathscr{L}$ formula $\varphi$ such that
$B\vdash S\varphi\leftrightarrow\sigma$ and hence $B+S\varphi\vdash
S\psi_{0}\wedge S\psi_{1}$, as required.

######  Corollary 18.

Let $n\in\mathbb{N}$ and let $\sigma$ be an $\mathscr{L}_{\mathrm{OR}}$
sentence. The following are equivalent.

  1. (i)

$\mathrm{PA}\vdash\sigma$.

  2. (ii)

There is a $<$-inductive formula $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\leftrightarrow\sigma$.

  3. (iii)

There is an $(n+1)$-step inductive formula $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\leftrightarrow\sigma$.

  4. (iv)

There is an $(n+1)$-inductive formula $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\leftrightarrow\sigma$.

  5. (v)

There is a p-inductive formula $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\leftrightarrow\sigma$. ∎

###  4.3. Walther’s method for comparing induction schemes

In the context of inductive theorem proving, Walther [Wal92, Section 7]
proposed a method of comparing induction axioms. Let us formulate his method
as follows. If $B$ is a finite set of natural numbers and $S$ is a finite set
of $\mathscr{L}_{\mathrm{OR}}$ terms, then define _$\mathrm{PA}(B,S)$_ to be
the $\mathscr{L}_{\mathrm{OR}}$ theory axiomatized by
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
and the following axioms for all $\mathscr{L}_{\mathrm{OR}}$ formulas
$\theta(x,\bar{z})$:

$\forall{\bar{z}}\
{\Bigl{(}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k\in
B}\theta(k,\bar{z})\wedge\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{t\in
S}\forall{x}\
{\bigl{(}\theta(x,\bar{z})\rightarrow\theta(t(x,\bar{z}),\bar{z})\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\Bigr{)}}.$

In this terminology, the $(n+1)$-step induction scheme in Proposition 11(iii)
is essentially

$\mathrm{PA}(\\{k\in\mathbb{N}:k<n+1\\},\\{x+n+1\\}).$

(Some choices of $B$ and $S$ may give rise to a scheme $\mathrm{PA}(B,S)$ that
is not true in $\mathbb{N}$, but this does not concern us here.) Walther
observed that if $B\subseteq B^{\prime}$ and $S\subseteq S^{\prime}$, then
$\mathrm{PA}(B,S)\vdash\mathrm{PA}(B^{\prime},S^{\prime})$.

In this section we make the observation (not stated in [Wal92]) that this
method for comparing induction schemes is incomplete in the sense that the
converse implication is not true. To see this, take $m,n\in\mathbb{N}$ such
that $m<n$. Then

$\displaystyle\mathrm{PA}(\\{k\in\mathbb{N}:k<n+1\\},\\{x+m+1\\})$
$\displaystyle\equiv\mathrm{PA}(\\{k\in\mathbb{N}:k<m+1\\},\\{x+m+1\\})$
$\displaystyle\equiv\mathrm{PA}(\\{k\in\mathbb{N}:k<n+1\\},\\{x+n+1\\})$

by Proposition 11. Clearly $\\{x+m+1\\}\not\subseteq\\{x+n+1\\}$.

Thanks to Theorem 13, the observation in the previous paragraph has an
analogue in the quantifier-free context. We formulate this as follows. If $B$
is a finite set of natural numbers and $S$ is a finite set of
$\mathscr{L}_{\mathrm{OR}}$ terms, then define
_$\mathrm{I}\mathrm{Open}(B,S)$_ to be the $\mathscr{L}_{\mathrm{OR}}$ theory
axiomatized by
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
and the following axioms for all quantifier-free $\mathscr{L}_{\mathrm{OR}}$
formulas $\theta(x,\bar{z})$:

$\forall{\bar{z}}\
{\Bigl{(}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k\in
B}\theta(k,\bar{z})\wedge\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{t\in
S}\forall{x}\
{\bigl{(}\theta(x,\bar{z})\rightarrow\theta(t(x,\bar{z}),\bar{z})\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\Bigr{)}}.$

Clearly, if $B\subseteq B^{\prime}$ and $S\subseteq S^{\prime}$, then
$\mathrm{I}\mathrm{Open}(B,S)\vdash\mathrm{I}\mathrm{Open}(B^{\prime},S^{\prime})$.
The converse is not true because whenever $m,n\in\mathbb{N}$ such that $m<n$,
we have

$\displaystyle\mathrm{I}\mathrm{Open}(\\{k\in\mathbb{N}:k<n+1\\},\\{x+m+1\\})$
$\displaystyle\equiv\mathrm{I}\mathrm{Open}(\\{k\in\mathbb{N}:k<m+1\\},\\{x+m+1\\})$
$\displaystyle\equiv\mathrm{I}\mathrm{Open}(\\{k\in\mathbb{N}:k<n+1\\},\\{x+n+1\\})$

by Theorem 13, but $\\{x+m+1\\}\not\subseteq\\{x+n+1\\}$.

##  5\. Non-closure properties of cuts

In this short technical section we will establish an auxiliary result on cuts
that will be used in Section 6 and Section 7 for comparing solutions to ITP
and notions of inductiveness respectively. Note that the meaning of the word
“cut” here is different from that in Section 2.2. In the study of weak
theories of arithmetic, these cuts are frequently used in interpretations.
They also serve as notions of smallness in many arguments. In the following,
we borrow some terminology from Visser [Vis14]. A _cut_ is an inductive
formula $\varphi(x)$ such that

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x,y}\
{\bigl{(}x<y\wedge\varphi(y)\rightarrow\varphi(x)\bigr{)}}.$

An _a-cut_ is a cut $\varphi(x)$ such that

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\varphi(x+x)\bigr{)}}.$

An _am-cut_ is an a-cut $\varphi(x)$ such that

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\varphi(x\times x)\bigr{)}}.$

Inductive formulas, cuts, a-cuts, and am-cuts are all different notions. This
fact seems to be well known, but we can find no proof of this in the
literature. So we include one here. The proof assumes familiarity with some
parts of the Hájek–Pudlák book [HP93].

######  Lemma 19.

There are $\mathscr{L}_{\mathrm{OR}}$ formulas $\varphi(x)$ and $\delta(x)$
such that

  1. (1)

$\varphi(x)$ is an a-cut but not an am-cut;

  2. (2)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\exists{{!}x}\
{\delta(x)}\wedge\forall{x}\
{\bigl{(}\delta(x)\rightarrow\varphi(x)\bigr{)}}$; and

  3. (3)

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\neg\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\varphi(x\times
x)\bigr{)}}\rightarrow\forall{x}\
{\bigl{(}\delta(x)\rightarrow\varphi(x)\wedge\neg\varphi(x\times x)\bigr{)}}$.

######  Proof 5.1.

Let $M\models\mathrm{PA}$ which contains a nonstandard element $a$ that is
definable by a bounded formula. For instance, if $M\models\neg\mbox{\rm
Con}(\mathrm{PA})$, then we can take $a$ to be the least (code of a) proof of
contradiction from $\mathrm{PA}$ in $M$. Fix a bounded formula $\delta_{0}(x)$
such that $M\models\exists{{!}x}\ {\delta_{0}(x)}\wedge\delta_{0}(a)$. Notice

$I=2^{\mathbb{N}a}=\\{x\in M:\text{$x<2^{na}$ for some $n\in\mathbb{N}$}\\}$

is an initial segment of $M$, and $2^{ma}\times 2^{na}=2^{(m+n)a}\in I$
whenever $m,n\in\mathbb{N}$. So $I$ is itself an $\mathscr{L}_{\mathrm{OR}}$
structure. Since $\delta_{0}(x)$ is a bounded formula, it is straightforward
[HP93, Remark IV.1.18] to check that $a$ is the unique element which satisfies
$\delta_{0}(x)$ in $I$. We know $I\models\mathrm{I}\Delta_{0}$ because
$\mathrm{I}\Delta_{0}$ is preserved under taking initial segments [HP93,
Remark IV.1.21]. Thus

$\log I=\\{x\in I:I\models\exists{u}\ {(}2^{x}=u)\\}$

is an initial segment of $I$ that is closed under $+$ because

$\displaystyle\mathrm{I}\Delta_{0}$ $\displaystyle\vdash\forall{x,y}\
{\bigl{(}\exists{u}\ {(2^{x}=u)}\wedge y\leqslant
x\rightarrow\exists{v{\leqslant}{u}}\ {(2^{y}=v)}\bigr{)}}$
$\displaystyle\phantom{{}\vdash{}}\wedge\forall{u,v,x,y}\ {(2^{x}=u\wedge
2^{y}=v\rightarrow 2^{x+y}=uv)},$

as verified in Hájek–Pudlák [HP93, Lemma V.3.8(iii) and page 302]. We know
$\log I$ contains $a$ but not $a^{2}$ because

$\log I=\\{x\in I:\text{$x<na$ for some $n\in\mathbb{N}$}\\}$

and $a\not\in\mathbb{N}$. In particular, it is not closed under $\times$. The
whole situation in $I$ can be captured by the sentence

$\sigma\quad=\quad\begin{aligned} &\varphi_{0}(0)\wedge\forall{x}\
{(\varphi_{0}(x)\rightarrow\varphi_{0}(x+x))}\wedge\forall{x,y}\
{(x<y\wedge\varphi_{0}(y)\rightarrow\varphi_{0}(x))}\\\ &\wedge\exists{{!}x}\
{\delta_{0}(x)}\wedge\exists{x}\
{(\delta_{0}(x)\wedge\varphi_{0}(x)\wedge\neg\varphi_{0}(x\times
x))},\end{aligned}$

where $\varphi_{0}(x)$ denotes the formula $\exists{u}\ {(}2^{x}=u)$. Clearly,

$\displaystyle\varphi(x)$
$\displaystyle\quad=\quad\sigma\rightarrow\varphi_{0}(x)\quad\text{and}\quad$
$\displaystyle\delta(x)$
$\displaystyle\quad=\quad(\sigma\rightarrow\delta_{0}(x))\wedge(\neg\sigma\rightarrow
x=0)$

have the properties we want.

######  Corollary 20.

  1. (a)

There is an inductive formula that is not a cut.

  2. (b)

There is a cut that is not an a-cut.

  3. (c)

There is an a-cut that is not an am-cut.

######  Proof 5.2.

Let $\varphi(x)$ and $\delta(x)$ be as given by Lemma 19.

  1. (a)

Take $\varphi(x)\vee\exists{c}\ {(\delta(c)\wedge x\geqslant c^{2})}$.

  2. (b)

Take $\exists{c,z}\ {(\varphi(z)\wedge\delta(c)\wedge x\leqslant c^{2}+z)}$.

  3. (c)

Take $\varphi(x)$.

Solovay’s method of shortening cuts [HP93, Theorem III.3.5] provides a general
way of producing cuts with various closure properties. However, a technique
for producing cuts with specific non-closure properties in large quantities
does not seem available at present. In particular, it is not clear whether
there is an inverse of Solovay’s method. Let $\varphi(x)$ be a cut. Assuming
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\forall{x}\
{\varphi(x)}$, can one always find a cut $\psi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
proves

$\forall{x}\
{\bigl{(}\varphi(x)\rightarrow\psi(x)\bigr{)}}\quad\text{and}\quad\forall{x}\
{\varphi(x)}\leftrightarrow\forall{x}\ {\psi(x)}$

and $\psi(x)$ is _not_ an am-cut?

##  6\. Comparing solutions

Given a $\mathrm{PA}$-theorem $\sigma$, our formulation of ITP considers the
set of solutions, the search space, to be all inductive $\varphi(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\rightarrow\sigma$. In automated theorem proving, restrictions of
the search space (usually such that completeness is retained) play an
important role. In this short section, based on the results of Section 5, we
make a comment on comparisons of two solutions $\varphi_{0}(x)$ and
$\varphi_{1}(x)$.

There are (at least) two ways of comparing two induction axioms $\forall{x}\
{\varphi_{0}(x)}$ and $\forall{x}\ {\varphi_{1}(x)}$, where $\varphi_{0}(x)$
and $\varphi_{1}(x)$ are inductive formulas. The first way is to say
$\forall{x}\ {\varphi_{0}(x)}$ is stronger than $\forall{x}\ {\varphi_{1}(x)}$
when
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi_{0}(x)}\rightarrow\forall{x}\ {\varphi_{1}(x)}$. The second way is to
say $\forall{x}\ {\varphi_{0}(x)}$ is stronger than $\forall{x}\
{\varphi_{1}(x)}$ when
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{(\varphi_{0}(x)\rightarrow\varphi_{1}(x))}$. Clearly, if an induction axiom
is stronger than another one in the second sense, then it is also stronger in
the first sense. The converse, however, is not true.

######  Proposition 21.

There are cuts $\varphi_{0}(x),\varphi_{1}(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
proves

$\forall{x}\ {\varphi_{0}(x)}\leftrightarrow\forall{x}\
{\varphi_{1}(x)}\quad\text{and}\quad\forall{x}\
{(\varphi_{0}(x)\rightarrow\varphi_{1}(x))}$

but
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\forall{x}\
{(\varphi_{1}(x)\rightarrow\varphi_{0}(x))}$.

######  Proof 6.1.

Let $\varphi(x)$ be as given by Lemma 19. We show that
$\varphi_{0}(x)=\varphi(x\times x)$ and $\varphi_{1}(x)=\varphi(x)$ have the
properties we want.

As $\varphi(x)$ is an a-cut, it is not hard to check that $\varphi_{0}(x)$ is
a cut. Next, notice
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\rightarrow\forall{x}\ {\varphi(x\times x)}$ trivially. Thus
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi_{1}(x)}\rightarrow\forall{x}\ {\varphi_{0}(x)}$. Notice also that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\bigl{(}\varphi(x\times x)\rightarrow\varphi(x)\bigr{)}}$ because
$\varphi(x)$ is a cut. So
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{(\varphi_{0}(x)\rightarrow\varphi_{1}(x))}$. Finally, we know
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\forall{x}\
{(\varphi_{1}(x)\rightarrow\varphi_{0}(x))}$ since $\varphi(x)$ is not an am-
cut.

We can view Proposition 21 from another angle. One may expect that the weakest
induction axiom which can prove an induction axiom $\mathrm{I}\varphi_{0}$ is
$\mathrm{I}\varphi_{0}$ itself. The proposition above says that this is not
the case _if_ we adopt the second way of comparing induction axioms:
$\mathrm{I}\varphi_{0}$ may be provable from another induction axiom
$\mathrm{I}\varphi_{1}$ where $\varphi_{1}(x)$ is a strictly weaker than
$\varphi_{0}(x)$ over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
as formulas. One may question whether there is always a weakest induction
axiom for proving a given theorem of $\mathrm{PA}$ in this sense. We do not
know the answer.

Let $\varphi_{0}(x)$ be a cut. Assuming
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\forall{x}\
{\varphi_{0}(x)}$, can one always find a cut $\varphi_{1}(x)$ such that
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
proves

$\forall{x}\ {\varphi_{0}(x)}\leftrightarrow\forall{x}\
{\varphi_{1}(x)}\quad\text{and}\quad\forall{x}\
{(\varphi_{0}(x)\rightarrow\varphi_{1}(x))}$

but
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\forall{x}\
{(\varphi_{1}(x)\rightarrow\varphi_{0}(x))}$?

As one can show by imitating our proof of Proposition 21, a positive answer to
Question 5 implies a positive answer to Question 6.

##  7\. Comparing notions of inductiveness

The question of how an inductive theorem prover should choose the induction
rule to be applied to its current goal has received a great deal of attention
in the literature on inductive theorem proving. Pioneering work on this
question has been done in the context of the ACL2 system and its predecessor
NQTHM through the introduction of the recursion analysis technique [BM79].
This technique, which suggests an induction rule based on the type of
recursion present in the goal, is specific to goals involving primitive
recursive functions; see also Bundy et al. [BvHH+89] and Stevens [Ste88].
However, the choice of the induction rule also plays an important role in
other contexts; see the discussion on “induction revision” in the book
[BBHI05] by Bundy et al., for example.

The interest in this question comes from the tension between the choice of the
induction rule and the choice of the induction formula when proving a goal:
the more flexibility we have in choosing the induction rule, the less
flexibility we need in choosing the induction formula. In the very extreme
case, one can fix an induction formula, e.g., the goal, and search for an
induction rule with respect to which this formula is inductive. Thus one can
dispose of the difficult task of finding a non-analytic induction formula and
simply search for a suitable induction rule. In this section we will carry out
a comparison of the formulations of induction introduced in Section 4 from
this point of view: we fix a formula $\varphi(x)$ and ask with respect to
which induction schemes it is inductive. Let $X$ be any notion of
inductiveness defined in Section 4. Then we can state the computational
problem

$\textsc{ITP}^{X}$ Input: A sentence $\sigma$ provable in $\mathrm{PA}$
Output: An $X$-inductive formula $\varphi(x)$ s.t.
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{\varphi(x)}\rightarrow\sigma$

By Proposition 11 all these problems define total relations. By Theorem 13,
the quantifier-free versions of $\textsc{ITP}^{X}$ are equivalent for all $X$
except possibly polynomial induction.

In this section, we investigate implications between these notions of
inductiveness. As we will see, some notions turn out to be incomparable. For
instance, not all $2$-step inductive formulas are $3$-step inductive, and not
all $3$-step inductive formulas are $2$-step inductive. The following
proposition lists all the implications we can establish.

######  Proposition 22.

Let $m,n\in\mathbb{N}$.

  1. (a)

The following are equivalent for a formula: it is inductive; it is $1$-step
inductive; and it is $1$-inductive.

  2. (b)

If $m+1$ divides $n+1$, then all $(m+1)$-step inductive formulas are
$(n+1)$-step inductive.

  3. (c)

If $m\leqslant n$, then all $(m+1)$-inductive formulas are $(n+1)$-inductive.

  4. (d)

All $(n+1)$-step inductive formulas are $(n+1)$-inductive.

  5. (e)

If a formula is $(n+1)$-inductive for some $n\in\mathbb{N}$, then it is
$<$-inductive.

  6. (f)

A formula $\varphi(x)$ is $<$-inductive if and only if
$\forall{x^{\prime}{\leqslant}{x}}\ {\varphi(x^{\prime})}$ is inductive.

######  Proof 7.1.

Parts (a)–(d) are easy exercises.

  1. (e)

Suppose $\varphi(x)$ is $(n+1)$-inductive. Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
Let $y_{0}$ be such that $\forall{x{<}{y_{0}}}\ {\varphi(x)}$. If
$y_{0}\leqslant n$, then $\varphi(y_{0})$ holds by Lemma 12(d) because
$\varphi(x)$ is $(n+1)$-inductive. So suppose $y_{0}>n$. Use axiom P14 to find
$x_{0}$ such that $y_{0}=x_{0}+n+1$. Then
$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\varphi(x_{0}+k)$
because $x_{0}+k<y_{0}$ for each $k<n+1$ by P14 again. As $\varphi(x)$ is
$(n+1)$-inductive and $y_{0}=x_{0}+n+1$, this implies $\varphi(y_{0})$.

  2. (f)

First, assume $\forall{x^{\prime}{\leqslant}{x}}\ {\varphi(x^{\prime})}$ is
inductive. Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
Let $y_{0}$ be such that $\forall{x{<}{y_{0}}}\ {\varphi(x)}$. If $y_{0}=0$,
then $\varphi(y_{0})$ by our assumption. So suppose $y_{0}\not=0$. Apply Lemma
12(f) to find $y_{0}^{\prime}$ such that $y_{0}=y_{0}^{\prime}+1$. Notice
$\forall{x{\leqslant}{y_{0}^{\prime}}}\ {\varphi(x)}$ by Lemma 12(e). Our
assumption then implies $\forall{x{\leqslant}{y_{0}}}\ {\varphi(x)}$, which,
in particular, tells us that $\varphi(y_{0})$.

Conversely, suppose $\varphi(x)$ is $<$-inductive. Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
again. With the help of P16, P9 and P10, we have $\varphi(0)$ trivially by
$<$-inductiveness. So $\forall{x^{\prime}{\leqslant}{0}}\
{\varphi(x^{\prime})}$. Let $x_{0}$ be such that
$\forall{x^{\prime}{\leqslant}{x_{0}}}\ {\varphi(x^{\prime})}$. Then Lemma
12(c) and (a) imply $\forall{x^{\prime}{<}{x_{0}+1}}\ {\varphi(x^{\prime})}$
and so $\varphi(x_{0}+1)$ by $<$-inductiveness. This shows
$\forall{x^{\prime}{\leqslant}{x_{0}+1}}\ {\varphi(x^{\prime})}$, as required.

We now proceed to show non-implications (based on the non-closure properties
of cuts established in Section 5). In particular, we show that beyond
Proposition 22 there is no further implication between “$<$-inductive”, the
“$(n+1)$-step inductive”s, and the “$(n+1)$-inductive”s.

######  Proposition 23.

Let $m,n\in\mathbb{N}$.

  1. (a)

If $(m+1)$ does not divide $(n+1)$, then there is an $(m+1)$-step inductive
formula that is not $(n+1)$-step inductive.

  2. (b)

If $m>n$, then there is an $(m+1)$-inductive formula that is not
$(n+1)$-inductive.

  3. (c)

If $n\geqslant 1$, then there is an $(n+1)$-inductive formula that is not
$(n+1)$-step inductive.

  4. (d)

There is a $<$-inductive formula that is not $(n+1)$-inductive.

######  Proof 7.2.

Let $\varphi(x)$ and $\delta(x)$ be $\mathscr{L}_{\mathrm{OR}}$ formulas given
by Lemma 19. Recall $\varphi(x)$ is not an am-cut. Take $c\in
M\models\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\neg\forall{x}\
{(\varphi(x)\rightarrow\varphi(x^{2}))}+\delta(c)$.

  1. (a)

Assume all $(m+1)$-step inductive formulas are $(n+1)$-step inductive.
Consider the formula

$\chi(x)\quad=\quad\varphi(x)\vee\exists{y}\ {(x=(m+1)y)}.$

We first show that $\chi(x)$ is $(m+1)$-step inductive. By our assumption on
$m$ and $n$, this will imply $\chi(x)$ is $(n+1)$-step inductive. Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
We know
$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<m+1}\chi(k)$
because $\varphi(x)$ is inductive. Take $x_{0}$ satisfying $\chi(x_{0})$. If
$y_{0}$ is such that $x_{0}=(m+1)y_{0}$, then $x_{0}+m+1=(m+1)(y_{0}+1)$ by P8
and P5, and thus $\chi(x_{0}+m+1)$. So suppose $\neg\exists{y}\
{(x_{0}=(m+1)y)}$. Then $\varphi(x_{0})$ holds by the definition of the
formula $\chi(x)$. As $\varphi(x)$ is an inductive formula, this implies
$\varphi(x_{0}+m+1)$ and hence $\chi(x_{0}+m+1)$.

Now look at our model $M$. Let $a=(m+1)(n+1)c^{2}$, so that $M\models\chi(a)$.
Notice $M\models\neg\varphi(c^{2})$ by condition (3) in Lemma 19. So
$M\models\neg\varphi(a+n+1)$ because $\varphi(x)$ is a cut and
$a+n+1=c^{2}+c^{2}(mn+m+n)+n+1>c^{2}$ by axiom P14. However, the previous
paragraph tells us that $M\models\chi(a+n+1)$. So $M\models\exists{y}\
{(a+n+1=(m+1)y)}$ by the definition of $\chi(x)$.

Find $b\in M$ such that $a+n+1=(m+1)b$. By axiom P14, we know
$(m+1)b=a+n+1>a=(m+1)(n+1)c^{2}$. So Lemma 12(b) implies $b>(n+1)c^{2}$. Apply
axiom P14 to find $z\in M$ such that $(n+1)c^{2}+z+1=b$. Then

$a+(m+1)(z+1)=(m+1)(n+1)c^{2}+(m+1)(z+1)=(m+1)b=a+n+1$

and thus $(m+1)(z+1)=n+1$ by axioms P11 and P12. Now $n+1=z+m(z+1)+1$. Hence
$n+1>z$ by axiom P14. Lemma 12(d) then tells us $z\in\mathbb{N}$. We can thus
conclude that $(m+1)$ divides $(n+1)$, which is what we want.

  2. (b)

We show that the formula

$\rho(x)\quad=\quad\varphi(x)\vee\forall{c}\
{\Bigl{(}\delta(c)\rightarrow\operatorname*{\mathchoice{\bigvee\mkern-16.5mu\bigvee}{\bigvee\mkern-12.0mu\bigvee}{\bigvee\mkern-13.0mu\bigvee}{\bigvee\mkern-11.0mu\bigvee}}_{k<n+1}x=c^{2}+k\Bigr{)}}$

is an example we want.

Suppose $m>n$. We show that $\rho(x)$ is $m$-inductive. Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
If $\forall{x}\ {(\varphi(x)\rightarrow\varphi(x^{2}))}$, then $\forall{x}\
{(\rho(x)\leftrightarrow\varphi(x))}$ by condition (2) in Lemma 19, and so we
are done by Proposition 22(a) and (c). So suppose $\neg\forall{x}\
{(\varphi(x)\rightarrow\varphi(x^{2}))}$. Since $\varphi(x)$ is inductive, we
know
$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<m+1}\rho(k)$.
Let $c,x_{0}$ be such that
$\delta(c)\wedge\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<m+1}\rho(x_{0}+k)$.
Take $k<n+1$. We know $c^{2}+k+m\geqslant c^{2}+m>c^{2}+n$ by axiom P12, and
$\neg\varphi(c^{2}+k+m)$ since $\varphi(x)$ is a cut and $\neg\varphi(c^{2})$.
These together imply $\neg\rho(c^{2}+k+m)$. So $x_{0}\not=c^{2}+k$ because
$\rho(x_{0}+m)$ holds. As the choice of $k<n+1$ is arbitrary, we know
$\varphi(x_{0})$ by the definition of $\rho(x)$. It follows that
$\varphi(x_{0}+m+1)$ because $\varphi(x)$ is inductive. Hence
$\rho(x_{0}+m+1)$.

We now show that $\rho(x)$ is not $(n+1)$-inductive using our model $M$. The
definition of $\rho(x)$ tells us
$M\models\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\rho(c^{2}+k)$.
On the one hand, notice $M\models\neg\varphi(c^{2})$ by condition (3) in Lemma
19. Also $c^{2}+n+1>c^{2}$ by axiom P14. Hence $\neg\varphi(c^{2}+n+1)$ since
$\varphi(x)$ is a cut. On the other hand, notice $c^{2}+n+1>c^{2}+k$ for any
$k<n+1$ by axiom P12. These together say that $M\models\neg\rho(c^{2}+n+1)$.

  3. (c)

We claim that the formula

$\rho_{0}(x)\quad=\quad\varphi(x)\vee\forall{c}\ {(\delta(c)\rightarrow
x=c^{2})}$

has the desired properties.

To show that $\rho_{0}(x)$ is $(n+1)$-inductive, let us work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
As in the previous part, we assume $\neg\forall{x}\
{(\varphi(x)\rightarrow\varphi(x^{2}))}$. Since $\varphi(x)$ is inductive, we
know
$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\rho_{0}(k)$.
Let $c,x_{0}$ be such that
$\delta(c)\wedge\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\rho_{0}(x_{0}+k)$.
As $n\geqslant 1$, we know $\rho_{0}(x_{0})\wedge\rho_{0}(x_{0}+1)$ in
particular. Notice $\neg\varphi(c^{2}+1)$ because $\varphi(x)$ is a cut and
$\neg\varphi(c^{2})$ by condition (3) in Lemma 19. Also $c^{2}+1\not=c^{2}$ by
Lemma 12(e). Thus $\neg\rho_{0}(c^{2}+1)$ holds, from which one deduces
$x_{0}\not=c^{2}$. This implies $\varphi(x_{0})$ by the definition of
$\rho_{0}(x)$. Since $\varphi(x)$ is inductive, we conclude that
$\varphi(x_{0}+n+1)$.

To show that $\rho_{0}(x)$ is not $(n+1)$-step inductive, we use $M$ as in the
proof of (b). Notice $M\models\rho_{0}(c^{2})$ by the definition of
$\rho_{0}(x)$. On the one hand, we know $M\models\neg\varphi(c^{2})$ by
condition (3) in Lemma 19. Also $c^{2}+n+1>c^{2}$ by axiom P14. Hence
$\neg\varphi(c^{2}+n+1)$ since $\varphi(x)$ is a cut. On the other hand, we
know $c^{2}+n+1>c^{2}$ by P14. These together say that
$M\models\neg\rho_{0}(c^{2}+n+1)$.

  4. (d)

It suffices to prove that the formula $\rho(x)$ defined in the proof of (b) is
$<$-inductive.

Work over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
Let $c,y_{0}$ be such that $\delta(c)$ and $\forall{x{<}{y_{0}}}\ {\rho(x)}$.
We will show $\rho(y_{0})$. If $y_{0}=0$, then $\varphi(y_{0})$ because
$\varphi(x)$ is inductive, and so $\rho(y_{0})$ holds. Therefore, assume
$y_{0}\not=0$. Apply Lemma 12(f) to find $x_{0}$ such that $y_{0}=x_{0}+1$.
Notice $y_{0}>x_{0}$ by Lemma 12(e). So, by the choice of $y_{0}$, we know
$\rho(x_{0})$.

Consider the case when $\neg\forall{x}\
{(\varphi(x)\rightarrow\varphi(x^{2}))}$. Then $\neg\varphi(c^{2})$ by
condition (3) in Lemma 19. This implies $c^{2}\not=0$ because $\varphi(x)$ is
inductive. Use Lemma 12(f) to find $w$ such that $c^{2}=w+1$. Then
$\neg\varphi(w)$ since $\varphi(x)$ is inductive and $\neg\varphi(w+1)$ holds.
Also, Lemma 12(e) implies $w<c^{2}\leqslant c^{2}+k$ for each $k<n+1$. We thus
know $\neg\rho(w)$ by the definition of $\rho(x)$. Our assumption on $y_{0}$
then implies $x_{0}<x_{0}+1=y_{0}\leqslant w<w+1=c^{2}$. Thus
$x_{0}\not=c^{2}+k$ for any $k<n+1$ by axiom P9, and so $\varphi(x_{0})$ must
hold.

If $\forall{x}\ {(\varphi(x)\rightarrow\varphi(x^{2}))}$, then
$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\varphi(c^{2}+k)$
by conditions (1) and (2) in Lemma 19. So $\varphi(x_{0})$ in either case
because $\rho(x_{0})$ holds. Since $\varphi(x)$ is inductive, we deduce
$\varphi(x_{0}+1)$ and hence $\rho(y_{0})$, as required.

Buss’s notion of polynomial induction does not fit well into the picture.

######  Proposition 24.

  1. (a)

There is a formula that is $(n+1)$-step inductive for every $n\in\mathbb{N}$
but is not p-inductive.

  2. (b)

For every $n\in\mathbb{N}$, there is a p-inductive formula that is not
$(n+1)$-inductive.

######  Proof 7.3.

  1. (a)

By Corollary 20(b), there is a cut that is not an a-cut. Such a cut is
$(n+1)$-step inductive for every $n\in\mathbb{N}$, but it is not p-inductive.

  2. (b)

Let $\varphi(x),\delta(x)$ be $\mathscr{L}_{\mathrm{OR}}$ formulas given by
Lemma 19. Define $\chi(x)$ to be the formula

$\varphi(x)\vee\exists{c}\ {\exists{s}\ {\exists{\ell}\ {\left(\begin{aligned}
&\delta(c)\wedge\operatorname*{\mathchoice{\bigvee\mkern-16.5mu\bigvee}{\bigvee\mkern-12.0mu\bigvee}{\bigvee\mkern-13.0mu\bigvee}{\bigvee\mkern-11.0mu\bigvee}}_{k<n+1}(s)_{0}=c^{2}+k\wedge(s)_{\ell}=x\\\
&\wedge\forall{i{<}{\ell}}\
{\bigl{(}(s)_{i+1}=2(s)_{i}\vee(s)_{i+1}=2(s)_{i}+1\bigr{)}}\\\
&\wedge\forall{i,j{\leqslant}{\ell}}\
{\bigl{(}i<j\rightarrow(s)_{i}<(s)_{j}\bigr{)}}\end{aligned}\right)}}}.$

Here $(s)_{i}=x$ is the $\mathscr{L}_{\mathrm{OR}}$ formula expressing “the
$i$th element in the sequence coded by $s$ is $x$” over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
given in Jeřábek [Jeř12]. It is then straightforward to see that $\chi(x)$ is
p-inductive. However, the formula $\chi(x)$ is not $(n+1)$-inductive because
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\exists{c}\
{\bigl{(}\delta(c)\wedge\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+1}\chi(c^{2}+k)\bigr{)}}$
and
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\exists{c}\
{(\delta(c)\wedge\chi(c^{2}+n+1))}$.

We do not know whether all p-inductive formulas are $<$-inductive. What we
have is only a translation of this question into a model-theoretic language.

######  Proposition 25.

The following are equivalent.

  1. (i)

There is a p-inductive formula that is not $<$-inductive.

  2. (ii)

In some model of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$,
there is a parameter-free definable element that is neither even nor odd.

######  Proof 7.4.

First, suppose (ii) fails. Let $\varphi(x)$ be any $\mathscr{L}_{\mathrm{OR}}$
formula that is not $<$-inductive. Find $c\in
M\models\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\forall{x{<}{c}}\
{\varphi(x)}\wedge\neg\varphi(c)$. If $c=0$, then
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\nvdash\varphi(0)$
and we are done. So suppose $c\not=0$. Notice $c=(\min x)(\neg\varphi(x))$. It
is, therefore, a parameter-free definable element of $M$. The failure of (ii)
then gives us $d\in M$ such that $c=2d$ or $c=2d+1$. By Lemma 12(f) and axiom
P14, we know $d<c$. Hence $M\models\varphi(d)$ by the minimality of $c$. This
shows $\varphi(x)$ is not p-inductive.

Conversely, suppose (ii) holds. Let $c\in
M\models\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
in which $c$ is a non-even non-odd parameter-free definable element. Find an
$\mathscr{L}_{\mathrm{OR}}$ formula $\delta(x)$ that defines $c$ in $M$.
Define $\varphi_{0}(x)$ to be

$\exists{{!}y}\ {\delta(y)}\rightarrow\exists{y}\ {(\delta(y)\wedge x<y)},$

and let $\varphi(x)$ be

$\exists{s}\ {\exists{\ell}\
{\bigl{(}\varphi_{0}((s)_{0})\wedge(s)_{\ell}=x\wedge\forall{i{<}{\ell}}\
{\bigl{(}(s)_{i+1}=2(s)_{i}\vee(s)_{i+1}=2(s)_{i}+1\bigr{)}}\bigr{)}}},$

where $(s)_{i}=x$ is the $\mathscr{L}_{\mathrm{OR}}$ formula expressing “the
$i$th element in the sequence coded by $s$ is $x$” in our proof of Proposition
24. Then $\varphi(x)$ is p-inductive by construction. Notice
$M\models\forall{x{<}{c}}\ {\varphi_{0}(x)}$. So $M\models\forall{x{<}{c}}\
{\varphi(x)}$ because
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\forall{x}\
{(\varphi_{0}(x)\rightarrow\varphi(x))}$. However, every element $x\in M$
satisfying $\varphi(x)$ must lie strictly below $c$ or be either even or odd.
Hence $M\models\neg\varphi(c)$ by our choice of $c$. We thus know $\varphi(x)$
is not $<$-inductive.

######  Remark 26.

All results in this paper about base-2 polynomial induction generalize to
other bases. Let us say an $\mathscr{L}_{\mathrm{OR}}$ formula $\varphi(x)$ is
_$(n+2)$ -p-inductive_, where $n\in\mathbb{N}$, if

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\varphi(0)\wedge\forall{x}\
{\Bigl{(}\varphi(x)\rightarrow\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{k<n+2}\varphi\bigl{(}(n+2)x+k\bigr{)}\Bigr{)}}.$

In this terminology, the p-inductive formulas are precisely the
$2$-p-inductive formulas. Let $m,n\in\mathbb{N}$. Then $n+2$ being a power of
$m+2$ is a necessary and sufficient condition for every $(m+2)$-p-inductive
formula to be $(n+2)$-p-inductive. We omit the proof here.

##  8\. Removing the order from the language

Another aspect of our formulation of ITP is that we search for an inductive
formula in the same language as the input sentence. In this section we
consider a restriction of the language of the inductive formula. Since most of
our arguments about $\mathrm{I}\mathrm{Open}$ depend on the presence (or, in
fact, the quantifier-free definability) of the order $<$ in
$\mathscr{L}_{\mathrm{OR}}$, it is natural to ask whether
$\mathrm{I}\mathrm{Open}$ really becomes strictly weaker when the induction
scheme is restricted to formulas in which $<$ does not appear. It turns out
that the induction scheme for quantifier-free formulas in this restricted
language is already provable in the base theory
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
According to Shepherdson [She67, page 27], this fact was first observed by M.
D. Gladstone. A stronger result was established by Shepherdson [She67, Theorem
2], who proved the same scheme from a weak subtheory of
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
If one starts from
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$,
then one can actually prove the least number principle (also known as the
scheme of strong induction, cf. Proposition 11(ii) and Theorem 13(ii)) for
quantifier-free formulas in the restricted language. This was pointed out by
Richard Kaye in a conversation in April 2016. With Kaye’s permission, we
include his proof here. Many ideas in the proof were already present in
Shepherdson’s contribution [She64] to Theorem 13.

Denote the language $\\{0,1,{+},{\times}\\}$ for rings by
_$\mathscr{L}_{\mathrm{R}}$_. Define

$\mathrm{I}\mathrm{Open}(\mathscr{L}_{\mathrm{R}})=\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is a quantifier-free $\mathscr{L}_{\mathrm{R}}$~{}formula}\\}.$

Let _$\mathrm{L}\mathrm{Open}(\mathscr{L}_{\mathrm{R}})$_ be the theory
axiomatized by
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$
and the scheme

$\forall{\bar{z}}\ {\bigl{(}\forall{y}\ {\bigl{(}\forall{x{<}{y}}\
{\theta(x,\bar{z})\rightarrow\theta(y,\bar{z})}\bigr{)}}\rightarrow\forall{x}\
{\theta(x,\bar{z})}\bigr{)}},$

where $\theta$ ranges over quantifier-free $\mathscr{L}_{\mathrm{R}}$
formulas.

The following elementary algebraic fact plays a key role in Kaye’s proof.

######  Lemma 27.

Let $F$ be a field. For every polynomial $p(x,\bar{a})$ in a single variable
$x$ with coefficients $\bar{a}\in F$, the set $\\{x\in F:p(x,\bar{a})=0\\}$ is
either finite or equal to $F$. ∎

######  Theorem 28 (Kaye).

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}\vdash\mathrm{L}\mathrm{Open}(\mathscr{L}_{\mathrm{R}})$.

######  Proof 8.1.

Let
$M\models\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$.
We will show $M\models\mathrm{L}\mathrm{Open}(\mathscr{L}_{\mathrm{R}})$. Fix
$\bar{a}\in M$. Consider a quantifier-free $\mathscr{L}_{\mathrm{R}}$ formula
$\theta(x,\bar{z})$. Put $\neg\theta(x,\bar{z})$ in disjunctive normal form

$\operatorname*{\mathchoice{\bigvee\mkern-16.5mu\bigvee}{\bigvee\mkern-12.0mu\bigvee}{\bigvee\mkern-13.0mu\bigvee}{\bigvee\mkern-11.0mu\bigvee}}_{i\leqslant
m}\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{j\leqslant
n}\bigl{(}p_{ij}(x,\bar{z})=0\wedge q_{ij}(x,\bar{z})\not=0\bigr{)},$

where the $p_{ij}$’s and the $q_{ij}$’s are polynomials over $\mathbb{Z}$. It
suffices to show that for each $i\leqslant m$, if some $x\in M$ satisfies
$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{j\leqslant
n}\bigl{(}p_{ij}(x,\bar{a})=0\wedge q_{ij}(x,\bar{a})\not=0\bigr{)}$, then
there is a least such $x$. So for notational convenience, let us assume $m=0$,
so that $\neg\theta(x,\bar{z})$ becomes

$\operatorname*{\mathchoice{\bigwedge\mkern-16.5mu\bigwedge}{\bigwedge\mkern-12.0mu\bigwedge}{\bigwedge\mkern-13.0mu\bigwedge}{\bigwedge\mkern-11.0mu\bigwedge}}_{j\leqslant
n}\bigl{(}p_{0j}(x,\bar{z})=0\wedge q_{0j}(x,\bar{z})\not=0\bigr{)}.$

Since $M$ is the non-negative part of a discretely ordered ring, we can
further simplify the formula $\neg\theta(x,\bar{z})$ to

$p(x,\bar{z})=0\wedge q(x,\bar{z})\not=0$

by setting $p(x,\bar{z})=\sum_{j\leqslant n}(p_{0j}(x,\bar{z}))^{2}$ and
$q(x,\bar{z})=\prod_{j\leqslant n}q_{0j}(x,\bar{z})$.

Assume $M\models\forall{y}\ {\bigl{(}\forall{x{<}{y}}\
{\theta(x,\bar{a})\rightarrow\theta(y,\bar{a})}\bigr{)}}$. We will construct a
strictly decreasing sequence $(c_{\ell})_{\ell\in\mathbb{N}}$ of elements of
$M$ by recursion as follows. If $M\models\forall{x}\ {\theta(x,\bar{a})}$,
then we are done already. So suppose not, and take an arbitrary $c_{0}\in
M\models\neg\theta(c_{0},\bar{a})$. Next, suppose $c_{\ell}$ is found such
that $M\models\neg\theta(c_{\ell},\bar{a})$. Using our assumption, pick any
$c_{\ell+1}<c_{\ell}$ in $M$ with $M\models\neg\theta(c_{\ell+1},\bar{a})$ and
carry on.

The result of this construction is an infinite sequence
$c_{0}>c_{1}>c_{2}>\cdots$ of elements of $M$ such that
$p(c_{\ell},\bar{a})=0$ and $q(c_{\ell},\bar{a})\not=0$ for all
$\ell\in\mathbb{N}$. Lemma 27 then implies $p(x,\bar{a})$ is the zero
polynomial. Hence, actually $M\models\forall{x}\
{\bigl{(}\neg\theta(x,\bar{a})\leftrightarrow q(x,\bar{a})\not=0\bigr{)}}$. By
an external induction using our assumption in the previous paragraph, one sees
that $q(k,\bar{a})=0$ for all $k\in\mathbb{N}$. Applying Lemma 27 again, we
conclude $M\models\forall{x}\ {q(x,\bar{a})=0}$, as required.

The obvious argument [HP93, Lemma I.2.8] shows
$\mathrm{L}\mathrm{Open}(\mathscr{L}_{\mathrm{R}})\vdash\mathrm{I}\mathrm{Open}(\mathscr{L}_{\mathrm{R}})$.
Therefore, Lemma 14 and Theorem 28 tell us that
$\mathrm{I}\mathrm{Open}(\mathscr{L}_{\mathrm{R}})$ is strictly weaker than
$\mathrm{I}\mathrm{Open}$. In terms of computational problems we obtain that

$\textsc{ITPOpen}(\mathscr{L}_{\mathrm{R}})$ Input: A sentence $\sigma$
provable in $\mathrm{PA}$ Output: A quantifier-free $\mathscr{L}_{\mathrm{R}}$
formula $\theta(x,\bar{z})$ s.t.
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\mathrm{I}_{x}\theta\vdash\sigma$

is defined on strictly fewer inputs than

ITPOpen Input: A sentence $\sigma$ provable in $\mathrm{PA}$ Output: A
quantifier-free $\mathscr{L}_{\mathrm{OR}}$ formula $\theta(x,\bar{z})$ s.t.
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\mathrm{I}_{x}\theta\vdash\sigma$

To recover the strength of $\mathrm{I}\mathrm{Open}$, it suffices to have
induction for a single inequality.

######  Theorem 29 (Shepherdson).

$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}+\\{\mathrm{I}_{x}\theta:\text{$\theta(x,\bar{z})$
is an atomic
$\mathscr{L}_{\mathrm{OR}}$~{}formula}\\}\vdash\mathrm{I}\mathrm{Open}$.

######  Proof 8.2.

See page 83f in Shepherdson [She64].

##  9\. Conclusion

What do we learn from these results for the automation of inductive theorem
proving?

In comparison with successor induction and the uniform proof shape
$\textsc{ITP}_{\textsc{U}}$, both the use of $<$-induction and that of the
non-uniform proof shape ITP come at the price of introducing a universal
quantifier to the goals. However, both also come with a significant pay-off:
there are strictly more $<$-inductive formulas than $(n+1)$-inductive formulas
for any $n\in\mathbb{N}$. Similarly, the uniform proof shape
$\textsc{ITP}_{\textsc{U}}$ is not complete while the non-uniform proof shape
ITP is complete (with respect to $\mathrm{PA}$). Therefore, assuming the
theorem proving environment is able to deal with universal quantifiers in the
assumptions of a goal efficiently, these results clearly indicate to prefer
$<$-induction over $(n+1)$-induction for any $n\in\mathbb{N}$ and the ITP
proof shape over the $\textsc{ITP}_{\textsc{U}}$ proof shape.

As Theorem 8 shows, the non-uniform proof shape ITP can be restricted to the
non-uniform equivalence proof shape $\textsc{ITP}_{\textsc{Eq}}$ while
preserving completeness, thus strongly reducing the search space. Whether this
can be exploited for practical applications in inductive theorem proving is
unclear to the authors. What would be needed is a practically reasonable
procedure for generating universal formulas which are
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$-equivalent
to a given sentence. To the best of the authors’ knowledge, no such procedure
has been devised for use in inductive theorem proving yet. On a more
theoretical note, Theorem 8 shows that the essential difficulty of inductive
theorem proving does not lie in finding an inductive formula which is stronger
than the goal (in the sense that it implies the goal over
$\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{$\mathrm{PA}$}}^{\mathord{-}}}}$);
it is sufficient to find an inductive formula as strong as the goal. Instead,
the essential difficulty lies in the non-analyticity of the inductive formula
as discussed in Section 2.2.

The results of Section 8 illustrate the importance of the choice of the
language for the inductive formulas: allowing a single predicate symbol
defined using a single quantifier can increase the strength of the theory
considerably.

From a broader perspective, we believe that this paper demonstrates the
potential of the use of methods and results from mathematical logic, and in
particular, from theories of arithmetic, in inductive theorem proving. In our
opinion, a good illustration of this potential is provided by Proposition 23.
The construction of theorem-specific induction rules has a long history in
inductive theorem proving [BM79, BvHH+89, Ste88, BBHI05]. This approach is
typically justified empirically by demonstrating, in the context of a certain
algorithm or implementation, that the option to switch to another induction
rule allows to solve more goals than before (by that particular algorithm or
by a certain implementation within a certain timeout). Proposition 23 provides
a much more solid foundation to this approach: if there are strictly more
formulas which are inductive in sense X than in sense Y an algorithm for
inductive theorem proving can get trapped in a situation where the induction
formula currently under consideration allows a proof using rule X but does not
allow a proof using rule Y, regardless of which algorithm or implementation is
used, since there simply is no proof.

All of the results in this paper are restricted to arithmetical theories in
the strict sense, i.e., theories about the natural numbers. In inductive
theorem proving, one typically works in a broader syntactic setting of many-
sorted first-order logic with inductive data types such as lists, trees, etc.
Since many results about theories of arithmetic depend on results about
numbers, rings, etc., it is not straightforward to extend them to this more
general syntactic setting. Coding is not an option since it introduces an
amount of syntactic complication that is not realistic in inductive theorem
proving. However, for the continuation of the line of work in this paper we
consider such an extension of the model theory of arithmetic to be of high
importance. One prototypical problem along this line is to classify (some of)
the benchmark examples from the TIP suite [CJRS15] according to the weakest
induction schemes (e.g., atomic, quantifier-free) required to prove them.

We believe, as argued in Section 2, that the non-analyticity of induction
axioms is a key aspect of inductive theorem proving, so we have considered the
set of inductive formulas as the search space in our model. In the case of
theorem proving in pure first-order logic, the search space is quite well
understood theoretically and consequently we have very powerful tools at our
disposal for navigating in it such as (most general) unification, subsumption,
reduction orderings, (resolution) refinements, etc. At present, we do not seem
to have a similarly complete theoretical understanding of the set of inductive
formulas and how they relate to a given goal. We believe that further work in
this direction is crucial for advancing the state of the art in inductive
theorem proving.

##  10\. Acknowledgements

The authors are very grateful to Emil Jeřábek for pointing out some results in
the literature [Joh93, She64, She67] that answer several questions posed in an
earlier version of this paper. The authors would like to thank Zofia
Adamowicz, Alan Bundy, Richard Kaye, and Leszek Kołodziejczyk for illuminating
discussions around the topics of this paper. The authors would also like to
thank the anonymous reviewers whose insightful feedback has led to a
considerable improvement of this paper.

## References

  * [AdBO09] Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog.  Verification of Sequential and Concurrent Programs.  Texts in Computer Science. Springer-Verlag, Dordrecht, third, extended edition, 2009.  Reprinted with corrections, 2010.
  * [BBHI05] Alan Bundy, David Basin, Dieter Hutter, and Andrew Ireland.  Rippling: Meta-Level Guidance for Mathematical Reasoning, volume 56 of Cambridge Tracts in Theoretical Computer Science.  Cambridge University Press, Cambridge, 2005.
  * [BGP12] James Brotherston, Nikos Gorogiannis, and Rasmus L. Petersen.  A generic cyclic theorem prover.  In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, volume 7705 of Lecture Notes in Computer Science, pages 350–367, Berlin, 2012. Springer-Verlag.
  * [BM79] Robert S. Boyer and J. Strother Moore.  A Computational Logic.  ACM monograph series. Academic Press, New York, 1979.
  * [BM07] Aaron R. Bradley and Zohar Manna.  The Calculus of Computation: Decision Procedures with Applications to Verification.  Springer-Verlag, Berlin, 2007.
  * [BS11] James Brotherston and Alex Simpson.  Sequent calculi for induction and infinite descent.  Journal of Logic and Computation, 21(6):1177–1216, December 2011\.
  * [Bus86] Samuel R. Buss.  Bounded Arithmetic, volume 3 of Studies in Proof Theory, Lecture Notes.  Bibliopolis, Naples, 1986.  Revision of the 1985 Ph.D. thesis.
  * [Bus98a] Samuel R. Buss.  An Introduction to Proof Theory.  In Handbook of Proof Theory [Bus98c], pages 2–78.
  * [Bus98b] Samuel R. Buss.  First-Order Proof Theory of Arithmetic.  In Handbook of Proof Theory [Bus98c], pages 79–147.
  * [Bus98c] Samuel R. Buss, editor.  Handbook of Proof Theory, volume 137 of Studies in Logic and the Foundations of Mathematics.  Elsevier, Amsterdam, 1998.
  * [BvHH+89] Alan Bundy, Frank van Harmelen, Jane Hesketh, Alan Smaill, and Andrew Stevens.  A rational reconstruction and extension of recursion analysis.  In N. S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence (IJCAI-89), volume 1, pages 359–365, San Francisco, 1989. Morgan Kaufmann Publishers.
  * [CJRS13] Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone.  Automating inductive proofs using theory exploration.  In Maria Paola Bonacina, editor, Automated Deduction — CADE-24, volume 7898 of Lecture Notes in Computer Science, pages 392–406, Berlin, 2013. Springer-Verlag.
  * [CJRS15] Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone.  TIP: Tons of inductive problems.  In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 333–337, Cham, 2015. Springer-Verlag.
  * [Com01] Hubert Comon.  Inductionless induction.  In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 14, pages 913–962. Elsevier, Amsterdam, 2001.
  * [Cru15] Simon Cruanes.  Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond.  PhD thesis, École Polytechnique, Palaiseau, France, 2015.
  * [DKR11] Alastair F. Donaldson, Daniel Kroening, and Philipp Rümmer.  Automatic analysis of DMA races using model checking and $k$-induction.  Formal Methods in System Design, 39(1):83–113, 2011.
  * [EHR+16] Gabriel Ebner, Stefan Hetzl, Giselle Reis, Martin Riener, Simon Wolfsteiner, and Sebastian Zivota.  System description: GAPT 2.0.  In Nicola Olivetti and Ashish Tiwari, editors, 8th International Joint Conference on Automated Reasoning (IJCAR), volume 9706 of Lecture Notes in Computer Science, pages 293–301. Springer, 2016.
  * [Gen54] Gerhard Gentzen.  Zusammenfassung von mehreren vollständigen Induktionen zu einer einzigen.  Archiv für mathematische Logik und Grundlagenforschung, 2(1):1–3, January 1954.
  * [HP93] Petr Hájek and Pavel Pudlák.  Metamathematics of First-Order Arithmetic.  Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1993.
  * [IB96] Andrew Ireland and Alan Bundy.  Productive Use of Failure in Inductive Proof.  Journal of Automated Reasoning, 16(1–2):79–111, 1996.
  * [Jeř12] Emil Jeřábek.  Sequence coding without induction.  Mathematical Logic Quarterly, 58(3):244–248, May 2012.
  * [Joh93] Jan Johannsen.  On the weakness of sharply bounded polynomial induction.  In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, volume 713 of Lecture Notes in Computer Science, pages 223–230, Berlin, 1993. Springer-Verlag.
  * [Joo15] Joost J. Joosten.  Turing jumps through provability.  In Arnold Beckmann, Victor Mitrana, and Mariya Soskova, editors, Evolving Computability, volume 9136 of Lecture Notes in Computer Science, pages 216–225, Cham, 2015. Springer-Verlag.
  * [Kay90] Richard Kaye.  Diophantine induction.  Annals of Pure and Applied Logic, 46(1):1–40, January 1990.
  * [Kay91] Richard Kaye.  Models of Peano Arithmetic, volume 15 of Oxford Logic Guides.  Clarendon Press, Oxford, 1991.
  * [KP13] Abdelkader Kersani and Nicolas Peltier.  Combining superposition and induction: A practical realization.  In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems, volume 8152 of Lecture Notes in Computer Science, pages 7–22, Berlin, 2013. Springer-Verlag.
  * [PB12] Lawrence C. Paulson and Jasmin Christian Blanchette.  Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.  In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, The 8th International Workshop on the Implementation of Logics (IWIL), 2010, volume 2 of EPiC Series in Computing, pages 1–11. EasyChair, 2012\.
  * [She64] John C. Shepherdson.  A non-standard model for a free variable fragment of number theory.  Bulletin de l’Académie Polonaise des Sciences. Série des Sciences Mathématiques, Astronomiques et Physiques, XII(2):79–86, 1964.
  * [She67] John C. Shepherdson.  The rule of induction in the three variable arithmetic based on $+$ and $\times$.  Annales de la Faculté des Sciences de l’Université de Clermont. Mathématiques, 35(4):25–31, 1967.
  * [SSS00] Mary Sheeran, Satnam Singh, and Gunnar Stålmarck.  Checking Safety Properties Using Induction and a SAT-Solver.  In Warren A. Hunt Jr. and Steven D. Johnson, editors, Third International Conference on Formal Methods in Computer-Aided Design (FMCAD), volume 1954 of Lecture Notes in Computer Science, pages 108–125. Springer, 2000.
  * [Ste88] Andrew Stevens.  A rational reconstruction of Boyer and Moore’s technique for constructing induction formulas.  In Yves Kodratoff, editor, ECAI 88, pages 565–570, London, 1988\. Pitman Publishing.
  * [Sut16] Geoff Sutcliffe.  The CADE ATP System Competition - CASC.  AI Magazine, 37(2):99–101, 2016.
  * [Vis05] Albert Visser.  Faith & falsity.  Annals of Pure and Applied Logic, 131(1–3):103–131, January 2005\.
  * [Vis14] Albert Visser.  Peano Corto and Peano Basso: A study of local induction in the context of weak theories.  Mathematical Logic Quarterly, 60(1–2):92–117, February 2014.
  * [Wal92] Christoph Walther.  Computing induction axioms.  In Andrei Voronkov, editor, Logic Programming and Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 381–392, Berlin, 1992. Springer-Verlag.
  * [WP87] Alex J. Wilkie and Jeff B. Paris.  On the scheme of induction for bounded arithmetic formulas.  Annals of Pure and Applied Logic, 35:261–302, 1987.
  * [WW] Daniel Wand and Christoph Weidenbach.  Automatic induction inside superposition.  Available at http://people.mpi-inf.mpg.de/~dwand/datasup/d.pdf.