Skip to content

The Proof Theory Blog

Γ ⊨ A ⇒ Γ ⊢ A

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

Lifting proofs: from Specker sequences to nets

Posted on May 30, 2020June 1, 2020 by Sam Sanders

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”

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

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

      Reply

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2023 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT