The Dialectica-style functional interpretation of Kripke-Platek set theory with infinity ( $\hbox{\sf KP} \omega$ ) given in [1] uses a choice functional (which is not a definable set function of ( $hbox{\sf KP} \omega$ ). By means of a Diller-Nahm-style interpretation (cf. [4]) it is possible to eliminate the choice functional and give an interpretation by set functionals primitive recursive in $x\mapsto\omega$ . This yields the following characterization: The class of $\Sigma$ -definable set functions of $\hbox{\sf KP} \omega$ coincides with (...) the collection of set functionals of type 1 primitive recursive in $x\mapsto \omega$. (shrink)

Constructive set theory started with Myhill's seminal 1975 article [8]. This paper will be concerned with axiomatizations of the natural numbers in constructive set theory discerned in [3], clarifying the deductive relationships between these axiomatizations and the strength of various weak constructive set theories.

Gödel's dialectica interpretation of Heyting arithmetic HA may be seen as expressing a lack of confidence in our understanding of unbounded quantification. Instead of formally proving an implication with an existential consequent or with a universal antecedent, the dialectica interpretation asks, under suitable conditions, for explicit 'interpreting' instances that make the implication valid. For proofs in constructive set theory CZF-, it may not always be possible to find just one such instance, but it must suffice to explicitly name a set (...) consisting of such interpreting instances. The aim of eliminating unbounded quantification in favor of appropriate constructive functionals will still be obtained, as our ∧-interpretation theorem for constructive set theory in all finite types CZFω- shows. By changing to a hybrid interpretation ∧q, we show closure of CZFω- under rules that – in stronger forms – have already been studied in the context of Heyting arithmetic. In a similar spirit, we briefly survey modified realizability of CZFω- and its hybrids. Central results of this paper have been proved by Burr 2000a and Schulte 2006, however, for different translations. We use a simplified interpretation that goes back to Diller and Nahm 1974. A novel element is a lemma on absorption of bounds which is essential for the smooth operation of our translation. (shrink)