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/CAESt%3DXv_F5c8KLPQeB-vUE%3D0UVXcCv5mv1SePq-%2BpzVwYXG%2BKw%40mail.gmail.com.
