Page 45 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 37
priori witnessing ranges or bounds thereof and, in certain circumstances, bounds which are independent from certain inputs. The names of Harvey Friedman and Ulrich Kohlenbach come to mind for results of this kind: see Propositions 4.9 and 4.10, and Proposition 4.11 for the kind of independency mentioned. In a semi-intuitionistic setting, the matrices A need not be quantifier-free, as the results of Section 2.5 show.
Setting aside philosophical motivations and putting our concern squarely on the extraction of computational content, we can view higher types merely as instrumental in this endeavour. Given the present methodology, we have no choice but to consider all finite types because logic forces us to do so when trying to establish soundness theorems for proof interpretations.
Under suitable representations of ordinary mathematical objects (real num- bers, continuous functions, Polish spaces, etc), we may apply these techniques to results in ordinary mathematical analysis. This is the business of Kohlenbach’s programme of ‘Proof Mining’. The recent introduction of new base types (e.g., types for normed spaces) has given novel applications and further insights into Proof Mining.
Question 7. Extend bounded interpretations to new base types.
Bounded interpretations rely on majorizability considerations. One can ask
the following question:
Question 8. Are there proof interpretations which give to continuity a role anal- ogous to majorizability in bounded interpretations?
I believe that a positive answer to the above question would uncover nice proof-theoretic properties and shed more light on the metamathematics of Brouwerian intuitionism.
In the early sixties, a computational scheme dubbed bar recursion was used by Clifford Spector for interpreting (via Dialectica) full second-order classical arithmetic. Bar recursion is regarded as a somewhat cryptic and mysterious technique and has not been investigated much, but a new form of bar recursion (modified bar recursion) was recently discovered in connection with the principle of ‘double-negation shift’ within the framework of modified realizability. These are interesting developments.
Question 9. Extend bounded interpretations with bar recursive functionals.