A proof-theoretic characterization of the primitive recursive set functions
Keyword(s):
AbstractLet 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.
Keyword(s):
2014 ◽
Vol 14
(2)
◽
pp. 203-245
◽
Keyword(s):
2021 ◽
Vol 31
(3)
◽
pp. 033107
2011 ◽
Vol 07
(01)
◽
pp. 173-202