Page 44 - Textos de Matemática Vol. 38

36 FERNANDO FERREIRA
In particular, the theory E-PRAω + bAC0,1 + AC1,0 + Σ1-UB proves that ≤ qf qf 0
every type 2 functional is uniformly continuous in the Cantor space. It can indeed be shown that all real-valued functions are locally uniformly continuous (the fact that R is locally compact plays a decisive role here). Not only is it consistent to assume this postulate in a classical setting with a bit of choice, we also know that the consequences of this assumption which have the sentential form ∀x0/1∃yAqf(x,y), with Aqf quantifier-free, are true and, additionally, some explicit computational information can be extracted from them.
Question 6. Do we have similar results to the above in which it is provable that all functionals of type 2 in the Baire space are continuous (note that the Baire space is not locally compact)?
5 Coda
There are various motivations for engaging in constructivism. First, there is the philosophical motivation of rebuffing the dominant (sometimes closet, most times unreflective) platonism/formalism of ordinary mathematical prac- tice. This motivation has sources in Leopold Kronecker and L. E. J. Brouwer, both preoccupied with the mounting estrangement of mathematics from “con- crete or constructive meaning” provoked by modern abstract mathematics and, in particular, by set theory. This concern is exemplified by the works of Andrey Markov, Arend Heyting, Errett Bishop and Per Martin-Lo¨f. The philosophi- cal motivation may also lead to the consideration of conceptual questions like “What are the computable functionals of finite-type?” as though they should have answers. Of course, this particular question does have reasonable answers in types (e.g.) 1, 2 or 1 → 1, but it may be an illusion to think that the question is well-posed in general. Nevertheless, working on these questions (never mind the motivation) is far from being a futile exercise because some good mathe- matics did arise from it, e.g. the discovery of interesting and illuminating type theoretic structures.
Another motivation, which often comes hand in hand with the above, is that of extracting computational content from theorems of mathematics. If the results have the form ∀x∃yA(x, y) and if x and y are of low type (0 or 1), then in constructive mathematics one can elicit a computable witness. Nevertheless, it is not the case that in order to be able to extract computational information one must engage in constructive reasoning. It may happen that one can use non-constructive principles and/or (even) false set-theoretic principles and have metatheorems that guarantee that, if the matrix A is suitably restricted, then the proofs elicit computational witnesses or bounds. In the classical setting, for well-known reasons, the present methodologies require that the matrix A be quantifier-free, in which case computational witnesses for y of type 0 always exist anyway: for a trivial reason – by search. However, Proof Theory provides a