Proof-theoretic uniform boundedness and bounded collection principles and countable Heine-Borel compactness (Q2238150)

In the recent work [Adv. Math. 354, Article ID 106728, 55 p. (2019; Zbl 1446.03100)], which we reviewed (see that review for more context), \textit{F. Ferreira} et al. showed how a previously mysterious empirical fact of proof mining -- namely that in a previous extraction [\textit{U. Kohlenbach}, Adv. Math. 226, No. 3, 2764--2795 (2011; Zbl 1223.03041)] of a functional out of an argument, originally due to Browder, the use of bar recursion is not needed even though the principles used in the proof would seem to require it -- may be actually explained by carrying out the extraction through the use of the so-called \textit{bounded functional interpretation} due to \textit{F. Ferreira} and \textit{P. Oliva} [Ann. Pure Appl. Logic 135, No. 1--3, 73--112 (2005; Zbl 1095.03060)] for a system containing principles which are set-theoretically false (`bounded collection') but which are nonetheless trivialized by the interpretation. The intuition for the use of these principles was governed by a `countable Heine-Borel covering principle' (CHBC), whose statement was given there as follows: \[(\forall n \in \mathbb{N} (\Omega_n\ \text{is open}) \land \forall x \in X \exists n \in \mathbb{N} (x \in \Omega_n)) \to \exists n \in \mathbb{N} \forall x \in X \exists m \leq n (x \in \Omega_m).\] In the paper under review, U. Kohlenbach shows that this false principle can only be used in informal parlance and not as a formal statement whose use could be potentially removed by a proof interpretation (note that he uses his own `monotone' functional interpretation instead of the bounded one, but it is remarked that the results ``carry over \textit{mutatis mutandis}''). Specifically, he gives an explicit sentence \(A\) of sufficiently low complexity that the metatheorems of proof mining do apply for it, such that \(A\) can be proven using the formalized CHBC but which nevertheless is false in arbitrary hyperbolic (even Hilbert) spaces. In a follow-up result, \textit{F. Ferreira} [Lect. Notes Comput. Sci. 12813, 199--203 (2021; Zbl 07495168)] confirmed this line of thought, showing firstly that the formalized CHBC can even be shown to be inconsistent when the theory is augmented with axioms which express that the underlying space is infinite-dimensional and secondly that one can deduce from this inconsistency some `metatheorem failures' which are similar to the ones in the paper under review.