A Diller-Nahm-style functional interpretation of \(\text{KP}\omega\) (Q1590194)

\(\text{KP} \omega\) stands for Kripke-Platek set theory with infinity. In a previous paper [ibid. 37, No. 3, 199-214 (1998; Zbl 0913.03051)], the author, with \textit{V. Hartung}, presented a Dialectica functional interpretation of it. But they needed a choice functional, and so the theory interpreted is not \(\text{KP} \omega\) but \(\text{KP} \omega+\)(uniform AC). The difficulty lies in set theory itself. For instance, to interprete a simple formula \(a\neq\emptyset \to\exists y\) \(y\in a\), one must produce a term \(t(a)\) that verifies \(t(a)\in a\). And so, a choice functional was necessary. In this paper, the author takes a little different route, and gives a ``set'' of terms containing some that verify the formula (rather than a specific term), using bounded quantification as the Diller-Nahm variant did. An object of the lowest type, i.e. type \(o\), is a set. To handle a set of higher type \(\tau\), the author uses a pair of functionals, \(w\) and \(X\), of types \(o\to\tau\) and \(o\), and lets \(\{wx/x\in X\}\) be the set. Since the author uses the Shoenfield style interpretation, the translation of \(\varphi\) takes the form \(\forall v\exists wX \exists x\in X\) \(\overline \varphi(v,wx)\). The main result states: if \(\text{KP} \omega\vdash \varphi\), then there are functional terms \(w\) and \(X[v]\) such that \(\exists x\in X\) \(\overline\varphi (v,wx)\) is valid in the type structure over \(V\). The proof is long and complicated, but straightforward. A characterization of \(\Sigma\)-definable set functions of \(\text{KP}\omega\) is given as a corollary: they are exactly those type 1 functionals that are primitive recursive in \(x\mapsto \omega\).