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_qjmHGz72V%3DuCjn_CpjTo3yEBqwyFCcRezMNUmFwL0Ew%40mail.gmail.com.
