Bounded functional interpretation (Q2488269)

Gödel's Dialectica interpretation is suitable for extracting precise witnesses from constructive proofs of existential statements (or more generally of \(\forall \exists\)-statements). In the present paper, the authors present a new functional interpretation -- the so called \textit{bounded functional interpretation}, b.f.i. henceforth -- which aims at providing \textit{bounds} for witnessing information. The technique is inspired by previous work on the so-called monotone functional interpretation (developed by Kohlenbach) and it can be enlisted as a new tool in the area of \textit{proof-mining} (i.e. extracting concrete mathematical information from elaboration of mathematical proofs). The main motivation is that, even if sometimes a mathematical existence theorem lacks a constructive or computable realization (think of theorems proven by means of compactness arguments which fail in recursive analysis), it is still possible to devise formal methods to extract effective bounds. In addition, b.f.i. does not require decidability of atomic formulas and it can also yield precise witnesses in certain situations (typically, when the bound determines a finite set of possible solutions or when the relation involved in the witnessing argument meets suitable monotonicity requirements). In essence, the effect of the b.f.i. is the assignment to each arbitrary statements \(A\) of suitable bounded version \((A)^B\) thereof (the bounded functional interpretation of \(A\)). Of course, bounds are to be defined in hereditary style over all types, and this requires a suitable \textit{intensional} notion of majorizability. As to the content of the paper, Section 2 introduces the basic framework where to develop b.f.i.; the language, besides all finite types with basic combinators and ordering at the ground type, is extended with intensional majorizability relations for each finite type and this allows the authors to make the notion of bounded formula precise. Section 3 defines in a natural fashion the map \(A\mapsto A^B\) for \(A\) of arbitrary logical complexity (above the bounded statements) and proves a natural soundness theorem, which hinges upon a monotonicity lemma. The next step (Section 4, Theorem 3) is to characterize the functional interpretation; interestingly, this leads to discover sound principles that are novel with respect to the usual Dialectica interpretation (e.g. bounded versions of choice, independence of premises, Markov's principle, a contrapositive version of bounded collection, a generalization of Brouwer's fan principle, a majorizability axiom, etc.). By contrast with the Dialectica interpretation, some of these principles are classically inconsistent. Sections 5--6 apply the machinery to classical arithmetical systems, including subsystems based on fragments of the Gödel functional systems corresponding to levels of the Grzegorczyk hierarchy. Sections 7--9 show how to interpret via b.f.i. a uniform version of Weak König's Lemma and forms of the so-called uniform boundedness principle of Kohlenbach. {Reviewer's remark: In proof theory there are other examples where witnessing arguments are replaced by suitable majorization arguments combined with cut elimination (asymmetric interpretations). E.g., this is the case for Friedman's theorem of conservativity of WKL\(_0\) over PRA for \(\Pi^0_2\)-formulas. These refined Gentzen-style techniques usually turn out to be enough to obtain the needed conservation theorems or to estimate the provably recursive functions. Question: is there any link with b.f.i.? Certainly, b.f.i. is more powerful since it also applies to higher logical complexity, and not only to the usual \(\forall \exists \)-statements at the ground type}.