Are key theorems finitistically reducible?

Question

Simpson writes on page 378 of his Subsystems of Second Order Arithmetic:

"For example, all of the following key theorems of infinitistic mathematics are provable in WKL$_0$ and therefore, by theorem IX.3.16, reducible to finitism. (1) The Heine/Borel covering theorem for closed bounded subsets of $\mathbb R^n$ or for closed subsets of any compact metric space. (2) Basic properties of continuous real-valued functions of several real variables. (3) The local existence theorem for solutions of ordinary differential equations. (4) The Hahn/Banach theorem in separable Banach spaces. (5) The existence theorem for prime ideals in countable commutative rings. (6) Existence and uniqueness of the algebraic closure of a countable field. (7) Orderability and existence of the real closure of a countable formally real field."

This point of view apparently follows Hilbert's. However, the applicability of Theorem IX.3.16 to a sentence requires it to be in $\Pi^0_2$ form, which is not the case for the "key theorems" Simpson mentioned. What relevance does it have for the specific result called Heine/Borel covering etc., that it can be included in a theory that is finitistically reducible for $\Pi^0_2$-sentences (which Heine/Borel itself is not)? What does Simpson mean here exactly?

Answer 1

There are various problems with finitistic reducibility as Simpson develops it; for a survey, see §5.3 of my Stanford Encyclopedia of Philosophy entry on reverse mathematics. I tend to agree that the problem you raise is a worry for these kinds of reductionist programme—it also applies to the predicative reductionism that Simpson develops in §5 of his 1985 paper 'Friedman’s Research on Subsystems of Second Order Arithmetic', in which $\mathsf{ATR}_0$ plays the role of $\mathsf{WKL}_0$ and the theory of ramified analysis up to $\Gamma_0$ plays the role of $\mathsf{PRA}$.

These kind of reductionist views stem ultimately from the conservativity programme espoused by Hilbert, under which 'real' (meaningful, finitary) sentences are distinguished from 'ideal' (meaningless, infinitary) ones, and the ideal part of a theory is supposed to only play an instrumental role in deriving real consequences. This does not sit well with Simpson's tendency (understandable, given the success of reverse mathematics in establishing equivalences between important theorems and independently motivated subsystems of second-order arithmetic) to emphasise the theorems that one can prove in these subsystems (e.g. the Heine–Borel theorem in $\mathsf{WKL}_0$) rather than their $\Pi^0_1$ consequences. One could, if one wanted to be charitable, say that this is just a matter of emphasis, and the real view of the finitistic reductionist is that it's those $\Pi^0_1$ consequences that really matter.

To spell out the point more clearly, and give a direct answer to the question: I think the view has to be that "key theorems" like the Heine–Borel theorem being provable in a finitistically reducible system like $\mathsf{WKL}_0$ has only instrumental value, but that (because they are key theorems, used in many proofs) this instrumental value is substantial, even if the finitistic reductionist's official view is that they are (in and of themselves) meaningless ideal statements. However, as pointed out by Burgess (2010) and others, even this view runs into substantial difficulties.