 For many mathematical theorems \(\tau\), there is a weakest natural subsystem \({\bS}(\tau)\) of \(\bZ_2\) such that \({\bS}(\tau)\) proves \(\tau\). Very often, if a theorem of ordinary mathematics is proved from the weakest possible set existence axioms, the statement of that theorem will turn out to be provably equivalent to those axioms over a still weaker base theory. Moreover, it has turned out that \({\bS}(\tau)\) often belongs to a small list of specific subsystems of \(\bZ_2\) dubbed \(\RCA_0\), \(\WKL_0\), \(\ACA_0\), \(\ATR_0\) and \(({\bPi}^1_1{\Hy}{\bCA})_0\),  respectively.[27]  The systems are enumerated in increasing strength. \(\ACA_0\) is actually the same theory as \((\Pi^1_0{\Hy}\bCA)_0\). The main set existence axioms of \(\RCA_0\), \(\WKL_0\), \(\ACA_0\), \(\ATR_0\), and \(({{\bPi}}^1_1{\Hy}{\bCA})_0\) are recursive comprehension, weak König’s lemma, arithmetical comprehension, arithmetical transfinite recursion, and \(\bPi_1^1\)-comprehension, respectively. \(\ACA_0\) is actually the same theory as \((\Pi^1_0{\Hy}\bCA)_0\). For exact definitions of all these systems and their role in reverse mathematics see Simpson 1999. Examples of mathematical statements provable in \(\RCA_0\) are the intermediate value theorem and the Baire category theorem. Reversals for \(\WKL_0\) are the Heine/Borel covering lemma and the local existence theorem for solutions of ordinary differential equations. Among the many reversals for \(\ACA_0\), \(\ATR_0\), and \((\bPi^1_1{\Hy}{\bCA})_0\) one finds the existence of maximal ideals in countable rings, Ulm’s theorem, and the Cantor-Bendixson theorem, respectively.