Functional interpretation of Aczel's constructive set theory

DOI10.1016/S0168-0072(00)00007-5zbMath0959.03043OpenAlexW2064038675WikidataQ127156077 ScholiaQ127156077MaRDI QIDQ1577478

Wolfgang Burr

Publication date: 2 May 2001

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(00)00007-5

zbMATH Keywords

functional interpretationAczel's constructive set theoriesconstructive set functionals of finite types

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Relative consistency and interpretations (03F25)

Related Items (4)

From the weak to the strong existence property ⋮ Hybrids of the \({}^ \times \)-translation for \(\mathsf{CZF}^{\omega}\) ⋮ A complexity analysis of functional interpretations ⋮ Logical problems of functional interpretations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-theoretic analysis of KPM
• Pointwise hereditary majorization and some applications
• A characterization of the \(\Sigma_1\)-definable functions of \(\text{KP}\omega+(\text{uniform AC})\)
• Constructivism in mathematics. An introduction. Volume II
• Handbook of proof theory
• Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
• The strength of some Martin-Löf type theories
• A Diller-Nahm-style functional interpretation of \(\text{KP}\omega\)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Interpreting classical theories in constructive ones
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Recursive models for constructive set theories
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• A proof-theoretic characterization of the primitive recursive set functions
• Constructive set theory
• Choice Implies Excluded Middle
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• A note on Spector's quantifier-free rule of extensionality

This page was built for publication: Functional interpretation of Aczel's constructive set theory