Lifting proofs: from Specker sequences to nets

Introduction

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 $_0$ , the following are equivalent:
(a) arithmetical comprehension as in ACA $_0$
(b) MCT $_{\text{seq}}$ monotone convergence theorem for sequences in $[0,1]$ .
(c) The existence of the range of any function $f:\mathbb{N}\rightarrow\mathbb{N}$ .

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 $_0^\omega$ is Kohlenbach’s base theory from higher-order RM ([Ko05]), while QF-AC $^{0,1}$ is a fragment of countable choice.

Over RCA $_0^\omega$ + QF-AC $^{0,1}$ , we have (b’) => (c’), where
(b’) MCT $_{\text{net}}$ : the monotone convergence theorem for nets indexed by Baire space in $[0,1]$ .
(c’) The existence of the range of any functional $Y:\mathbb{N}^\mathbb{N}\rightarrow \mathbb{N}$ .

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 $f:\mathbb{N}\rightarrow \mathbb{N}$ and define the Specker sequence $c_{n}:=\sum_{i=0}^{n}2^{-f(i)}$ .
2) Note that MCT $_{\text{seq}}$ applies and let $c$ be $\lim_{n\rightarrow\infty}c_{n}$ .
3) Establish the following equivalence (for any $k\in \mathbb{N}$ ):

$(\exists m \in \mathbb{N})(f(m)=k)\leftrightarrow (\forall n \in \mathbb{N})\big( |c_{n}-c|<2^{-k}\rightarrow (\exists i\leq n)(f(i)=k) \big),$

4) Apply $\Delta_{1}^{0}$ -comprehension to this formula, yielding the set $\{k\in \mathbb{N}: (\exists n\in \mathbb{N})(f(n)=k)\}$ needed for (c).

The idea underlying the previous proof is simple: the range of $f$ is ‘coded’ as a Specker sequence $(c_n)_{n\in \mathbb{N}}$ and the limit $c$ allows us to write the $\Sigma_1^0$ -formula expressing that $k$ is in the range of $f$ , as a $\Delta_1^0$ -formula. For the latter, set existence is guaranteed by RCA $_0$ .

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 $^{0,1}$ :

( $\Delta$ -CA) $\begin{align*}(\forall Y^{2}, Z^{2})\big[ (\forall n^{0})\big( (\exists f^{1})&(Y(f, n)=0) \leftrightarrow (\forall g^{1})(Z(g, n)=0) \big) \\& \rightarrow (\exists X^{1})(\forall n^{0})(n\in X\leftrightarrow (\exists f^{1})(Y(f, n)=0)\big].\notag\end{align*}$

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 $Y:\mathbb{N}^{\mathbb{N}}\rightarrow \mathbb{N}$ and define the Specker net $c_{w}:=\sum_{i<|w|} 2^{-Y(w(i))}$ , where $w$ is a finite sequence of reals in $[0,1]$ (without repetition) with length $|w|$ . These sequences are ordered by inclusion.
2′) Note that this net is monotone, in that $v\subseteq w \rightarrow c_v \leq c_w$ . Hence, MCT $_{\text{net}}$ applies and let $c$ be the limit $\lim_{d} c_d$ .
3′) Establish the following equivalence (for any $k\in \mathbb{N}$ ):

$(\exists f \in \mathbb{N}^{\mathbb{N}})(Y(f)=k)\leftrightarrow (\forall w )\big( |c_{w}-c|<2^{-k}\rightarrow (\exists i <|w|)(Y(w(i))=k) \big),$

4′) Apply $\Delta$ -comprehension to this formula, yielding the set $\{k\in \mathbb{N}: (\exists f\in \mathbb{N}^{\mathbb{N}})(Y(f)=k)\}$ needed for (c’).

While the technical details are different, the main idea of the proof is exactly the same: the range of $Y$ is ‘coded’ as a Specker net $\lambda w. c_w$ and the limit $c$ allows us to write the formula expressing that $k$ is in the range of $Y$ , as a ‘ $\Delta$ -formula’, for which set existence is guaranteed by RCA $_0^\omega+$ QF-AC $^{0,1}$ , a conservative extension of RCA $_0$ .

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].

References

[Ko05] U. Kohlenbach, Higher order reverse mathematics, Reverse mathematics 2001, Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295.

[MooSmi22] E. H. Moore and H. Smith, A General Theory of Limits, Amer. J. Math. 44 (1922), 102–121.

[Sa19] S. Sanders, Plato and the foundations of mathematics, Submitted, arxiv: https://arxiv.org/ abs/1908.05676 (2019), pp. 40.

[Sa20a] _____, Lifting recursive counterexamples to higher-order arithmetic, Proceedings of LFCS2020, Lecture Notes in Computer Science, Springer (2020).

[Sa20b] ____, Lifting countable to uncountable mathematics, Submitted, arxiv: https://arxiv. org/abs/1908.05677 (2020), pp. 21.

[Si09] S. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, CUP, 2009.

[Spe49] E. Specker, Nicht konstruktiv beweisbare S ̈atze der Analysis, J. Symbolic Logic 14 (1949), 145–158 (German).

2 thoughts on “Lifting proofs: from Specker sequences to nets”

Andrei Sipoș says:
May 30, 2020 at 12:41 pm
“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.”
I think this touches a bit on one of the points that Gowers makes in his two cultures essay.
1. Sam Sanders says:
  May 30, 2020 at 7:35 pm
  Thanks for the suggestion. I have actually attended a talk by Gowers on the foundations of mathematics that was quite insightful. He was also quite impressed by Harvey Friedman’s visit to That Other Place.