Working within weak subsystems of second-order arithmetic $\mathbf{Z}_2$ we consider two versions of the Baire Category theorem which are not equivalent over the base system $RCA_0$. We show that one version (B.C.T.I) is provable in $RCA_0$ while the second version (B.C.T.II) requires a stronger system. We introduce two new subsystems of $\mathbf{Z}_2$, which we call $RCA^+_0$ and $WKL^+_0$, and show that $RCA^+_0$ suffices to prove B.C.T.II. Some model theory of $WKL^+_0$ and its importance in view of Hilbert's program is discussed, as well as applications of our results to functional analysis.