Functional interpretation of Aczelʹs constructive set theory Original Research Article

In the present paper we give a functional interpretation of Aczelʹs constructive set theories View the MathML source and CZF in systems View the MathML source and View the MathML source of constructive set functionals of finite types. This interpretation is obtained by a translation ×, a refinement of the ∧-translation introduced by Diller and Nahm (Arch. Math. Logik Grundlagenforsch. 16 (1974) 49–66) which again is an extension of Gödelʹs Dialectica translation. The interpretation theorem gives characterizations of the definable set functions of View the MathML source and CZF in terms of constructive set functionals. In a second part we introduce constructive set theories in all finite types. We expand the interpretation to these theories and give a characterization of the translation ×. We further show that the simplest non-trivial axiom of extensionality (for type 2) is not interpretable by functionals of View the MathML source and View the MathML source. We obtain this result by adapting Howardʹs notion of hereditarily majorizable functionals to set functionals. Subject of the last section is the translation ∨ that is defined in Burr (Arch. Math. Logic, to appear) for an interpretation of Kripke-Platek set theory with infinity (KPω).