  The program of so-called reverse mathematics developed by, in particular, Friedman and Simpson, is another continuation of Hilbert’s program. In the face of Gödel’s results showing that not all of classical mathematics can be reduced to the finitary, they seek to answer the question: how much of classical mathematics can be so reduced? Reverse mathematics seeks to give a precise answer to this question by investigating which theorems of classical mathematics are provable in weak subsystems of analysis which are reducible to finitary mathematics (in the sense discussed in the preceding paragraph). A typical result is that the Hahn-Banach theorem of functional analysis is provable in a theory known as \(WKL_0\) (for “weak König lemma”); \(WKL_0\) is conservative over \(\PRA\) for \(\Pi^{0}_2\) sentences (i.e., sentences of the form \(\forall x\exists yA(x, y)\). (See  Simpson 1988  for an overview and  Simpson 1999  for a technical treatment.)