In collaboration with Paulo Oliva, we defined in 2004 a new functional interpretation of arithmetic. The new interpretation differs from Gödel's original dialectica interpretation by not caring for precise witnesses of existential statements. Instead, it focus on bounds for such witnesses. The new interpretation sustains (without the need of bar recursors) Brouwer's FAN theorem and weak König's lemma. These principles trivialize under the bounded functional interpretation (in the same sense that Markov's principle trivializes under the dialectica interpretation). The paper is entitled Bounded functional interpretation (Annals of Pure and Applied Logic 135, 73-112, 2005. Doi: 10.1023/A:1004377219147). 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 clarifies the theoretical underpinnings of Proof Mining.
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, 557-578, 2002. Doi:10.2178/jsl/1190150098), 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 there may be differences between the manuscripts and the published versions. Should you actually want to cite a paper, please consult the published version (e.g., through the DOI).
Other papers available
On the removal of weak compactness arguments in proof mining, com Laurențiu Leuştean e Pedro Pinto. Advances in Mathematics 354 (2019).
On some semi-constructive theories related to Kripke-Platek set theory. In: “Feferman on Foundations. Logic, Mathematics, Philosophy,” edited by G. Jäger and W. Sieg. Outstanding Contributions to Logic, Springer International, 2018, pp. 347-384.
A herbrandized functional interpretations of classical logic, with Gilda Ferreira. Archive for Mathematical Logic 56(5-6), pp. 523-539 (2017).
Analysis in weak systems. In: “Logic and Computation. Essays in Honour of Amílcar Sernadas,” edited by C. Caleiro et al. College Publications, 2017, pp. 231-261.
Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic, with Bruno Dinis. Mathematical Logic Quarterly 63, pp. 114-123 (2017).
An elementary proof of strong normalization for atomic F, with Gilda Ferreira. Bulletin of the Section of Logic 45, pp. 1-15 (2016).
Spector's proof of the consistency of analysis. In: “Gentzen's Centenary. The quest for consistency,” edited by R. Kahle and M. Rathjen. Springer, 2015, pp. 278-300.
The faithfulness of Fat: a proof-theoretic proof, with Gilda Ferreira. Studia Logica 103, pp. 1303-1311 (2015).
Nonstandardness and the bounded functional interpretation, with Jaime Gaspar. Annals of Pure and Applied Logic 166, pp. 665-740 (2015).
The finitistic consistency of Heck's predicative Fregean system, with Luís Cruz-Filipe. Notre Dame Journal of Formal Logic 56, pp. 61-79 (2015).
A new computation of the Sigma-ordinal of KPw. The Journal of Symbolic Logic 79, pp. 306-324 (2014).
The faithfulness of atomic polymorphism, with Gilda Ferreira. In: “Trends in Logic XIII,” edited by A. Indrzejczak, J. Kaczmarek and Z. Zawidzki. Wydawnictwo Uniwersytetu Lodzkiego, Lodz 2014, pp. 55-65.
Interpretability in Robinson's Q, with Gilda Ferreira. The Bulletin of Symbolic Logic 19, pp. 289-317 (2013).
Techniques in weak analysis for conservation results, with António Fernandes and Gilda Ferreira. In “Studies in Weak Arithmetics II,” edited by P. Cégielski et al. CSLI Publications (Stanford) and Presses Universitaires (Paris 12) 2013, pp. 115-147.
Atomic polymorphism, with Gilda Ferreira. The Journal of Symbolic Logic 78, pp. 260-274 (2013).
A short note on Spector's proof of consistency of analysis. In: “How the World Computes,” edited by B. Cooper, A. Dawar & B. Löwe. Proceedings of the Turing Centenary Conference and CiE 2012, Lecture Notes in Computer Science, vol. 7318, pp. 222-227 (Springer, 2012).
The bounded functional interpretation of the double negation shift, with Patrícia Engrácia. The Journal of Symbolic Logic 75, pp. 759-773 (2010).
Proof interpretations and majorizability. In: “Logic Colloquium'07,” edited by Françoise Delon et al. Cambridge University Press, 2010, pp. 32-81.
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).
www.crcpress.com/Logic-and-Algebra/Ursini-Agliano/p/book/9780824796068
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.
www.emis.de/journals/PM/52f3/pm52f307.pdf
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.
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.