Skip to content

The Proof Theory Blog

⊢ ((A → B) → A) → A

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

Deterministic – nondeterministic pairs in proof theory

Posted on December 30, 2020December 31, 2020 by Anupam Das

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 inductionBy 'structural' induction I mean, e.g., induction on the structure of the binary representation of a number, not the number itself. Note that the aforementioned result of Parsons holds when restricting to only structural induction too, so we may assume only this sort of induction throughout this post. 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 unboundedNote in particular the primitive recursive functions are closed under bounded search..

Less obvious examples

To throw more spanners into the works, here are some other well-known resultsIn all cases, 'corresponds to' should be read in the same way as above, over a suitable base theory. :

  • 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 generalFor concreteness, let us assume that in all cases the theory is 'bootstrapped' to include at least Buss' language and its corresponding basic axioms, and induction is always structural. , 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 ‘semanticI use 'semantic' somewhat loosely here, but what is important is that such classes admit no complete problem.‘ 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] [doi] 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] [doi] 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”

  1. 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.

    Reply
    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!

      Reply

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2022 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT