 We described the system \(\bZ_2\) of second order arithmetic already at the end of section 3.2. It was viewed as the “next”system to be proved consistent—after first-order arithmetic PA had been shown to be. As we mentioned \(\bZ_2\) is also called “analysis”, because it allows the development of classical mathematical analysis: coding real numbers and continuous functions as sets of natural numbers, a good theory of the continuum can be developed from \(\bZ_2\)’s axioms. Indeed, Hermann Weyl showed in 1918 that a considerable portion of analysis can be developed in small fragments of \(\bZ_2\) that are actually conservative over PA. The idea of singling out the minimal fragment of \(\bZ_2\) required to expose a particular part of ordinary mathematics led in the 1980s to the research program of reverse mathematics. However, before discussing that program, we are going to proof-theoretic investigations of \(\bZ_2\) and its subsystems that have been a focal point until the very early 1980s.