Algorithmic correspondence for intuitionistic modal mu-calculus, Part 2

4 pages•Published: July 28, 2014

Willem Conradie, Yves Fomatati, Alessandra Palmigiano and Sumit Sourabh

Abstract

Sahlqvist-style correspondence results remain a perennial theme and an active topic of research within modal logic. Recently there has been interest in extending classical results in this area to the modal mu-calculus. We show how the `calculus of correspondence' and the ALBA algorithm (Conradie and Palmigiano, 2012) can be extended to the intuitionistic mu-calculus, and be used to derive FO+LFP frame correspondents for formulas of that logic. We define the class of recursive mu-inequalities, which we compare it with related classes in the literature including the Sahlqvist mu-formulas of van Benthem, Bezhanishvili and Hodkinson. We show that the ALBA algorithm succeeds in reducing every recursive mu-inequality, and hence that every recursive mu-inequality has a frame correspondent in FO+LFP.

Keyphrases: correspondence theory, heyting algebras, intuitionistic logic, modal logic, modal mu calculus, sahlvist theory

In: Nikolaos Galatos, Alexander Kurz and Constantine Tsinakis (editors). TACL 2013. Sixth International Conference on Topology, Algebra and Categories in Logic, vol 25, pages 57-60.

Links:	https://easychair.org/publications/paper/86Gl
	https://doi.org/10.29007/r68t

BibTeX entry

@inproceedings{TACL2013:Algorithmic_correspondence_intuitionistic_modal,
  author    = {Willem Conradie and Yves Fomatati and Alessandra Palmigiano and Sumit Sourabh},
  title     = {Algorithmic correspondence for intuitionistic modal mu-calculus, Part 2},
  booktitle = {TACL 2013. Sixth International Conference on Topology, Algebra and Categories in Logic},
  editor    = {Nikolaos Galatos and Alexander Kurz and Constantine Tsinakis},
  series    = {EPiC Series in Computing},
  volume    = {25},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/86Gl},
  doi       = {10.29007/r68t},
  pages     = {57-60},
  year      = {2014}}

Download PDF Open PDF in browser