Seminário remoto "Lógicos em Quarentena" 08/04/2021 (quinta-feira) 14:00h

[Bruno Lopes]

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