Em 2004, 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 majorantes de testemunhas. Esta interpretação sustenta uma forma geral do teorema FAN de Brouwer e, simultaneamente, o lema fraco de König. Estes princípios trivializam sob a interpretação funcional limitada (da mesma forma que o princípio de Markov trivializa sob a interpretação de Gödel). O artigo intitula-se Bounded functional interpretation (Annals of Pure and Applied Logic 135, 73-112, 2005. Doi: 10.1023/A:1004377219147). A nova interpretação difere concetualmente da interpretação monótona de Kohlenbach (que tem sido explorada, com grande sucesso, no programa de “Proof Mining”). A nossa interpretação “injeta uniformidades” que não são existem no universo dos conjuntos preservando, no entanto, proposições “reais”. Também ilumina teoricamente os fundamentos do programa do “Proof Mining”.
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 objeto 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. Doi:10.2178/jsl/1190150098), 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 Q de Raphael Robinson. 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 há algumas diferenças entre os manuscritos e os artigos publicados. Se pretender citar um artigo deve consultar a versão publicada (por exemplo através do apontador DOI).
Outros artigos disponíveis
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”, organizado por G. Jäger e W. Sieg. Outstanding Contributions to Logic, Springer International, 2018, pp. 347-384.
A herbrandized functional interpretations of classical logic, com 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 (C. Caleiro, F. Dionísio, P. Gouveia, P. Mateus, J. Rasga, eds.). College Publications, 2017, pp. 231-261.
Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic, com Bruno Dinis. Mathematical Logic Quarterly 63, pp. 114-123 (2017).
An elementary proof of strong normalization for atomic F, com 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”, organizado por R. Kahle and M. Rathjen. Springer, 2015, pp. 278-300.
The faithfulness of Fat: a proof-theoretic proof, com Gilda Ferreira. Studia Logica 103, pp. 1303-1311 (2015).
Nonstandardness and the bounded functional interpretation, com Jaime Gaspar. Annals of Pure and Applied Logic 166, pp. 665-740 (2015).
The finitistic consistency of Heck's predicative Fregean system, com 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, com Gilda Ferreira. In: “Trends in Logic XII”, organizado por A. Indrzejczak, J. Kaczmarek e Z. Zawidzki. Wydawnictwo Uniwersytetu Lodzkiego, Lodz 2014, pp. 55-65.
Interpretability in Robinson's Q, com Gilda Ferreira. The Bulletin of Symbolic Logic 19, pp. 289-317 (2013).
Techniques in weak analysis for conservation results, com António Fernandes e Gilda Ferreira. In “New Studies in Weak Arithmetics II”, organizado por P. Cégielski, Ch. Cornaros e C. Dimitracopoulos, CSLI Publications (Stanford) and Presses Universitaires (Paris 12), 2013, pp. 115-147.
Atomic polymorphism, com 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”, organizado por 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).
Proof interpretations and majorizability. In: “Logic Colloquium'07,” organizado por Françoise Delon et al. Cambridge University Press, 2010, pp. 32-81.
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”, organizado por 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.
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 “Actas do III Encontro dos Algebristas Portugueses”, organizado por 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.