Equivalence of bar induction and bar recursion for continuous functions with continuous moduli

DOI10.1016/j.apal.2019.04.001zbMath1459.03091OpenAlexW2938315336WikidataQ128082453 ScholiaQ128082453MaRDI QIDQ2417961

Tatsuji Kawai, Makoto Fujiwara

Publication date: 31 May 2019

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

Full work available at URL: https://doi.org/10.1016/j.apal.2019.04.001

zbMATH Keywords

continuity principleconstructive reverse mathematicsbar inductionbar recursionintuitionistic mathematicsFan theorem

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Related Items (3)

Decidable fan theorem and uniform continuity theorem with continuous moduli ⋮ Characterising Brouwer's continuity by bar recursion on moduli of continuity ⋮ Higher order functions and Brouwer’s thesis

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructivism in mathematics. An introduction. Volume I
• 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
• Bar induction and restricted classical logic
• A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM
• Principles of bar induction and continuity on Baire space
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• New Computational Paradigms
• Logical Approaches to Computational Barriers

This page was built for publication: Equivalence of bar induction and bar recursion for continuous functions with continuous moduli