Burr, Wolfgang; Hartung, Volker A characterization of the \(\Sigma_1\)-definable functions of \(\text{KP}\omega+(\text{uniform AC})\). (English) Zbl 0913.03051 Arch. Math. Logic 37, No. 3, 199-214 (1998). 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 [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 [J. Diller and 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 [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. Reviewer: Benjamin Blankertz (Münster) Cited in 1 ReviewCited in 1 Document MSC: 03F10 Functionals in proof theory 03F25 Relative consistency and interpretations 03E70 Nonclassical and second-order set theories 03E25 Axiom of choice and related propositions Keywords:functional interpretation; Kripke-Platek set theory; primitive-recursive set functionals; Church-Rosser theorem Citations:Zbl 0761.03016; Zbl 0090.01003; Zbl 0277.02006; Zbl 0481.03035 PDFBibTeX XMLCite \textit{W. Burr} and \textit{V. Hartung}, Arch. Math. Logic 37, No. 3, 199--214 (1998; Zbl 0913.03051) Full Text: DOI