Ola Valéria, Muito bacana, vou dar uma olhada, e passo a ele. Vai ficar muito satisfeito.
Abraços,. Walter Em dom., 1 de ago. de 2021 04:19, Valeria de Paiva < valeria.depa...@gmail.com> escreveu: > Pois e' Walter, a minha tese de doutorado fala justamente da Interpretacao > Dialectica, faz uma versao categorica e usa a variante de J. Diller e Nahm > pra mostrar como voltar pra logica intuicionista. > > A tese esta' em https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf, > a parte sobre Dialectica e Diller-Nahm num artigo em > http://www.cs.bham.ac.uk/~vdp/publications/dial87.pdf. > > abracos, > Valeria > > On Sat, Jul 31, 2021 at 8:28 AM Walter Carnielli <walte...@unicamp.br> > wrote: > >> Colegas: >> >> Gostaria de divulgar aqui um livro talvez pouco conhecido, mas que >> traz uma excelente visão sobre a interpretação funcional da >> aritmética, análise e teoria dos conjuntos. O livro revisita a famosa >> interpretação dialética de Gödel da aritmética de Heyting e sua >> generalização para tipos finitos, e expõe muito bem este temas, >> incluindo a interpretação de Diller-Nahm na aritmética de Heyting e >> Peano em tipos finitos e outros temas clássicos. >> >> Justus Diller foi meu "Gastgeber" (anfitrião) no tempo que passei em >> Münster como bolsista da Humboldt Stiftung, é um excelente lógico, >> matemático e filósofo da matemática e da lógica (embora talvez ele >> nem pretenda isso...). Foi também visitante no CLE Unicamp. >> >> Aprendi muito com ele. Recomendo realmente este livro. >> >> Abs, >> >> Walter >> >> [Inglês abaixo, c/c Diller] >> =================== >> Dear Colleagues: >> >> I would like to share here a book that is perhaps little known, but >> which provides an excellent insight into functional interpretation of >> arithmetic, analysis and set theory. The book revisits the famous >> Gödel's dialectical interpretation of Heyting arithmetic and its >> generalization to finite types, and exposes these very well, including >> the Diller-Nahm's interpretation of Heyting and Peano arithmetic on >> finite types, and other classical topics. >> >> Justus Diller was my "Gastgeber" (host) during my time in Münster on >> a Humboldt Stiftung scholarship, is an excellent logician, >> mathematician and philosopher of mathematics and logic (although >> perhaps he doesn't even intend to...). He was also a visitor at CLE >> Unicamp. >> >> I learned a lot from him. I really recommend this book. >> Best, >> Walter >> ================================== >> "Functional Interpretations: From the Dialectica Interpretation to >> Functional Interpretations of Analysis and Set Theory " >> >> Justus Diller (Univ of Münster, Germany) >> World Scientific Pub, 2019 >> >> >> https://www.worldofbooks.com/en-au/books/justus-diller-univ-of-munster/functional-interpretations-from-the-dialectica-interpretation-to-functional-inte/9789814551397 >> >> This book gives a detailed treatment of functional interpretations of >> arithmetic, analysis, and set theory. The subject goes back to >> Goedel's Dialectica interpretation of Heyting arithmetic which >> replaces nested quantification by higher type operations and thus >> reduces the consistency problem for arithmetic to the problem of >> computability of primitive recursive functionals of finite types. >> Regular functional interpretations, in particular the Dialectica >> interpretation and its generalization to finite types, the Diller-Nahm >> interpretation, are studied on Heyting as well as Peano arithmetic in >> finite types and extended to functional interpretations of >> constructive as well as classical systems of analysis and set theory. >> Kreisel's modified realization and Troelstra's hybrids of it are >> presented as interpretations of Heyting arithmetic and extended to >> constructive set theory, both in finite types. They serve as >> background for the construction of hybrids of the Diller-Nahm >> interpretation of Heyting arithmetic and constructive set theory, >> again in finite types. All these functional interpretations yield >> relative consistency results and closure under relevant rules of the >> theories in question as well as axiomatic characterizations of the >> functional translations. >> >> Table of Contents >> >> Arithmetic: Primitive Recursive Functionals; - (Diller - Nahm) >> Interpretation of Heyting Arithmetic in Finite Types; The Dialectica >> Interpretation and Equality Functionals; Simultaneous Recursions in >> Linear Types; Computability, Consistency, Continuity; Modified >> Realization and its Hybrids; Hybrids of the -Interpretation; >> N-Interpretations; Interpretations of Classical Arithmetic; >> Extensionality and Majorizability; Analysis: Bar Recursive >> Functionals; - and Dialectica Interpretation of Bar Induction by Bar >> Recursion; Functional Interpretations of Classical Analysis; >> Computability of Bar Recursive Functionals; Set Theory: Constructive >> Set Functionals; Kripke - Platek Set Theory and Its Functional >> Interpretations; Constructive Set Theory and Its -Interpretation; >> Modified Realizations of Constructive Set Theory; The Q-Hybrid of the >> -Interpretation of Constructive Set Theory in Finite Types; >> Majorizability of Constructive Set Functionals. >> >> =========================== >> Walter Carnielli, Professor >> Centre for Logic, Epistemology and the History of Science and >> Department of Philosophy >> University of Campinas –UNICAMP >> 13083-859 Campinas -SP, Brazil >> Phone: (+55) (19) 3521-6517 >> Institutional e-mail: walter.carnie...@cle.unicamp.br >> Website: http://www.cle.unicamp.br/prof/carnielli >> >> -- >> Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" >> dos Grupos do Google. >> Para cancelar inscrição nesse grupo e parar de receber e-mails dele, >> envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. >> Para ver esta discussão na web, acesse >> https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAOrCsLcH_gynoLchVEaTjiCzFNsorDcOVGwMJerKXw_f1A1nNQ%40mail.gmail.com >> . >> > -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAOrCsLda7D%3DpmTw0Ga-2HL0S7mJ25is29Zs%3Dbms2VBuOTX-E_g%40mail.gmail.com.