Characterising Brouwer’s continuity by bar recursion on moduli of continuity

Makoto Fujiwara, Tatsuji Kawai

Research output: Contribution to journalArticlepeer-review

Abstract

We identify bar recursion on moduli of continuity as a fundamental notion of constructive mathematics. We show that continuous functions from the Baire space NN to the natural numbers N which have moduli of continuity with bar recursors are exactly those functions induced by Brouwer operations. The connection between Brouwer operations and bar induction allows us to formulate several continuity principles on the Baire space stated in terms of bar recursion on continuous moduli which naturally characterise some variants of bar induction. These principles state that a certain kind of continuous function from NN to N admits a modulus of continuity with a bar recursor. The results for the Baire space are recast in the setting of the Cantor space { 0 , 1 } N using the notion of fan recursor, a bar recursor for binary trees. This yields characterisations of uniformly continuous functions on the Cantor space and fan theorem in terms of fan recursors. The results for the Cantor space hold over the extensional version of intuitionistic arithmetic in all finite types (E- HAω), and those for the Baire space hold over E- HAω extended with the type for Brouwer operations. Our work places Spector’s bar recursion in a proper context of Brouwer’s intuitionistic mathematics and clarifies the connection between bar recursion and bar induction.

Original languageEnglish
Pages (from-to)241-263
Number of pages23
JournalArchive for Mathematical Logic
Volume60
Issue number1-2
DOIs
Publication statusPublished - Feb 2021

Keywords

  • Bar induction
  • Bar recursion
  • Brouwer operation
  • Constructive reverse mathematics
  • Continuity principle
  • Fan theorem
  • Intuitionistic mathematics

Fingerprint

Dive into the research topics of 'Characterising Brouwer’s continuity by bar recursion on moduli of continuity'. Together they form a unique fingerprint.

Cite this