Set existence property for intuitionistic theories with dependent choice

DOI10.1016/0168-0072(83)90011-8zbMath0539.03039OpenAlexW2074713441MaRDI QIDQ793723

Harvey M. Friedman, Andrej Scedrov

Publication date: 1983

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

Full work available at URL: https://doi.org/10.1016/0168-0072(83)90011-8

zbMATH Keywords

countable choiceintuitionistic type theoryexistence propertyrecursive realizabilityFriedman slashintuitionistic theoriesintuitionistic Zermelo set theoryintuitionistic ZFrelativized dependent choicesecond order intuitionistic arithmetic

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50)

Related Items (3)

CZF does not have the existence property ⋮ From the weak to the strong existence property ⋮ The disjunction and related properties for constructive Zermelo-Fraenkel set theory

Cites Work

• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Constructive set theory
• Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
• Unnamed Item
• Unnamed Item

This page was built for publication: Set existence property for intuitionistic theories with dependent choice