A Proof-Theoretic Characterization of the Primitive Recursive Set Functions
Rathjen, Michael
J. Symbolic Logic, Tome 57 (1992) no. 1, p. 954-969 / Harvested from Project Euclid
Let $\mathrm{KP}^-$ be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let $G: V \rightarrow V (V:=$ universe of sets) be a $\triangle_0$-definable set function, i.e. there is a $\triangle_0$-formula $\varphi(x, y)$ such that $\varphi(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 $\Sigma_1$-definable in $\mathrm{KP}^- + \Sigma_1$-Foundation $+ \forall x \exists!y\varphi (x, y)$. Moreover, we show that this is still true if one adds $\Pi_1$-Foundation or a weak version of $\triangle_0$-Dependent Choices to the latter theory.
Publié le : 1992-09-14
Classification: 
@article{1183744050,
     author = {Rathjen, Michael},
     title = {A Proof-Theoretic Characterization of the Primitive Recursive Set Functions},
     journal = {J. Symbolic Logic},
     volume = {57},
     number = {1},
     year = {1992},
     pages = { 954-969},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744050}
}
Rathjen, Michael. A Proof-Theoretic Characterization of the Primitive Recursive Set Functions. J. Symbolic Logic, Tome 57 (1992) no. 1, pp.  954-969. http://gdmltest.u-ga.fr/item/1183744050/