 Modern analyses of “finitist mathematics” consider it as situated between PRA and PA. When arguing that Gödel’s second incompleteness theorem refutes Hilbert’s finitist program, von Neumann argued that finitist mathematics is included in PA and, if not there, undoubtedly in \(\bZ_2\). So it is quite clear that a consistency proof of \(\bZ_2\) would use non-finitist principles or that the pursuit of the consistency program would require an extension of the finitist standpoint. In the next section we discuss briefly a variety of extensions and elaborate two in greater detail.