Em colaboração com Paulo Oliva, concebemos uma interpretação funcional da aritmética que, ao contrário da original devida a Gödel em 1958, não quer saber de testemunhas precisas de quantificações existenciais, mas apenas de suas majorações. Esta interpretação sustenta uma forma geral do teorema FAN de Brouwer e, simultaneamente, o lema fraco de König. O artigo intitula-se Bounded functional interpretation (Annals of Pure and Applied Logic 135, 73-112, 2005). A nova interpretação difere conceptualmente da interpretação monótona de Kohlenbach (que tem sido explorada, com grande sucesso, no programa de “Proof Mining”). A nossa interpretação “injecta uniformidades” que não são existem no universo dos conjuntos preservando, no entanto, proposições “reais”. Também fornece uma forma nova (e simples) de olhar para a teoria do “Proof Mining”. Escrevi recentemente uma pequena monografia sobre estes assuntos (Logic Colloquium'07, Françoise Delon et al. org., Cambridge University Press 2010, pp. 32-81).
A formalização da matemática em sistemas aritméticos de segunda-ordem tem uma história longa e distinta. Pode dizer-se que remonta a Richard Dedekind e que foi objecto da atenção de, entre outros, Hermann Weyl, David Hilbert, Paul Bernays, Gaisi Takeuti, Solomon Feferman, Harvey Friedman e Stephen Simpson. Na década de oitenta, Samuel Buss introduziu sistemas aritméticos relacionados com classes notáveis da complexidade computacional.
Em Groundwork for weak analysis (The Journal of Symbolic Logic 67, 557-578, 2002), eu e António M. Fernandes desenvolvemos os princípios mais básicos da análise matemática num sistema formal associado à computabilidade em tempo polinomial (um sistema fraco da análise). Um corolário interessante deste trabalho é o resultado de que a teoria dos corpos ordenados realmente fechados (de Tarski) é interpretával na teoria aritmética de Robinson Q. Por outras palavras, a álgebra e análise elementares (incluindo a geometria analítica) interpretam-se numa teoria aritmética sem indução.
Os artigos ainda não publicados devem ser considerados rascunhos. Não os citem sem a minha permissão.
Quanto aos artigos publicados, note o leitor que os artigos on line são manuscritos que deram origem às versões publicadas. Há algumas diferenças entre os manuscritos e os artigos publicados. Se pretender citar um artigo deve consultar a versão publicada.
Outros artigos disponíveis
The bounded functional interpretation of the double negation shift, com Patrícia Engrácia. The Journal of Symbolic Logic 75, pp. 759-773 (2010).
Commuting conversions vs. the standard conversions of the “good” connectives, com 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, com Gilda Ferreira. Archive for Mathematical Logic 47, pp. 91-100 (2008).
The Riemann integral in weak systems of analysis, com Gilda Ferreira. Journal of Universal Computer Science, 14, no. 6, pp. 908-937 (2008).
Bounded functional interpretation and feasible analysis, com Paulo Oliva. Annals of Pure and Applied Logic 145, pp. 115-129 (2007).
Bounded modified realizability, com Ana Nunes. The Journal of Symbolic Logic 71, pp. 329-346 (2006).
Counting as integration in feasible analysis, com Gilda Ferreira. Mathematical Logic Quarterly 52, pp. 315-329 (2006).
Basic applications of weak König's lemma in feasible analysis, com António Fernandes. In "Reverse Mathematics 2001", organizado por Stephen Simpson. Lecture Notes in 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, pp. 83-91, 2005.
Two general results on intuitionistic bounded theories, Mathematical Logic Quarterly 45: 399-407, 1999.
Extracting algorithms from intuitionistic proofs, com António 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", organização de Aldo Ursini e 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 "Actas do III Encontro dos Algebristas Portugueses", organização de 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.
[Os artigos acima são apenas para uso pessoal. Na maior parte dos casos, os editores são detentores do Copyright ©.]
Para ver ou imprimir os artigos 'on-line' desta página necessita de ter, ou necessita de fazer o 'download' duma cópia do Adobe Acrobat Reader.