The binary expansion and the intermediate value theorem in constructive reverse mathematics

DOI10.1007/S00153-018-0627-2OpenAlexW2741308551WikidataQ129893498 ScholiaQ129893498MaRDI QIDQ1712938

Takayuki Kihara, Josef Berger, Takako Nemoto, Hajime Ishihara

Publication date: 24 January 2019

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-018-0627-2

zbMATH Keywords

constructive reverse mathematicsconvex treethe binary expansionthe intermediate value theoremthe weak König lemma

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Other constructive mathematics (03F65)

Related Items (8)

König's lemma, weak König's lemma, and the decidable fan theorem ⋮ Coding of real‐valued continuous functions under WKL$\mathsf {WKL}$ ⋮ Constructive Proofs of Negated Statements ⋮ The Monotone Completeness Theorem in Constructive Reverse Mathematics ⋮ Weihrauch and constructive reducibility between existence statements ⋮ An extension of the equivalence between Brouwer's fan theorem and weak König's lemma with a uniqueness hypothesis ⋮ Parallelizations in Weihrauch reducibility and constructive reverse mathematics ⋮ Bishop-Style Constructive Reverse Mathematics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative
• Equivalents of the (weak) fan theorem
• Techniques of constructive analysis
• Weak König's lemma implies Brouwer's fan theorem: a direct proof
• Constructivism in mathematics. An introduction. Volume II
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On computable sequences
• Relativization of Real Numbers to a Universe
• An omniscience principle, the König Lemma and the Hahn‐Banach theorem
• The Weak Kőnig Lemma, Brouwer’s Fan Theorem, De Morgan’s Law, and Dependent Choice
• Brouwer's fan theorem and unique existence in constructive analysis

This page was built for publication: The binary expansion and the intermediate value theorem in constructive reverse mathematics