On the removal of weak compactness arguments in proof mining

DOI10.1016/J.AIM.2019.106728MaRDI QIDQ2324564zbMATH OpenOpenAlexFDO

Publication date 11 September 2019

Published in Advances in Mathematics (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1810.01508

bounded functional interpretation conservation results nonexpansive mappings proof mining quantitative versions rates of metastability

Mathematics Subject Classification ID

Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Contraction-type mappings, nonexpansive mappings, (A)-proper mappings, etc. (47H09) Fixed-point theorems (47H10) Nonlinear ergodic theorems (47H25) Iterative procedures involving nonlinear operators (47J25)

Abstract: The main observation of this paper is that some sequential weak compactness arguments in Hilbert space theory can be replaced by Heine/Borel compactness arguments (for the strong topology). Even though the latter form of compactness fails in (infinite-dimensional) Hilbert spaces, it nevertheless trivializes under the so-called bounded functional interpretation. As a consequence, the proof mining programme of extracting computational bounds from ordinary proofs of mathematics can be applied to {em modified proofs} which use these false Heine/Borel compactness arguments. Additionally, the bounded functional interpretation provides good logical guidance in formulating quantitative versions of analytical statements. We illustrate these claims with three minings. The bounded functional interpretation is here used for the first time in proof mining.

Review text

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.

Recommendations

Cites work

Cited in

(32)

This page was built for publication: On the removal of weak compactness arguments in proof mining

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2324564)