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: 08 de abril de 2021 (quinta-feira)
Horário: 14:00h GMT-3
Apresentador: Mirna Džamonja (Logique Consult & IHPST)
Título: Formalising Ordinal Partition Relations Using Isabelle/HOL
Resumo:
Joint work with with Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson,
FRS, Cambridge
This talk is about an application in set theory of what is sometimes called
'automated theorem proving' by mathematicians. This actually refers to
several different things, including what computer scientists call
formalisation. After briefly discussing general aspects of formalisation,
we shall give an overview of a formalisation project in the proof assistant
Isabelle/HOL of a number of results in ordinal partition relations :
theorems by Erdős–Milner, Specker, Larson and Nash-Williams, leading to
Jean Larson’s proof of the unpublished result by E.C. Milner asserting that
for all $m\in \mathbb N $, $\omega^{\omega }\rightarrow (\omega^{\omega
},m)$. Ordinal partition relations are notoriously hard to study by
classical methods and have the uncanny feature to be mostly interesting for
countable ordinals, where modern set theory seems to be quite silent. Our
approach has been to see if formalising might bring us closer to resolving
some of the many unsolved problems in the area. The talk will focus on the
process of formalisation, the difficulties and the hopes of the process. In
particular, no new proof has yet been obtained by proof assistants. We are
hoping that some of the counter-example finding methods in ordinal
partitions we developed in this formalisation might allow us to make some
modest progress in that direction. The actual formalisation behind our
paper was done by Paulson and is available on the Archive of Formal Proofs.
This project is also a demonstration of working with Zermelo–Fraenkel set
theory in higher-order logic, as developed in this context by Paulson.
A apresentação ocorrerá pelo Google Meet através do link público
https://meet.google.com/xab-ixmv-msn .
--
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 [email protected].
Para ver esta discussão na web, acesse
https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAD-Wq09xqrhGdDuH3F%3DVuhvFEKKYJ%3D2LmQ8P2Qdu0wCHR4Xg0A%40mail.gmail.com.
