Hostname: page-component-8448b6f56d-t5pn6 Total loading time: 0 Render date: 2024-04-23T20:31:19.522Z Has data issue: false hasContentIssue false
  • English
  • Français

A proof-theoretic characterization of the primitive recursive set functions

Published online by Cambridge University Press:  12 March 2014

Michael Rathjen
Michael Rathjen*
Affiliation:
Institut für Mathematische Logik und Grundlagenforschung, Westfälische Wilhelms-Universität Münster, W-4400 Münster, Germany
*
Department of Mathematics, Ohio State University, Columbus, Ohio 43210.
Get access Rights & Permissions [Opens in a new window]

Abstract

Let KP− be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V ≔ universe of sets) be a Δ0-definable set function, i.e. there is a Δ0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and V ⊨ ∀x∃!yφ(x, y). In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection of those functions which are Σ1-definable in KP− + Σ1-Foundation + ∀x∃!yφ(x, y). Moreover, we show that this is still true if one adds Π1-Foundation or a weak version of Δ0-Dependent Choices to the latter theory.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 57 , Issue 3 , September 1992 , pp. 954 - 969
Copyright
Copyright © Association for Symbolic Logic 1992

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

[B]Barwise, J., Admissible sets and structures, Springer-Verlag, Berlin, 1975.CrossRefGoogle Scholar
[C]Cantini, A., On weak theories of sets and classes which are based on strict -reflection, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 31 (1985), pp. 321–332.CrossRefGoogle Scholar
[D]Devlin, K., Constructibility, Springer-Verlag, Berlin, 1984.CrossRefGoogle Scholar
[G]Gandy, R. O., Set-theoretic functions for elementary syntax, Axiomatic set theory. Part 2, Proceedings of Symposia in Pure Mathematics, vol. 13, part 2, American Mathematical Society, Providence, Rhode Island, 1974, pp. 103–126.CrossRefGoogle Scholar
[JäPo]Jäger, G. and Pohlers, W., Eine beweistheoretische Untersuchungen von und verwandter Systeme, Bayerische Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse: Sitzungsberichte, 1982, pp. 1–28.Google Scholar
[J]Jensen, R. B., The fine structure of the constructible hierarchy, Annals of Mathematical Logic, vol. 4 (1972), pp. 229–308.CrossRefGoogle Scholar
[JK]Jensen, R. B. and Karp, C., Primitive recursive set functions, Axiomatic set theory. Part 1, Proceedings of Symposia in Pure Mathematics, vol. 13, part 1, American Mathematical Society, Providence, Rhode Island, 1971, pp. 143–176.CrossRefGoogle Scholar
[P]Parsons, C., On a number theoretic choice schema and its relation to induction, Intuitionism and proof theory (Kino, A.et al., editors), North-Holland, Amsterdam, 1970, pp. 459–474.Google Scholar
[Schw]Schwichtenberg, H., Some applications of cut-elimination, Handbook of Mathematical Logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 868–895.Google Scholar
[Si]Simpson, S. G., Set theoretic aspects of ATR, Logic Colloquium '80 (van Dalen, D.et al., editors), North-Holland, Amsterdam, 1982, pp. 255–271.Google Scholar
[T]Tait, W. W., Normal derivability in classical logic, The syntax and semantics of infinitary languages (Barwise, J., editor), Springer-Verlag, Berlin, 1968, pp. 204–236.CrossRefGoogle Scholar