×

A characterization of the \(\Sigma_1\)-definable functions of \(\text{KP}\omega+(\text{uniform AC})\). (English) Zbl 0913.03051

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.

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
PDFBibTeX XMLCite
Full Text: DOI