LIRa Session: Giuseppe Greco and Alessandra Palmigiano

On October 25, Giuseppe Greco and Alessandra Palmigiano will give a LIRa talk. Everyone is cordially invited!

Speakers: Giuseppe Greco and Alessandra Palmigiano
Title: Epistemic updates on algebras, and display-style sequent calculi for dynamic logics
Room: Science Park 904, D1.113
Time: Thursday, 25 October, 15:30-17:30

Abstract: Dynamic logics are nicely behaved from a computational point of view; however, in some cases, such as the Dynamic Epistemic Logics (DEL), they lack properties such as the closure under uniform substitution. This makes their algebraic and proof-theoretic behaviour not so straightforward.

Several proof-systems have been proposed in the literature, which are not entirely satisfactory, either because they are too restricted and not easily generalizable, or because they are unintuitive, or because they are not sound with respect to the standard relational semantics.

In this talk, we present:

(a) a general, algebra-based semantics for the logic of public announcements (PAL) and for the Baltag-Moss-Solecki logic (BMS). This semantics is grounded on a construction on algebras which generalizes epistemic updates on relational models. This generalized semantics leads to a (semantically motivated) axiomatic definition of the counterparts of PAL and BMS on a weaker than classical propositional base;

(b) display-style, cut-free sequent calculi for both the intuitionistic and the classical versions of PAL and BMS. Besides being very transparent, these calculi are sound and complete with respect to both the algebraic and the relational semantics of PAL, and enjoy a weaker form of display property, which is still enough to prove the cut-admissibility. These calculi are also modular, so just by modifying the structural rules, they are generalizable both to different Dynamic Logics (Epistemic, Deontic, etc.) and to different propositional bases (Linear, Relevant, etc.). We will focus in particular on the weak display property and discuss the generalizations to other dynamic logics.