Correção: 27/05 (quinta-feira). Em seg, 24 de mai de 2021 08:00, Bruno Lopes <br...@ic.uff.br> escreveu:
> Numa iniciativa conjunta da Sociedade Brasileira de Lógica e do Grupo de > Interesse em Lógica da Sociedade Brasileira de Computação, gostaríamos de > convidar a todos a participarem do Seminário "Lógicos em Quarentena". > Trata-se de um seminário remoto com apresentações informais por membros > da comunidade e espaço para perguntas no fim. As apresentações usualmente > são gravadas e disponibilizadas na página do evento http://lq.sbl.org.br (com > a agenda completa). > > Data: 17 de maio de 2021 (quinta-feira) > Horário: 16:00h GMT-3 > Apresentador: Michael Shulman (University of San Diego) > Título: Linear logic for constructive mathematics > Resumo: > Informally, "constructivism" is a programme of mathematics aiming to > ensure that anything asserted to exist must be explicitly constructed. It > is generally practiced using "intuitionistic logic", which achieves this by > rejecting the "law of excluded middle' (the claim that all statements are > either true or false). The same result is also achieved by Girard's "linear > logic", which instead restricts the number of times each hypothesis can be > used in a proof; but essentially no practicing constructivists today use > linear logic. I will show that intuitionistic and linear approaches to > constructive mathematics are intimately connected, through an > interpretation of the latter into the former based on the categorical "Chu > construction". In particular, many odd features of intuitionistic > mathematics, such as inequality relations, anti-subgroups, and apartness > spaces, arise automatically and unavoidably by translating natural > definitions from linear logic across this interpretation. Thus linear logic > can be used as a "high-level tool" for intuitionistic mathematics, and we > also obtain a "migration path" towards a potential constructive mathematics > based natively on linear logic instead. > > A apresentação ocorrerá pelo Google Meet através do link público > https://meet.google.com/xrc-ujtf-dxk . > > -- > Bruno Lopes > Professor Adjunto > Instituto de Computação > Universidade Federal Fluminense > http://www.ic.uff.br/~bruno > -- 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/CAD-Wq0_xkUp8mEoqCmovsMj2ry8FwNAYiKPUMkKfVqKK1YqoVg%40mail.gmail.com.
