Some observations on the logical foundations of inductive theorem proving
Stefan Hetzl, Tin Lok Wong
TL;DR
This paper explores the logical foundations of automated inductive theorem proving by developing a theoretical model to analyze the selection of induction axioms, proof shapes, rules, and formulas, clarifying their interrelations.
Contribution
It introduces a new theoretical model centered on the difficulty of finding sufficient induction axioms and clarifies the relationships between different notions of inductiveness in the literature.
Findings
Model highlights the importance of induction axiom selection
Analysis of proof shape and induction rule choices
Clarification of inductiveness notions via model-theoretic techniques
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 arXiv:1704.01930v5 published originally on Nov.~16, 2017.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
\lmcsheading
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
and
Tin Lok Wong
Kurt Gödel Research Center for Mathematical Logic
University of Vienna
Währinger Straße 25
AT-1090 Vienna
Austria
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 (). Robinson’s 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 as the base theory in this paper. First, if one adopts 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,
[TABLE]
are not provable in ; 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 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 . Nevertheless, many other results in this paper, for example, Theorem 8, Proposition 9 and Lemma 19, remain true over . {defi} Denote the language for ordered rings by . Abusing notation, if , then we denote the closed term
[TABLE]
by . 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.
- (P1)
\forall{x}\ {\forall{y}\ {\forall{z}\ {\bigl{(}(x+y)+z=x+(y+z)\bigr{)}}}}. 2. (P2)
. 3. (P3)
\forall{x}\ {\forall{y}\ {\forall{z}\ {\bigl{(}(x\times y)\times z=x\times(y\times z)\bigr{)}}}}. 4. (P4)
. 5. (P5)
. 6. (P6)
. 7. (P7)
. 8. (P8)
. 9. (P9)
. 10. (P10)
. 11. (P11)
. 12. (P12)
. 13. (P13)
. 14. (P14)
. 15. (P15)
. 16. (P16)
.
Here is an abbreviation for .
{defi}
If is an formula, then the induction axiom for with respect to the variable , denoted by or simply , is the sentence
[TABLE]
Define
[TABLE]
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 . For a theory and a formula , if and only if there is a finite set and an LK-proof of the sequent . Gentzen’s cut-elimination theorem states that:
Theorem 1**.**
If there is an LK-proof of a sequent , then there is a cut-free LK-proof of .
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 is an instance of a subformula of a formula that occurs in . 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 then there is a finite and a cut-free LK-proof of the sequent .
So we see that in the sense of the above corollary, inductive theories do allow cut-elimination. However, may contain induction axioms on induction formulas which are not instances of subformulas of , 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 sentence. More specifically, for all there is a sentence expressing the consistency of , see for example [Bus98b]. We then have:
Theorem 3**.**
For all : but .
Note that this result embodies a very strong non-analyticity requirement: given any , in order to prove not only do we need a non-analytic induction formula, but we need one with more than quantifier alternations even though is only a sentence.
This theorem entails the necessity of cut in the following sense. First, formulate induction as the inference rule
[TABLE]
with the usual side condition and being an arbitrary formula. Observe that if and only if there is an -proof of \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}\longrightarrow\varphi. Now, in contrast to LK, the calculus does not have cut-elimination:
Corollary 4**.**
There is a formula such that \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}\longrightarrow\varphi has an -proof but no cut-free -proof.
Proof 2.1**.**
Let for any . Then, by Theorem 3, and consequently there is an -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 -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 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 -proof translate to instances (in the sense of second-order logic) of the second-order induction axiom. Thus a -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 such that . 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 , there are, in theory, the following options for generating (non-analytic) induction axioms which suffice to prove . (1) One can use coding, for example as in the proof of the finite axiomatizability of in [HP93, Theorem I.2.52]. Thus one can formulate the theorem-proving problem in (for a 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 , sufficiently high for practical purposes, so that we are interested only in finding proofs whose induction axioms contain at most 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 which are input to an inductive theorem prover: if it is feasible to find simple formulas 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 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 and the induction formulas 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 minute per proof using, on average, 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. {defi} An formula 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 is an inductive formula, then is trivially equivalent over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} to the induction axiom
[TABLE]
Therefore, sentences of the form , where 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 be an formula. Define to be
[TABLE]
Then 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 is inductive. Work over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. We have trivially. Suppose is such that holds, and take such that the hypothesis in holds, i.e.,
[TABLE]
Then must be true since , and thus is also true by the second conjunct displayed above. This shows .
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 . Take such that
[TABLE]
We want . So pick any . We know holds by hypothesis. Thus by the definition of , as required.
Conversely, assume holds, i.e.,
[TABLE]
Let be arbitrary. We want . So take any 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 , 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 formulas , there is an inductive formula 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 and 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 . Define . As and are both inductive, it is easy to see that is inductive too. Moreover, the sentence implies and thus also over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}.
The above proof straightforwardly generalizes to an arbitrary number of formulas and so we obtain:
Corollary 7**.**
Let be an sentence. Then if and only if there is an inductive formula 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 provable in
Output:
An inductive formula 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 and ). But of course, implicitly, we take the perspective of wanting to compute such a from a given . 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 . 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 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 be an sentence. Then if and only if there is an inductive formula 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 such that \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}\vdash\forall{x}\ {\psi(x)}\rightarrow\sigma. We verify that
[TABLE]
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 . Since \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}\vdash\forall{x}\ {\psi(x)}\rightarrow\sigma, this implies . If is such that , then and so . 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 is inductive because it is equivalent to either or depending on whether holds or not, and both and 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 sentence is equivalent to a consistency statement. This result motivates the consideration of the equivalence version of ITP:
Input:
A sentence provable in
Output:
An inductive formula 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 is a total relation in the sense that for every input there is an output as required. However, for a fixed the ’s permitted in 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 . 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 , i.e., , and seeking an inductive formula 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 -provable formulas.
Proposition 9**.**
There is an formula such that but no inductive formula 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 sentence that is provable in but not in \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. Consider the formula , which is defined to be
[TABLE]
Then because . 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 by the definition of . Therefore, for no formula can
[TABLE]
As a result, the following uniform version of ITP
Input:
A sentence provable in
Output:
An inductive formula 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 sentences provable in a sufficiently weak fragment of , as the following theorem shows.
{defi}
An formula is bounded if all the quantifiers it contains are of the form or , where is a term in that does not involve the variable . Bounded formulas are also called formulas. The theory is
[TABLE]
Fix a bounded formula such that
[TABLE]
Let be the axiom .
See Section V.3(c) in Hájek–Pudlák [HP93], for example, for a construction of the formula .
Theorem 10** (Wilkie–Paris).**
The following are equivalent for a bounded formula .
- (i)
. 2. (ii)
There is an inductive formula 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
{defi}
Let be an formula. We define the following induction axioms:
- •
The -induction axiom is
[TABLE]
- •
Let . The -step induction axiom \mathrm{I}^{\text{(n+1)-step}}_{x}\theta is
[TABLE]
- •
Let . The -induction axiom is
[TABLE]
- •
The polynomial induction axiom is
[TABLE]
Each of these schemes naturally induces a notion of inductiveness. {defi} Let be an formula with precisely one free variable .
- •
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 . We say is -step inductive if
[TABLE]
- •
Let . We say is -inductive if
[TABLE]
- •
is polynomially inductive, or simply p-inductive, if
[TABLE]
The first of the above formulations, -induction, is also known as strong induction and is commonly used in mathematics. The consideration of -step induction is motivated by its use in [BBHI05]. The -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 :
- (i)
\mathrm{PA}=\mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}+\{\mathrm{I}_{x}\theta:\text{\theta(x,\bar{z})\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})\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})\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})\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})\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 and . 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*
- (a)
, 2. (b)
, 3. (c)
, 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 ,* 5. (e)
, and 6. (f)
.
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 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 , then axiom P16 implies , and so we get the we want by P14.
Theorem 13** (mostly Shepherdson).**
The following are equivalent for all :
- (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})\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})\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})\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})\mathscr{L}_{\mathrm{OR}}~{}formula}\}.
Proof 4.2**.**
We refer the reader to the original Shepherdson paper [She64] for a proof of . 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 . Work over (ii). Fix and let be a quantifier-free formula such that . Use (ii) to find . If , then by Lemma 12(d). So suppose . Then by (the contrapositive of) Lemma 12(c). Apply axiom P14 to find such that . Then holds by the minimality of , but , as required.
The implication is clear.
Consider . Work over (iv). Fix and let be a quantifier-free formula such that \theta(0,\bar{z})\wedge\forall{x}\ {\bigl{(}\theta(x,\bar{z})\rightarrow\theta(x+1,\bar{z})\bigr{)}}. Then
[TABLE]
and so we are done by (iv).
The following small lemma will be handy when proving the quantifier-free analogue of of Proposition 11.
Lemma 14**.**
- (a)
, 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 . Take any with . Using the axioms of \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} and Lemma 12(f), one can routinely verify that . Apply induction on for the atomic formula to find which satisfies . Then setting gives us what we want.
For the unprovability part, consider the set of all elements of the polynomial ring 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,
[TABLE]
Proposition 15**.**
* proves*
[TABLE]
for every quantifier-free formula .
Proof 4.4**.**
Work over . Let be a quantifier-free formula and be parameters such that . By Proposition 13(ii), this has a least witness, say . If , then . So suppose . Using Lemma 14, find such that or . Since , we know by Lemma 12(f) and axiom P14. So by the minimality of . We are thus done because .
Following the proof of Theorem V.4.6 in Hájek–Pudlák [HP93], one can prove from \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} plus the polynomial induction scheme for formulas of the form where is a quantifier-free formula and is an term not involving . 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})\mathscr{L}_{\mathrm{OR}}~{}formula}\}* does not prove . Consequently, it is strictly weaker than .*
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 one needs in establishing Theorem 8.
{defi}
Let be a language. Denote by the language obtained from by adding one new unary predicate symbol . Let be a sentence in . If is an formula, then define to be the universal closure of the formula obtained from by replacing each occurrence of by . The scheme determined by , denoted , is defined to be . The scheme is mergeable over an theory if for all formulas , there is an formula such that .
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 . Let be a scheme and be an theory such that . The following are equivalent.
- (i)
* is mergeable over .* 2. (ii)
For every sentence provable from , there exists an formula such that .
Proof 4.6**.**
For , imitate the proof of Theorem 8. Conversely, suppose (ii) holds. Pick arbitrary formulas and . Define . Then trivially. By (ii), we get an formula such that and hence , as required.
Corollary 18**.**
Let and let be an sentence. The following are equivalent.
- (i)
. 2. (ii)
There is a -inductive formula 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 -step inductive formula 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 -inductive formula 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 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 is a finite set of natural numbers and is a finite set of terms, then define to be the theory axiomatized by \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} and the following axioms for all formulas :
[TABLE]
In this terminology, the -step induction scheme in Proposition 11(iii) is essentially
[TABLE]
(Some choices of and may give rise to a scheme that is not true in , but this does not concern us here.) Walther observed that if and , then .
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 such that . Then
[TABLE]
by Proposition 11. Clearly .
Thanks to Theorem 13, the observation in the previous paragraph has an analogue in the quantifier-free context. We formulate this as follows. If is a finite set of natural numbers and is a finite set of terms, then define to be the theory axiomatized by \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} and the following axioms for all quantifier-free formulas :
[TABLE]
Clearly, if and , then . The converse is not true because whenever such that , we have
[TABLE]
by Theorem 13, but .
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]. {defi} A cut is an inductive formula such that
[TABLE]
An a-cut is a cut such that
[TABLE]
An am-cut is an a-cut such that
[TABLE]
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 formulas and such that
- (1)
* 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 which contains a nonstandard element that is definable by a bounded formula. For instance, if , then we can take to be the least (code of a) proof of contradiction from in . Fix a bounded formula such that . Notice
[TABLE]
is an initial segment of , and whenever . So is itself an structure. Since is a bounded formula, it is straightforward [HP93, Remark IV.1.18] to check that is the unique element which satisfies in . We know because is preserved under taking initial segments [HP93, Remark IV.1.21]. Thus
[TABLE]
is an initial segment of that is closed under because
[TABLE]
as verified in Hájek–Pudlák [HP93, Lemma V.3.8(iii) and page 302]. We know contains but not because
[TABLE]
and . In particular, it is not closed under . The whole situation in can be captured by the sentence
[TABLE]
where denotes the formula . Clearly,
[TABLE]
have the properties we want.
Corollary 20**.**
- (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 and be as given by Lemma 19.
- (a)
Take . 2. (b)
Take . 3. (c)
Take .
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. {qu} Let 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 such that \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} proves
[TABLE]
and is not an am-cut?
6. Comparing solutions
Given a -theorem , our formulation of ITP considers the set of solutions, the search space, to be all inductive 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 and .
There are (at least) two ways of comparing two induction axioms and , where and are inductive formulas. The first way is to say is stronger than 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 is stronger than 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 such that \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} proves
[TABLE]
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 be as given by Lemma 19. We show that and have the properties we want.
As is an a-cut, it is not hard to check that 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 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 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 is itself. The proposition above says that this is not the case if we adopt the second way of comparing induction axioms: may be provable from another induction axiom where is a strictly weaker than 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 in this sense. We do not know the answer.
{qu}
Let 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 such that \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} proves
[TABLE]
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 and ask with respect to which induction schemes it is inductive. Let be any notion of inductiveness defined in Section 4. Then we can state the computational problem
Input:
A sentence provable in
Output:
An -inductive formula 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 are equivalent for all 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 -step inductive formulas are -step inductive, and not all -step inductive formulas are -step inductive. The following proposition lists all the implications we can establish.
Proposition 22**.**
Let .
- (a)
The following are equivalent for a formula: it is inductive; it is -step inductive; and it is -inductive. 2. (b)
If divides , then all -step inductive formulas are -step inductive. 3. (c)
If , then all -inductive formulas are -inductive. 4. (d)
All -step inductive formulas are -inductive. 5. (e)
If a formula is -inductive for some , then it is -inductive. 6. (f)
A formula is -inductive if and only if is inductive.
Proof 7.1**.**
Parts (a)–(d) are easy exercises.
- (e)
Suppose is -inductive. Work over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. Let be such that . If , then holds by Lemma 12(d) because is -inductive. So suppose . Use axiom P14 to find such that . Then because for each by P14 again. As is -inductive and , this implies . 2. (f)
First, assume is inductive. Work over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. Let be such that . If , then by our assumption. So suppose . Apply Lemma 12(f) to find such that . Notice by Lemma 12(e). Our assumption then implies , which, in particular, tells us that .
Conversely, suppose 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 trivially by -inductiveness. So . Let be such that . Then Lemma 12(c) and (a) imply and so by -inductiveness. This shows , 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 “-step inductive”s, and the “-inductive”s.
Proposition 23**.**
Let .
- (a)
If does not divide , then there is an -step inductive formula that is not -step inductive. 2. (b)
If , then there is an -inductive formula that is not -inductive. 3. (c)
If , then there is an -inductive formula that is not -step inductive. 4. (d)
There is a -inductive formula that is not -inductive.
Proof 7.2**.**
Let and be formulas given by Lemma 19. Recall 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).
- (a)
Assume all -step inductive formulas are -step inductive. Consider the formula
[TABLE]
We first show that is -step inductive. By our assumption on and , this will imply is -step inductive. Work over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. We know because is inductive. Take satisfying . If is such that , then by P8 and P5, and thus . So suppose . Then holds by the definition of the formula . As is an inductive formula, this implies and hence .
Now look at our model . Let , so that . Notice by condition (3) in Lemma 19. So because is a cut and by axiom P14. However, the previous paragraph tells us that . So by the definition of .
Find such that . By axiom P14, we know . So Lemma 12(b) implies . Apply axiom P14 to find such that . Then
[TABLE]
and thus by axioms P11 and P12. Now . Hence by axiom P14. Lemma 12(d) then tells us . We can thus conclude that divides , which is what we want. 2. (b)
We show that the formula
[TABLE]
is an example we want.
Suppose . We show that is -inductive. Work over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. If , then by condition (2) in Lemma 19, and so we are done by Proposition 22(a) and (c). So suppose . Since is inductive, we know . Let be such that . Take . We know by axiom P12, and since is a cut and . These together imply . So because holds. As the choice of is arbitrary, we know by the definition of . It follows that because is inductive. Hence .
We now show that is not -inductive using our model . The definition of tells us . On the one hand, notice by condition (3) in Lemma 19. Also by axiom P14. Hence since is a cut. On the other hand, notice for any by axiom P12. These together say that . 3. (c)
We claim that the formula
[TABLE]
has the desired properties.
To show that is -inductive, let us work over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. As in the previous part, we assume . Since is inductive, we know . Let be such that . As , we know in particular. Notice because is a cut and by condition (3) in Lemma 19. Also by Lemma 12(e). Thus holds, from which one deduces . This implies by the definition of . Since is inductive, we conclude that .
To show that is not -step inductive, we use as in the proof of (b). Notice by the definition of . On the one hand, we know by condition (3) in Lemma 19. Also by axiom P14. Hence since is a cut. On the other hand, we know by P14. These together say that . 4. (d)
It suffices to prove that the formula defined in the proof of (b) is -inductive.
Work over \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}. Let be such that and . We will show . If , then because is inductive, and so holds. Therefore, assume . Apply Lemma 12(f) to find such that . Notice by Lemma 12(e). So, by the choice of , we know .
Consider the case when . Then by condition (3) in Lemma 19. This implies because is inductive. Use Lemma 12(f) to find such that . Then since is inductive and holds. Also, Lemma 12(e) implies for each . We thus know by the definition of . Our assumption on then implies . Thus for any by axiom P9, and so must hold.
If , then by conditions (1) and (2) in Lemma 19. So in either case because holds. Since is inductive, we deduce and hence , as required.
Buss’s notion of polynomial induction does not fit well into the picture.
Proposition 24**.**
- (a)
There is a formula that is -step inductive for every but is not p-inductive. 2. (b)
For every , there is a p-inductive formula that is not -inductive.
Proof 7.3**.**
- (a)
By Corollary 20(b), there is a cut that is not an a-cut. Such a cut is -step inductive for every , but it is not p-inductive. 2. (b)
Let be formulas given by Lemma 19. Define to be the formula
[TABLE]
Here is the formula expressing “the th element in the sequence coded by is ” 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 is p-inductive. However, the formula is not -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.
- (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 be any 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 , then \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}\nvdash\varphi(0) and we are done. So suppose . Notice . It is, therefore, a parameter-free definable element of . The failure of (ii) then gives us such that or . By Lemma 12(f) and axiom P14, we know . Hence by the minimality of . This shows 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 is a non-even non-odd parameter-free definable element. Find an formula that defines in . Define to be
[TABLE]
and let be
[TABLE]
where is the formula expressing “the th element in the sequence coded by is ” in our proof of Proposition 24. Then is p-inductive by construction. Notice . So because \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}\vdash\forall{x}\ {(\varphi_{0}(x)\rightarrow\varphi(x))}. However, every element satisfying must lie strictly below or be either even or odd. Hence by our choice of . We thus know is not -inductive.
Remark 26**.**
All results in this paper about base-2 polynomial induction generalize to other bases. Let us say an formula is -p-inductive, where , if
[TABLE]
In this terminology, the p-inductive formulas are precisely the -p-inductive formulas. Let . Then being a power of is a necessary and sufficient condition for every -p-inductive formula to be -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 depend on the presence (or, in fact, the quantifier-free definability) of the order in , it is natural to ask whether 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.
{defi}
Denote the language for rings by . Define
[TABLE]
Let be the theory axiomatized by \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}} and the scheme
[TABLE]
where ranges over quantifier-free formulas.
The following elementary algebraic fact plays a key role in Kaye’s proof.
Lemma 27**.**
Let be a field. For every polynomial in a single variable with coefficients , the set is either finite or equal to . ∎
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 . Fix . Consider a quantifier-free formula . Put in disjunctive normal form
[TABLE]
where the ’s and the ’s are polynomials over . It suffices to show that for each , if some 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 . So for notational convenience, let us assume , so that becomes
[TABLE]
Since is the non-negative part of a discretely ordered ring, we can further simplify the formula to
[TABLE]
by setting and .
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 of elements of by recursion as follows. If , then we are done already. So suppose not, and take an arbitrary . Next, suppose is found such that . Using our assumption, pick any in with and carry on.
The result of this construction is an infinite sequence of elements of such that and for all . Lemma 27 then implies 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 for all . Applying Lemma 27 again, we conclude , as required.
The obvious argument [HP93, Lemma I.2.8] shows . Therefore, Lemma 14 and Theorem 28 tell us that is strictly weaker than . In terms of computational problems we obtain that
Input:
A sentence provable in
Output:
A quantifier-free formula 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 provable in
Output:
A quantifier-free formula s.t. \mathord{\mathrel{\mathrm{PA}}\joinrel\mathrel{\mbox{\vphantom{\mathrm{PA}}}^{\mathord{-}}}}+\mathrm{I}_{x}\theta\vdash\sigma
To recover the strength of , 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})\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 , 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 -inductive formulas for any . Similarly, the uniform proof shape is not complete while the non-uniform proof shape ITP is complete (with respect to ). 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 -induction for any and the ITP proof shape over the proof shape.
As Theorem 8 shows, the non-uniform proof shape ITP can be restricted to the non-uniform equivalence proof shape 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.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[Ad BO 09] 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.
- 2[BBHI 05] 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.
- 3[BGP 12] 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.
- 4[BM 79] Robert S. Boyer and J. Strother Moore. A Computational Logic . ACM monograph series. Academic Press, New York, 1979.
- 5[BM 07] Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification . Springer-Verlag, Berlin, 2007.
- 6[BS 11] James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation , 21(6):1177–1216, December 2011.
- 7[Bus 86] Samuel R. Buss. Bounded Arithmetic , volume 3 of Studies in Proof Theory, Lecture Notes . Bibliopolis, Naples, 1986. Revision of the 1985 Ph.D. thesis.
- 8[Bus 98a] Samuel R. Buss. An Introduction to Proof Theory. In Handbook of Proof Theory [ Bus 98c ] , pages 2–78.