Deterministic - nondeterministic pairs in proof theory

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 $I\Sigma_1 \vdash \forall \vec x \exists ! y \ \phi(\vec x,y)$ , for $\phi\in \Sigma_1$ , then $\phi$ computes the graph of a primitive recursive function in the standard model $\mathbb N$ .

Conversely, for every primitive recursive function $f(\vec x)$ , there is a $\Sigma_1$ formula $\phi_f (\vec x, y)$ computing the graph of $f$ such that $I\Sigma_1 \vdash \forall \vec x \exists ! y \ \phi_f(\vec x, y)$ .

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:

Induction on semi-recursive predicates corresponds to primitive recursion.

Now let us consider Buss’ theory $S^1_2$ , which extends some basic universal axioms by ‘ $\Sigma^b_1$ polynomial-induction’, – think of this as structural induction over only $\mathbf{NP}$ -predicates. The notable witnessing theorem here is:

Theorem 2 ([2]). If $S^1_2 \vdash \forall \vec x \exists ! y \ \phi(\vec x,y)$ , for $\phi\in \Sigma_1$ , then $\phi$ computes the graph of a polynomial-time function in the standard model $\mathbb N$ .
Conversely, for every polynomial-time function $f(\vec x)$ , there is a $\Sigma^b_1$ formula $\phi_f (\vec x, y)$ computing the graph of $f$ such that $S^1_2\vdash \forall \vec x \exists ! y \ \phi_f(\vec x, y)$ .

Notice the similarity? Here the motto is:

Structural induction on $\mathbf{NP}$ predicates corresponds to polynomial time.

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 $S^1_2$ the non-deterministic class is obtained by extending the deterministic one by bounded search, whereas for $I\Sigma_1$ it is unbounded.

Less obvious examples

To throw more spanners into the works, here are some other well-known results:

Induction on arithmetical predicates (i.e. $\mathsf{PA}$ ) corresponds to the Gödel primitive recursive functionals. (via, say, Gödel’s functional interpretation of arithmetic, [3])
Structural induction on $\mathbf{NEXP}$ predicates corresponds to $\mathbf{PSPACE}$ . ([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 $\Phi$ what are, in general, the provably recursive functions of $I\Phi$ ?
Conversely, given a ‘well-behaved’ class of functions $\mathcal C$ , what is the ‘largest non-deterministic’ ‘well-behaved’ class of formulas $\Phi$ such that $I\Phi$ corresponds to $\mathcal C$ ?

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 $\Phi$ and $\mathcal C$ above.

Beyond nondeterminism

The question above is arguably not so robust, since induction for a well-behaved class, say $\Phi$ , is typically conservatively extended by induction over, say, Boolean combinations over $\Phi$ . In fact we can go further, e.g.:

Proposition 4. $I\Delta_2$ is $\Pi_3$ -conservative over $I\Sigma_1$ . Thus the provably recursive functions of $I\Delta_2$ are precisely the primitive recursive functions.

This is a special case of the fact that $B\Sigma_{n+1}$ is $\Pi_{n+2}$ -conservative over $I\Sigma_{n}$ , and since $B\Sigma_{n+1} \implies I\Delta_{n+1}$ (see, e.g., [4]).

A more pertinent reframing of the above question might be: given a ‘well-behaved’ class of functions $\mathcal C$ , what is the ‘largest’ ‘well-behaved’ class of formulas $\Phi$ for which $I\Phi$ 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. $I\Sigma_1$ and $S^1_2$ above, and admit witness extraction to a ‘deterministic’ function class.
$I\Delta_2$ does not really admit induction on $\Delta_2$ predicates per se, but rather provably $\Delta_2$ predicates. This dependence on provability means that the class of formulas is not, in my opinion, ‘well-behaved’.
Boolean combinations of $\Sigma_1$ , 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 $\Sigma_1$ , but there is no universal primitive recursive evaluator for primitive recursion.

For other ‘semantic‘ classes such as the arithmetical hierarchy, I would argue that the correspondence between $\mathsf{PA}$ 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

[1]

C. Parsons, “On n-quantifier induction,” Journal of Symbolic Logic, vol. 37, iss. 3, p. 466–482, 1972.
[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},
}

[2] S. R. Buss, Bounded arithmetic, Napoli: Bibliopolis, 1986.
[Bibtex]

@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",
}

[3]

V. K. Gödel, “Über eine bisher noch nicht benützte erweiterung des finiten standpunktes,” Dialectica, vol. 12, iss. 3‐4, pp. 280-287, 1958.
[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}
}

[4] P. Hájek and P. Pudlák, Metamathematics of First-Order Arithmetic, Springer, 1993.
[Bibtex]

@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},
}

2 thoughts on “Deterministic – nondeterministic pairs in proof theory”

Ulrik Buchholtz says:

December 31, 2020 at 7:53 am

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.

1. Anupam Das says:
  
  December 31, 2020 at 11:52 am
  
  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 $I\Sigma_1$ , 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 $\omega$ rather than to higher types in Parsons’ work. Very nice to have so many proof-theoretic perspectives on the same objects!