A carregar...
Publicação
On the Proof Theory of Modal Logics
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 660.28 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
This thesis aims at presenting a proof-theoretical analysis of modal logics.
Modal logics extend classical propositional logic by adding to the language operators ′□′
and ′♢
′
, expressing necessity and possibility. In this work, we will be focusing on the modal logics in the 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 the study of sequent systems for this family of
logics. The systems we present are based on Gentzen’s calculus G3cp, 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 [2, 3]
and tableau [10]. Moreover, labels can represent, not only worlds in a model, but also truth values [28].
We discuss several results that have been obtained in the literature for this family of modal logics, such
as admissibility of weakening, contraction, and most notably cut-admissibility, 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 S4 which we take as a case
study.
Descrição
Tese de Mestrado, Matemática, 2024, Universidade de Lisboa, Faculdade de Ciências
Palavras-chave
Teoria da demonstração Lógica modal Cálculo de sequentes Dedução etiquetada Decidibilidade Teses de mestrado - 2024