Functional interpretation of Aczel's constructive set theory
From MaRDI portal
Publication:1577478
DOI10.1016/S0168-0072(00)00007-5zbMath0959.03043OpenAlexW2064038675WikidataQ127156077 ScholiaQ127156077MaRDI QIDQ1577478
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
functional interpretationAczel's constructive set theoriesconstructive set functionals of finite types
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
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
- 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
- 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
