Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-23T07:00:58.906Z Has data issue: false hasContentIssue false
  • English
  • Français

On the induction schema for decidable predicates

Published online by Cambridge University Press:  12 March 2014

Lev D. Beklemishev
Lev D. Beklemishev*
Affiliation:
Steklov Mathematical Institute, Gubkina 8, 117966 Moscow, Russia, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, IΔ1. We show that IΔ1 is independent from the set of all true arithmetical Π2-sentences. Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also obtain some conservation and independence results for parameter free and inference rule forms of Δ1-induction.

An open problem formulated by J. Paris (see [4, 5]) is whether IΔ1 proves the corresponding least element principle for decidable predicates, LΔ1 (or, equivalently, the Σ1-collection principle BΣ1). We reduce this question to a purely computation-theoretic one.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 68 , Issue 1 , March 2003 , pp. 17 - 34
Copyright
Copyright © Association for Symbolic Logic 2003

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Beklemishev, L. D., Induction rules, reflection principles, and provably recursive functions, Annals of Pure and Applied Logic, vol. 85 (1997), pp. 193–242.CrossRefGoogle Scholar
[2]Beklemishev, L. D., A proof-theoretic analysis of collection, Archive for Mathematical Logic, vol. 37 (1998), pp. 275–296.CrossRefGoogle Scholar
[3]Beklemishev, L. D., Open least element principle and bounded query computation, Computer science logic, 13th international workshop, CSL '99, Madrid, Spain, September 20–25, 1999, Proceedings (Flum, J. and Rodrigues-Artalejo, M., editors), Lecture Notes in Computer Science, vol. 1683, Springer-Verlag, Berlin, 1999, pp. 389–404.Google Scholar
[4]Clote, P. and Krajíček, J., Open problems, Arithmetic, proof theory, and computational complexity (Clote, P. and Krajíček, J., editors), Oxford University Press, Oxford, 1993, pp. 1–19.CrossRefGoogle Scholar
[5]Hájek, P. and Pudlák, P., Metamathematics of first order arithmetic, Springer-Verlag, Berlin, Heidelberg, New York, 1993.CrossRefGoogle Scholar
[6]Kaye, R., Paris, J., and Dimitracopoulos, C., On parameter free induction schemas, this Journal, vol. 53 (1988), no. 4, pp. 1082–1097.Google Scholar
[7]Paris, J., A hierarchy of cuts in models of arithmetic, Model theory of algebra and arithmetic, Proceedings, Karapascz, Poland, 1979, Lecture Notes in Mathematics, vol. 834, Springer-Verlag, 1980, pp. 312–337.Google Scholar
[8]Parsons, C., On a number-theoretic choice schema and its relation to induction, Intuitionism and proof theory (Kino, A., Myhill, J., and Vessley, R. E., editors), North-Holland, Amsterdam, 1970, pp. 459–473.Google Scholar
[9]Parsons, C., On n-quantifier induction, this Journal, vol. 37 (1972), no. 3, pp. 466–482.Google Scholar
[10]Rastsvetaev, A. and Beklemishev, L., On the query complexity of finding a local maximum point, Logic Group Preprint Series 206, University of Utrecht, 2000.Google Scholar
[11]Schwichtenberg, H., Some applications of cut-elimination, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 867–896.CrossRefGoogle Scholar