Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

On axiom schemes for T-provably \({\Delta_{1}}\) formulas


This paper investigates the status of the fragments of Peano Arithmetic obtained by restricting induction, collection and least number axiom schemes to formulas which are \({\Delta_1}\) provably in an arithmetic theory T. In particular, we determine the provably total computable functions of this kind of theories. As an application, we obtain a reduction of the problem whether \({I\Delta_0 + \neg \mathit{exp}}\) implies \({B\Sigma_1}\) to a purely recursion-theoretic question.

This is a preview of subscription content, log in to check access.


  1. 1

    Adamowicz Z., Kołodziejczyk L.A., Paris J.B.: Truth definitions without exponentiation and the \({\Sigma_1}\) collection scheme. J. Symb. Logic 77, 649–655 (2012)

  2. 2

    Avigad J.: Saturated models of universal theories. Ann. Pure Appl. Logic 118, 219–234 (2002)

  3. 3

    Beklemishev L.D.: Induction rules, reflection principles, and provably recursive functions. Ann. Pure Appl. Logic 85, 193–242 (1997)

  4. 4

    Beklemishev L.D.: A proof-theoretic analysis of collection. Arch. Math. Logic 37, 275–296 (1998)

  5. 5

    Beklemishev L.D.: On the induction scheme for decidable predicates. J. Symb. Logic 68, 17–34 (2003)

  6. 6

    Clote P., Krajíček J.: Open problems. In: Clote, P., Krajíček, J. (eds) Arithmetic, Proof Theory, and Computational Complexity, pp. 1–19. Oxford University Press, Oxford (1993)

  7. 7

    Cordón-Franco A., Fernández-Margarit A., Lara-Martín F.F.: On the quantifier complexity of \({\Delta_{n+1}(T)}\) -induction. Arch. Math. Logic 43, 371–398 (2004)

  8. 8

    Cordón-Franco, A., Fernández-Margarit, A., Lara-Martín, F.F.: Provably total primitive recursive functions: theories with induction. In: Marcinkowski, J., Tarlecki, A. (eds.) Computer Science Logic, 18th International Workshop, CSL 2004, Karpacz, Poland, Sept 20–24, 2004, Proceedings, pp. 355–369, Lecture Notes in Comput. Sci. 3210, Springer, Berlin, Heidelberg (2004)

  9. 9

    Cordón-Franco A., Fernández-Margarit A., Lara-Martín F.F.: Fragments of Arithmetic and true sentences. MLQ Math. Log. Q. 51, 313–328 (2005)

  10. 10

    Cordón-Franco A., Fernández-Margarit A., Lara-Martín F.F.: A note on parameter free \({\Pi_1}\) -induction and restricted exponentiation. MLQ Math. Log. Q. 57, 444–455 (2011)

  11. 11

    Fernández-Margarit A., Lara-Martín F.F.: Induction, minimization and collection for \({\Delta_{n+1}(T)}\) -formulas. Arch. Math. Logic 43, 505–541 (2004)

  12. 12

    Hájek P., Pudlák P.: Metamathematics of First-Order Arithmetic. Springer, Berlin, Heidelberg (1993)

  13. 13

    Kaye, R.: Diophantine and parameter-free induction. Ph.D. thesis, University of Manchester (1987)

  14. 14

    Kaye R., Paris J., Dimitracopoulos C.: On parameter free induction schemas. J. Symb. Logic 53, 1082–1097 (1988)

  15. 15

    Kreisel H., Lévy A.: Reflection principles and their use for establising the complexity of axiomatic systems. Arch. Math. Logik Grundlag. 14, 97–142 (1968)

  16. 16

    Lessan, H.: Models of Arithmetic. Ph.D. thesis, University of Manchester (1978)

  17. 17

    Paris J.B., Kirby L.: \({\Sigma_n}\) -Collection schemas in arithmetic. In: Macintyre, A., Pacholski, L., Paris, J. (eds) Logic Colloquium 77, Studies in Logic and the Foundations of Mathematics 96., pp. 285–296. North-Holland, Amsterdam (1978)

  18. 18

    Parsons C.: On n-quantifier induction. J. Symb. Logic 37, 466–482 (1972)

  19. 19

    Rose H.E.: Subrecursion: Functions and Hierarchies. Clarendon Press, Oxford (1984)

  20. 20

    Sirokofskich A., Dimitracopoulos C.: On a problem of J. Paris. J. Log. Comput. 17, 1099–1107 (2007)

  21. 21

    Slaman T.: \({\Sigma_n}\) -bounding and \({\Delta_n}\) -induction. Proc. Am. Math. Soc. 132, 2449–2456 (2004)

  22. 22

    Takeuti G.: Grzegorcyk’s hierarchy and Iep\({\Sigma_1}\) . J. Symb. Logic 59, 1274–1284 (1994)

  23. 23

    Thapen N.: A note on \({\Delta_1}\) induction and \({\Sigma_1}\) collection. Fund. Math. 186, 79–84 (2005)

  24. 24

    Wilkie A.J., Paris J.B.: On the existence of end-extensions of models of bounded induction. In: Fenstad, J.E., Frolov, I.T., Hilpinen, R. (eds) Logic, Methodology, and Philosophy of Science VIII, Moscow, 1987, pp. 143–161. North-Holland, Amsterdam (1989)

Download references

Author information

Correspondence to A. Cordón-Franco.

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Cordón-Franco, A., Fernández-Margarit, A. & Lara-Martín, F.F. On axiom schemes for T-provably \({\Delta_{1}}\) formulas. Arch. Math. Logic 53, 327–349 (2014).

Download citation


  • Fragments of Peano Arithmetic
  • \({\Delta_1}\) formulas
  • Provably total computable functions

Mathematics Subject Classification

  • 03F30
  • 03D20