On the constructive Dedekind reals

DOI10.1007/s11813-007-0005-6zbMath1162.03034arXiv1510.00641OpenAlexW2145724981WikidataQ59903909 ScholiaQ59903909MaRDI QIDQ1000868

Robert S. Lubarsky, Michael Rathjen

Publication date: 11 February 2009

Published in: Logic and Analysis (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1510.00641

zbMATH Keywords

constructive set theoryDedekind reals

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50)

Related Items

CZF does not have the existence property, On the Cauchy completeness of the constructive Cauchy reals, Should pluralists be pluralists about pluralism?, Topological inductive definitions, Logics of intuitionistic Kripke-Platek set theory, Quantitative continuity and Computable Analysis in Coq, On the failure of BD-ℕ and BD, and an application to the anti-specker property, On the Cauchy Completeness of the Constructive Cauchy Reals, Refinement is equivalent to Fullness, On the existence of Stone-Čech compactification, The Hahn-Banach theorem by disjunction elimination, Ordering groups constructively, Completion of premetric spaces

Cites Work

• Unnamed Item
• The lack of definable witnesses and provably recursive functions in intuitionistic set theories
• Constructivism in mathematics. An introduction. Volume II
• Independence results around constructive ZF
• On the Cauchy completeness of the constructive Cauchy reals
• On constructing completions