In this paper, we show that the dense existence of nowhere-differentiable continuous functions in is provable, using a version of the Baire category theorem, in an intuitionistic subsystem of elementary analysis whose induction is restricted to formulae.
S.Banach, Über die Baire’sche Kategorie gewisser Funktionenmengen, Studia Mathematica3 (1931), 174–179. doi:10.4064/sm-3-1-174-179.
2.
J.Berger, H.Ishihara, T.Kihara and T.Nemoto, The binary expansion and the intermediate value theorem in constructive reverse mathematics, Arch. Math. Logic (2018). doi:10.1007/s00153-018-0627-2.
3.
E.Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York, 1967.
4.
V.Brattka, Computable versions of Baire’s category theorem, in: Mathematical Foundations of Computer Science 2001. MFCS 2001, J.Sgall, A.Pultr and P.Kolman, eds, Lecture Notes in Computer Science, Vol. 2136, Springer, Berlin, Heidelberg, 2001.
5.
D.K.Brown and S.G.Simpson, The Baire category theorem in weak subsystem of second-order-arithmetic, the Journal of Symbolic Logic58 (1993), 557–578. doi:10.2307/2275219.
6.
H.Ishihara, Constructive reverse mathematics: Compactness properties, in: From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, P.Schuster and L.Crosilla, eds, Oxford University Press, 2005, pp. 245–267. doi:10.1093/acprof:oso/9780198566519.003.0016.
7.
H.Ishihara and P.Schuster, A continuity principle, a version of Baire’s theorem and a boundedness principle, J. Symbolic Logic73 (2008), 1354–1360. doi:10.2178/jsl/1230396924.
8.
T.Nemoto, Finite sets and infinite sets in weak intuitionistic arithmetic, Arch. Math. Logic (2020). doi:10.1007/s00153-019-00704-8.
9.
T.Nemoto and K.Sato, A marriage of Brouwer’s Intuitionism and Hilbert’s Finitism I: Arithmetic, Journal of Symbolic Logic., to appear.
10.
J.C.Oxtoby, Measure and Category, Springer-Verlag, New York, 1971.
11.
S.G.Simpson, Subsystems of Second Order Arithmetic, 2nd edn, Cambridge University Press, 2009.
12.
S.G.Simpson, Baire categoricity and -induction, Notre Dame J. Formal Logic55(1) (2014), 75–78. doi:10.1215/00294527-2377887.
13.
A.S.Troelstra and D.van Dalen, Constructivism in Mathematics, Vol. I and II, North-Holland, Amsterdam, 1988.
14.
K.Yokoyama, On the strength of Ramsey theorem without -induction, Mathematical Logic Quaterly19 (2013), 108–111. doi:10.1002/malq.201200047.
