17 April 2012, Logic Tea, Sumit Sourabh

Sahlqvist correspondence theory is one of the most important and useful results of classical modal logic. It gives a syntactic identification of a class of modal formulas whose associated normal modal logics are strongly complete with respect to elementary (i.e. first-order definable) classes of frames. Every Sahlqvist formula is both canonical and corresponds to some elementary frame condition which can be effectively obtained from the formula. Recently this class has significantly been extended to inductive and complex formulas.

In this talk, I will give an introduction to the algebraic account of Sahlqvist correspondence theory using the duality between Kripke frames and complete atomic boolean algebras with operators. Using the algebraic approach, Sahlqvist and inductive formulas can be equivalently defined in terms of order theoretic conditions on the algebraic interpretation of the logical connectives. These definitions hold in a much wider setting than classical modal logic, and I will discuss them in the setting of intuitionistic modal logic as a concrete example. Finally, I'll illustrate using ackermann lemma based algorithm, an alternative way to compute the first order correspondents of intuitionistic modal formulas.

The Logic Tea homepage can be found at http://www.illc.uva.nl/logic_tea/ For more information, please contact Umberto Grandi (u.grandi at uva.nl), Tong Wang (tongwang01 at gmail.com), or Matthijs Westera (M.Westera at uva.nl).