A characterization of the \(\Sigma_1\)-definable functions of \(\text{KP}\omega+(\text{uniform AC})\) (Q1128184)

\textit{M. Rathjen} showed [J. Symb. Log. 57, 954-969 (1992; Zbl 0761.03016)]\ by proof-theoretic means that the set-functions primitive-recursive in \((x\mapsto\omega)\) are exactly the \(\Sigma_1\)-definable set-functions of KP\(\omega\) with foundation restricted to \(\Sigma_1\)-formulae. The authors of the paper under review were guided by the aim to achieve an analogous result for KP\(\omega\) with full foundation using a Gödel-style [\textit{K. Gödel}, Dialectica 12, 280-287 (1958; Zbl 0090.01003)]\ functional interpretation: (1) The class of \(\Sigma_1\) definable set functions of KP\(\omega\) coincides with the collection of set functionals of type 1 primitive-recursive in \((x\mapsto\omega)\). In this paper only a modification of that aim could be established, namely: (2) The \(\Sigma_1\)-definable set-functions of KP\(\omega\)+(uniform AC) are exactly the set functionals of type 1 primitive recursive in \((x\mapsto\omega)\) and a fixed choice functional \(F_C\) of type 1. But in the meantime the first author developed a new Diller-Nahm style [\textit{J. Diller} and \textit{W. Nahm}, Arch. Math. Logik Grundlagenforsch. 16, 49-66 (1974; Zbl 0277.02006)]\ translation by which (1) can by shown. Additionally this translation allows a functional interpretation of CZF, Aczel's constructive set theory [\textit{P. Aczel}, Logic colloquium '77, Stud. Logic Found. Math. 96, 56-66 (1978; Zbl 0481.03035)]. For the proof of (2) a variant of the Shoenfield \(\forall\exists\)-translation is defined for all formulae of \({\mathcal L}+\{F_C\}\) which allows a Gödel-style functional interpretation of KP\(\omega\)+(uniform AC). For the treatment of the bounded \(\forall\)-rule the choice-functional \(F_C\) is needed. For the remaining inclusion the computability of the used set functionals is shown by proving informally in KP\(\omega \)+(uniform AC) a suitable Church-Rosser-theorem. The article under review is carefully written. The proofs are detailed and complete.