Por Maria Osório Costa (CMAFcIO, Faculdade de Ciências da Universidade de Lisboa).

This talk is a report on my Master's Thesis, supervised by Professor Fernando Ferreira and Doctor Marianna Girlando. The thesis aims at presenting a proof-theoretical analysis of modal logics.

Modal logics extend classical propositional logic by adding to the language operators $'\Box'$ and $'\Diamond'$, expressing necessity and possibility. In this work, we will focus on the modal logics in the $\mathbf{S5}$-cube, built from the basic modal logic $\K$ by considering combinations of certain frame conditions such as reflexivity, symmetry and transitivity.

We are interested in studying sequent systems for this family of logics. The systems we present are based on Gentzen's calculus $\G$, with two additional pairs of rules for the modal operators and where the language has been extended with labels. These labels annotate formulas denoting worlds in a Kripke-model where they are satisfied. Note that this idea is not limited to sequent calculi, in fact, it has been studied for other formal systems such as natural deduction and tableaux. Moreover, the labels can represent, not only worlds in a model but also truth values.

We discuss several results that have been obtained in the literature for this family of modal logics, such as the admissibility of weakening, contraction, and most notably of the cut rule, which ensures the subformula property. Furthermore, we investigate proof-search termination strategies, which allows us to obtain countermodels for non-derivable sequents, and prove, via proof-theoretical tools, decidability and the finite model property for the logics in the cube, in particular for $\K$ and $\mathbf{S4}$ which we take as a case study.

Transmissão via Zoom.