Takako Nemoto: Baire category theorem and nowhere differentiable continuous function...

Full title: Baire category theorem and nowhere differentiable continuous function in constructive mathematics

The lecture was held within the framework of the Hausdorff Trimester Program: Types, Sets and Constructions.

Abstract:
In Bishop's constructive mathematics, it is known that Baire category theorem is provable. This proof requires the axiom of countable choice (cf. [1]). On the other hand, in classical reverse mathematics, their same form of Baire category theorem restricted for complete separable metric space is provable in RCA0, which has only restricted version of countable choice (cf. [2, Theorem II.5.8]). In this talk, we will see that the proof in classical reverse mathematics also works in constructive counterpart EL0 of RCA0, which has only quantifier free number-number choice and ∑10 induction. We will also see that this version of Baire category theorem is enough to show the existence of nowhere differentiable continuous function on [0; 1].

References:
[1] E. Bishop, Foundations of Constructive Analysis, Mcgraw-Hill, 1967.
[2] S. G. Simpson, Subsystems of Second Order Arithmetic, Cambridge University Press, 2009.