On Friday, December 12th, we will have a LIRa session with Alessandra Palmigiano.
Everyone is cordially invited!
Speaker: Alessandra Palmigiano (Delft University of Technology)
(joint work with Giuseppe Greco, Minghui Ma, Apostolos Tzimoulis and Zhiguang Zhao)
Date and Time: Friday, December 12, 2014, 14:30-16:00
Venue: Science Park 107, Room F1.15
Title: Unified Correspondence as a Proof-Theoretic Tool
Abstract: This talk focuses on the formal connections which have recently been highlighted between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap.
These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterisation of the modal axioms (which he calls primitive formulas) which can be effectively transformed into `good’ structural rules of display calculi. In this context, a rule is `good’ if adding it to a display calculus preserves Belnap’s cut-elimination theorem.
In recent years, correspondence theory has been uniformly extended from classical modal logic to diverse families of nonclassical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi. This generalisation has given rise to a theory called unified correspondence, the most important technical tool of which is the algorithm ALBA.
We put ALBA to work to obtain a generalisation of Kracht’s transformation procedure from axioms into `good’ rules. This generalisation concerns more than one aspect. Firstly, we define primitive formulas/inequalities in any logic the algebraic semantics of which is based on distributive lattices with operators. Secondly, in the context of each such logic, we significantly generalise the class of primitive formulas/inequalities, and we apply ALBA to obtain an effective transformation procedure for each member of this class.
Time permitting, we will discuss the connections between the ALBA-aided transformation procedure and other similar procedures existing in the literature, developed for instance by Negri, Ciabattoni and other authors.