This is meant to be a light post, posing a perhaps naive question. One of the hallmarks of computational proof theory is the association between arithmetic theories and complexity classes, in terms of their provably recursive functions. But is there a general rule for identifying the provably recursive functions of a class of induction invariants?
Consider the following well-known result of Parsons:
Theorem 1 ([1]). If
, for
, then
computes the graph of a primitive recursive function in the standard model
.
Conversely, for every primitive recursive function, there is a
formula
computing the graph of
such that
.
Edit (31 Dec 2020): both Takeuti and Mints independently discovered this particular result, see the comment from Ulrik Buchholtz below the post.
The motto is:
Now let us consider Buss’ theory , which extends some basic universal axioms by ‘
polynomial-induction’, – think of this as over only
-predicates. The notable witnessing theorem here is:
Theorem 2 ([2]). If
, for
, then
computes the graph of a polynomial-time function in the standard model
.
Conversely, for every polynomial-time function
, there is a
formula
computing the graph of
such that
.
Notice the similarity? Here the motto is:

Such theorems establish a link between some ‘non-deterministic’ predicate class and a ‘deterministic’ function class. However notice that determining a corresponding pair does not seem to be obvious. For the non-deterministic class is obtained by extending the deterministic one by bounded search, whereas for
it is .
Less obvious examples
To throw more spanners into the works, here are some other
:- Induction on arithmetical predicates (i.e.
) corresponds to the Gödel primitive recursive functionals. (via, say, Gödel’s functional interpretation of arithmetic, [3])
- Structural induction on
predicates corresponds to
. ([2])
For me, at least, the general relationship between a class of induction invariants and its provably recursive functions is not clear. One observation is that, as a theory gets more expressive, the corresponding deterministic and nondeterministic classes seem to become further apart, as we have seen from the examples thus far.
A high-level question
Let me pose a somewhat vaguely worded, yet I believe meaningful, question:
Question 3. Given a ‘well-behaved’ ‘non-deterministic’ class
what are, , the provably recursive functions of
?
Conversely, given a ‘well-behaved’ class of functions
, what is the ‘largest non-deterministic’ ‘well-behaved’ class of formulas
such that
corresponds to
?
Here I have put in inverted commas what I am not ready to formally define: an appropriate answer should address these notions too. For all I know, a general answer might indeed be well-known and/or (un)written, but it seems that published works typically focus on only special cases of and
above.
Beyond nondeterminism
The question above is arguably not so robust, since induction for a well-behaved class, say , is typically conservatively extended by induction over, say, Boolean combinations over
. In fact we can go further, e.g.:
Proposition 4.
is
-conservative over
. Thus the provably recursive functions of
are precisely the primitive recursive functions.
This is a special case of the fact that is
-conservative over
, and since
(see, e.g., [4]).
A more pertinent reframing of the above question might be: given a ‘well-behaved’ class of functions , what is the ‘largest’ ‘well-behaved’ class of formulas
for which
corresponds to it. I am not focussing on this version of the question for a few reasons:
- Most results in the literature focus on theories with induction on non-deterministic classes, e.g.
and
above, and admit witness extraction to a ‘deterministic’ function class.
does not really admit induction on
predicates per se, but rather provably
predicates. This dependence on provability means that the class of formulas is not, in my opinion, ‘well-behaved’.
- Boolean combinations of
, and similar classes, admit no complete problem, and so are not, in my opinion, ‘well-behaved’….
A note on ‘semantic’ classes
The final bullet point above is a little subtle, but I think a reasonable requirement since it provides a natural ‘stopping point’ for a class of inductive invariants. Note, however, that just because a class of inductive invariants admits a complete problem, this does not mean that the corresponding function class does. E.g., there is a universal Turing machine complete for , but there is no universal primitive recursive evaluator for primitive recursion.
For other ‘ and the primitive recursive functionals is, in fact, a family of correspondences, one for each level of the arithmetical hierarchy (and each corresponding type level of primitive recursion), as delineated by Parsons [1].
References
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[Bibtex]
@article{parsons72:on-n-quant-ind,
title={On n-quantifier induction},
volume={37},
DOI={10.2307/2272731},
number={3},
journal={Journal of Symbolic Logic},
publisher={Cambridge University Press},
author={Parsons, Charles},
year={1972},
pages={466–482},
}
@book{buss86:bounded-arithmetic,
year = "1986",
title = "Bounded arithmetic",
author = "Buss, Samuel R.",
address = "Napoli",
publisher = "Bibliopolis",
pages = "1 vol. (221 p.)",
series = "Studies in proof theory 3",
isbn = "88-7088-150-4",
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[Bibtex]
@article{goedel58:dialectica,
author = {Gödel, Von Kurt},
title = {Über eine bisher noch nicht benützte erweiterung des finiten standpunktes},
journal = {Dialectica},
volume = {12},
number = {3‐4},
pages = {280-287},
doi = {https://doi.org/10.1111/j.1746-8361.1958.tb01464.x},
url = {https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1746-8361.1958.tb01464.x},
eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/j.1746-8361.1958.tb01464.x},
year = {1958}
}
@book{hajek-pudlak93:metamathematics-fo-arithmetic,
author = {Petr H{\'{a}}jek and
Pavel Pudl{\'{a}}k},
title = {Metamathematics of First-Order Arithmetic},
series = {Perspectives in mathematical logic},
publisher = {Springer},
year = {1993},
url = {http://www.springer.com/mathematics/book/978-3-540-63648-9},
isbn = {978-3-540-63648-9},
}
Interesting post! I don’t have any answers, except to note that the questions of course have echoes for stronger, but still (meta)predicative, systems.
Also, I’d like to point out that the Π₂-conservativity of IΣ₁ over PRA, which you credit to Parsons, was independently established by Mints and Takeuti. Mints used the no-counterexample interpretation (Quantifier-free and one-quantifier systems. Journal of Soviet Mathematics, 1:71–84, 1972; Russian version 1971). Takeuti’s proof using ordinal analysis appears in the 1975 Proof Theory book.
Thanks! Which (meta)predicative systems are you thinking of? Second-order ones?
The question is certainly meaningful beyond purely first-order arithmetic, but what strikes me is that all of the results I mentioned can be taken over the same base theory (say Buss’ basic theory of bounded arithmetic), for which the only varying parameter is the class of induction invariants.
Finally, thank you for the references, – I have added an edited note underneath the statement of the result. I think I also could/should have mentioned an earlier Parsons paper, from 1970 (‘On a number-theoretic choice scheme and its relation to induction’). Mints’ result is only for
, right? I looked at Takeuti’s book again and realised that his argument is in a sense complementary to that of Parsons, establishing a correspondence from alternation of quantifiers to towers of
rather than to higher types in Parsons’ work. Very nice to have so many proof-theoretic perspectives on the same objects!