A proof-theoretic characterization of the primitive recursive set functions

Journal of Symbolic Logic 57 (3):954-969 (1992)
  Copy   BIBTEX

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 \models \forall x \exists!y\varphi (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

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 101,956

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Definability of types, and pairs of o-minimal structures.Anand Pillay - 1994 - Journal of Symbolic Logic 59 (4):1400-1409.
Flat sets.Arthur D. Grainger - 1994 - Journal of Symbolic Logic 59 (3):1012-1021.
Bounding Prime Models.Barbara F. Csima, Denis R. Hirschfeldt, Julia F. Knight & Robert I. Soare - 2004 - Journal of Symbolic Logic 69 (4):1117 - 1142.
Computable shuffle sums of ordinals.Asher M. Kach - 2008 - Archive for Mathematical Logic 47 (3):211-219.
Direct and local definitions of the Turing jump.Richard A. Shore - 2007 - Journal of Mathematical Logic 7 (2):229-262.
Ptykes in GödelsT und Definierbarkeit von Ordinalzahlen.Peter Päppinghaus - 1989 - Archive for Mathematical Logic 28 (2):119-141.

Analytics

Added to PP
2009-01-28

Downloads
258 (#105,444)

6 months
4 (#1,200,964)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Michael Rathjen
University of Leeds

Citations of this work

Computable aspects of the Bachmann–Howard principle.Anton Freund - 2019 - Journal of Mathematical Logic 20 (2):2050006.
Functional interpretation of Aczel's constructive set theory.Wolfgang Burr - 2000 - Annals of Pure and Applied Logic 104 (1-3):31-73.
Predicatively computable functions on sets.Toshiyasu Arai - 2015 - Archive for Mathematical Logic 54 (3-4):471-485.

View all 9 citations / Add more citations

References found in this work

The fine structure of the constructible hierarchy.R. Björn Jensen - 1972 - Annals of Mathematical Logic 4 (3):229.
On Weak Theories of Sets and Classes which are Based on Strict ∏11-REFLECTION.Andrea Cantini - 1985 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 31 (21-23):321-332.

Add more references