Functional interpretation of Aczel's constructive set theory

✍ Scribed by Wolfgang Burr

• Publisher: Elsevier Science
• Year: 2000
• Tongue: English
• Weight: 266 KB
• Volume: 104
• Category: Article
• ISSN: 0168-0072
• DOI: 10.1016/s0168-0072(00)00007-5

✦ Synopsis

In the present paper we give a functional interpretation of Aczel's constructive set theories CZF -and CZF in systems T∈ and T + ∈ of constructive set functionals of ÿnite types. This interpretation is obtained by a translation × , a reÿnement of the ∧ -translation introduced by Diller and Nahm (Arch. Math. Logik Grundlagenforsch. 16 (1974) 49 -66) which again is an extension of G odel's Dialectica translation. The interpretation theorem gives characterizations of the deÿnable set functions of CZF -and CZF in terms of constructive set functionals. In a second part we introduce constructive set theories in all ÿnite 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 T∈ and T + ∈ . 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 deÿned in Burr (Arch. Math. Logic, to appear) for an interpretation of Kripke-Platek set theory with inÿnity (KP!).