Baire categoricity and \(\Sigma_1^0\)-induction (Q2443120)

The main result of this paper is that the Baire category theorem (BCT) is equivalent to RCA\(_0\) over RCA\(_0^*\). The system RCA\(_0^*\) is RCA\(_0\) with \(\Sigma_1^0\)-induction weakened to \(\Sigma^0_0\)-induction plus totality of natural number exponentiation. The system RCA\(_0^*\) was introduced by \textit{S. G. Simpson} and \textit{R. L. Smith} in [Ann. Pure Appl. Logic 31, 289--306 (1986; Zbl 0603.03019)], where they showed that RCA\(^*_0\) is \(\Pi^0_2\) conservative over elementary function arithmetic (EFA). This proof of the equivalence BCT and RCA\(_0\) uses the equivalence of RCA\(_0\) and the assertion that every infinite subset of the natural numbers contains arbitrarily large finite sets, from the work of \textit{S. G. Simpson} and \textit{K. Yokoyama} [Ann. Pure Appl. Logic 164, No. 3, 284--293 (2013; Zbl 1267.03030)]. The first reverse mathematics formalization of BCT and its proof in RCA\(_0\) appear in [\textit{D. K. Brown} and \textit{S. G. Simpson}, J. Symb. Log. 58, No. 2, 557--578 (1993; Zbl 0794.03085)].