In collaboration with Paulo Oliva, we defined a new functional interpretation of arithmetic. The new interpretation differs from Gödel's original one by not caring for precise witnesses of existential statements. Instead, it focus on bounds for such witnesses. The new interpretation sustains Brouwer's FAN theorem and (at the same time) weak König's lemma. The paper is entitled Bounded functional interpretation (Annals of Pure and Applied Logic 135, 73-112, 2005). The new interpretation is conceptually different from Kohlenbach's monotone functional interpretation (exploited to great effect in the “Proof Mining” program). Our interpretation injects uniformities which are absent from set-theoretic mathematics, while maintaining unmoved “real” sentences. It also provides a new (and simple) way of looking at the theoretical underpinnings of Proof Mining. I recently wrote a survey paper on these issues (Logic Colloquium'07, Françoise Delon et al. eds., Cambridge University Press 2010, pp. 32-81).
The formalization of mathematics within second-order arithmetic has a long and distinguished history. We may say that it goes back to Richard Dedekind, and that it has been pursued by, among others, Hermann Weyl, David Hilbert, Paul Bernays, Gaisi Takeuti, Solomon Feferman, Harvey Friedman and Stephen Simpson. In the eighties, Samuel Buss introduced systems of arithmetic related with conspicuous classes of computational complexity. In Groundwork for weak analysis (The Journal of Symbolic Logic 67, pp. 557-578, 2002), in colaboration with António M. Fernandes, we developed the most basic principles of analysis within such a feasible system. A rewarding corollary of this work is the result that Tarski's elementary theory of the real closed ordered fields is interpretable in Raphael Robinson's theory of arithmetic Q.
Papers not yet published should be considered drafts. Do not cite them without my permission.
Concerning the published papers, please note that what is posted are manuscripts from which the published versions were created. There will be some differences between the manuscripts and the published versions. Should you actually want to cite a paper, please consult the published version.
Other papers available
The bounded functional interpretation of the double negation shift, with Patrícia Engrácia. The Journal of Symbolic Logic 75, pp. 759-773 (2010).
Commuting conversions vs. the standard conversions of the “good” connectives, with Gilda Ferreira. Studia Logica 92, pp. 63-84 (2009).
Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic 157, pp. 122-129 (2009).
Harrington’s conservation result redone, with Gilda Ferreira. Archive for Mathematical Logic 47, pp. 91-100 (2008).
The Riemann integral in weak systems of analysis, with Gilda Ferreira. Journal of Universal Computer Science, 14, no. 6, pp. 908-937 (2008).
Bounded functional interpretation and feasible analysis, with Paulo Oliva. Annals of Pure and Applied Logic 145, pp. 115-129 (2007).
Bounded modified realizability, with Ana Nunes. The Journal of Symbolic Logic 71, pp. 329-346 (2006).
Counting as integration in feasible analysis, with Gilda Ferreira. Mathematical Logic Quarterly 52, pp. 315-329 (2006).
Basic applications of weak König's lemma in feasible analysis, with António Fernandes. In "Reverse Mathematics 2001", edited by Stephen Simpson. Lecture Notes on Logic (Association for Symbolic Logic), vol. 21, pp. 175-188 (A K Peters, 2005).
A simple proof of Parsons' theorem, Notre Dame Journal of Formal Logic 46: 83-91, 2005.
Two general results on intuitionistic bounded theories, Mathematical Logic Quarterly 45: 399-407, 1999.
Extracting algorithms from intuitionistic proofs, with António M. Fernandes. Mathematical Logic Quarterly 44: 143-160, 1998.
On end-extensions of models of not-exp, Mathematical Logic Quarterly 42: 1-18, 1996.
Some notes on subword quantification and induction thereof, in "Logic and Algebra", edited by Aldo Ursini and Paulo Aglianò. Lectures Notes in Pure and Applied Mathematics, vol. 180, pp. 477-489 (Marcel Dekker, 1996).
What are the forall-sigma^b-1 consequences of T^1-2 and T^2-2?, Annals of Pure and Applied Logic 75: 79-88, 1995.
A note on a result of Buss concerning bounded theories and the collection scheme, Portugaliae Mathematica 52: 331-336, 1995.
A feasible theory for analysis, The Journal of Symbolic Logic 59, 1001-1011, 1994.
Análise, exequibilidade e lógica (in portuguese). In "Actas do III Encontro dos Algebristas Portugueses", edited by Marques de Sá et al., pp. 49-70 (Departamento de Matemática de Coimbra, 1994).
Binary models generated by their tally part, Archive for Mathematical Logic 33: 283-289, 1994.
[The above papers are available for personal use only. In most cases, copyright resides with the publisher.]
Please note that, to view the on-line papers, or to print them out, you need already to have, or will need to download, a copy of the Adobe Acrobat Reader.