The following quote by G. Kreisel is well-known in proof theory circles:
What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?
The canonical interpretation of Kreisel’s words have given rise to U. Kohlenbach’s proof mining program, about which others are much more qualified to speak. An unorthodox (non-standard?) interpretation of Kreisel’s question is as follows:
Can we somehow ‘lift’ proofs in a restricted language to interesting proofs in a richer language?
The answer is ‘yes’ and I will present an example based on something most logicians will be familiar with: Specker sequences. In general, many ‘reversals’ from Reverse Mathematics (RM) can be almost verbatim lifted to interesting results in third-order (and higher) arithmetic, as discussed in [Sa20a, Sa20b].
Finally, lest I be misunderstood, let me make the following very clear: there is no known ”meta-theorem” that governs these results: lifting proofs just works for many examples from RM. The young whippersnapper should try to obtain such a meta-theorem while the rest withhold judgement. Indeed, interesting observations in the sciences cannot always be made fully formal.
Summary of results
Going back to Specker in [Spe49], there exist Specker sequences, i.e. increasing and (Turing) computable sequences of rationals in the unit interval that do not converge to any computable real. This construct is used in RM to establish (b) => (c) in the following theorem from [Si09, III.2].
Over RCA, the following are equivalent:
(a) arithmetical comprehension as in ACA
(b) MCT monotone convergence theorem for sequences in .
(c) The existence of the range of any function .
Below, I show that the implication (b) => (c) can be lifted almost verbatim to third-order arithmetic to yield an interesting and much more general result about convergence theorems for nets, as follows. Note that RCA is Kohlenbach’s base theory from higher-order RM ([Ko05]), while QF-AC is a fragment of countable choice.
Over RCA + QF-AC, we have (b’) => (c’), where
(b’) MCT: the monotone convergence theorem for nets indexed by Baire space in .
(c’) The existence of the range of any functional .
Note that (c’) is just (c) with the domain ‘bumped up’ one type. The same is true to some extent for (b) and (b’). What is interesting is that nets constitute the generalisation of sequences to (possibly) uncountable index sets, going back about a century to Moore-Smith [MooSmi22].
The first reversal in SOSOA
In this section, we consider the well-known proof of (b) => (c) from [Si09, III.2] involving Specker sequences. This constitutes the first reversal in Simpson’s excellent monograph on RM.
First of all, we distill the essence of the proof (b) => (c), as follows.
1) Fix and define the Specker sequence .
2) Note that MCT applies and let be .
3) Establish the following equivalence (for any ):
4) Apply -comprehension to this formula, yielding the set needed for (c).
The idea underlying the previous proof is simple: the range of is ‘coded’ as a Specker sequence and the limit allows us to write the -formula expressing that is in the range of , as a -formula. For the latter, set existence is guaranteed by RCA.
Lifting the first reversal in SOSOA.
We now ‘lift’ the proof of (b) => (c) in the previous section to a proof of (b’) => (c’). We only need a minimal modification of the steps 1) – 4), and the following axiom, which follows from countable choice QF-AC:
Now observe that the following steps 1′) – 4′) establish (b’) => (c’). The technical details concerning nets can be found in e.g. [Sa20a].
1′) Fix and define the Specker net , where is a finite sequence of reals in (without repetition) with length . These sequences are ordered by inclusion.
2′) Note that this net is monotone, in that . Hence, MCT applies and let be the limit .
3′) Establish the following equivalence (for any ):
4′) Apply -comprehension to this formula, yielding the set needed for (c’).
While the technical details are different, the main idea of the proof is exactly the same: the range of is ‘coded’ as a Specker net and the limit allows us to write the formula expressing that is in the range of , as a ‘-formula’, for which set existence is guaranteed by RCA QF-AC, a conservative extension of RCA.
Finally, we note that the above ‘lifted’ proof is not optimal, in that a slight extension of the base theory was needed. In fact, (b’) => (c’) is proved in the base theory in [Sa19].