Mathematical Logic

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



Fernando Ferreira

[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.