A constructive proof of the dense existence of nowhere-differentiable functions in C[0,1]

Issue title: Dagstuhl Seminar on Measuring the Complexity of Computational Content 2018

Guest editors: Vasco Brattka, Damir D. Dzhafarov, Alberto Marcone and Arno Pauly

Article type: Research Article

Authors: Nemoto, Takako^{; *}

Affiliations: Department of Architectural Design, Faculty of Environmental Study, Hiroshima Institute of Technology, Japan. nemototakako@gmail.com

Correspondence: [*] Corresponding author. nemototakako@gmail.com.

Abstract: In this paper, we show that the dense existence of nowhere-differentiable continuous functions in C[0,1] is provable, using a version of the Baire category theorem, in an intuitionistic subsystem of elementary analysis whose induction is restricted to Σ10 formulae.

Keywords: Constructive mathematics, constructive reverse mathematics, Baire category theorem, nowhere-differentiable functions

DOI: 10.3233/COM-190247

Journal: Computability, vol. 9, no. 3-4, pp. 315-326, 2020