On the removal of weak compactness arguments in proof mining (Q2324564)

This paper is part of the research program of proof mining, which aims to use tools from proof theory, one of the main branches of mathematical logic, in order to analyze concrete mathematical proofs as to derive additional information out of them, e.g. bounds or realizers on existentially quantified variables or the weakening of premises. Proof mining has been driven during the last two decades largely by the work of Ulrich Kohlenbach and his students and collaborators, see, e.g. [\textit{U. Kohlenbach}, Applied proof theory. Proof interpretations and their use in mathematics. Berlin: Springer (2008; Zbl 1158.03002)]. A convergence statement is a \(\Pi_3\)-statement and thus a realizer for it (a rate of convergenc) is not guaranteed to exist -- in fact, there exist explicit examples (``Specker sequences'') of sequences of computable reals with no computable limit and thus with no computable rate of convergence. The next best thing is then what Terence Tao called a rate of metastability, i.e. a bound on the \(N\) in the statement \[\forall \varepsilon > 0 \forall g:\mathbb{N} \to \mathbb{N} \exists N \forall i,j \in [N,N+g(N)], d(x_i,x_j) \leq \varepsilon,\] which is a Herbrandization of the Cauchyness property of a sequence. The proof-theoretic tools that are used in proof mining are proof interpretations, e.g. Gödel's \textit{Dialectica} interpretations and variants of it. These are transformations that get applied onto a proof in order to yield realizers for modified versions of the sentences in it (like the Herbrandization above). The realizers are terms of a calculus of functionals determined by the strength of the system in which the proof may be formalized and interpreted. For example, the calculus System T of higher-type primitive recursive functionals due to Gödel suffices for systems around the strength of first-order arithmetic, whereas for stronger systems which contain dependent choice one needs extensions such as Spector's bar recursive functionals. Following the development of abstract logical metatheorems in the mid-2000s [\textit{P. Gerhardy} and \textit{U. Kohlenbach}, Trans. Am. Math. Soc. 360, No. 5, 2615--2660 (2008; Zbl 1130.03036)], rates of metastability started to be extracted for notable convergence results like the mean ergodic theorem. An interesting case was the analysis of the theorems of Browder and Wittmann in [\textit{U. Kohlenbach}, Adv. Math. 226, No. 3, 2764--2795 (2011; Zbl 1223.03041)]. What was curious about it was that even while the proof used dependent choice (in the form of weak compactness of closed convex bounded sets in Hilbert spaces), the corresponding interpreted formula that was actually used in the final analysis (its ``finitary residue'') had a realizer that did not use bar recursion. Thus, the rate of metastability proved to be a low-complexity functional definable in System T. The paper under review represents a successful effort to logically explain this phenomenon. Namely, the authors show that when analyzing the argument of Browder and Wittmann (later also used by Bauschke and Yamada) using the bounded functional interpretation of \textit{F. Ferreira} and \textit{P. Oliva} [Ann. Pure Appl. Logic 135, No. 1--3, 73--112 (2005; Zbl 1095.03060)], the use of weak compactness may be replaced by a form of Heine-Borel compactness if one adds to the higher-type system in which the proof is formalized the false principle of bounded collection, whose functional interpretation is trivially true and thus does not add any (bar recursive) complexity to the realizer. As the paper itself points out, the same kind of argument could also be made using Kohlenbach's monotone functional interpretation and the generalized uniform boundedness principle.