Unified correspondence and proof theory for strict implication

Minghui Ma, Zhiguang Zhao

Research output: Contribution to journalArticlepeer-review

12 Citations (Scopus)


The unified correspondence theory for distributive lattice expansion logics (DLE-logics) is specialized to strict implication logics. As a consequence of a general semantic consevativity result, a wide range of strict implication logics can be conservatively extended to Lambek Calculi over the bounded distributive full non-associative Lambek calculus (BDFNL). Many strict implication sequents can be transformed into analytic rules employing one of the main tools of unified correspondence theory, namely (a suitably modified version of) the Ackermann lemma based algorithm ALBA. Gentzen-style cut-free sequent calculi for BDFNL and its extensions with analytic rules, which are transformed from strict implication sequents, are developed.
Original languageEnglish
JournalJournal of Logic and Computation
Publication statusPublished - 2016


  • Regular modal logics
  • Unified correspondence
  • proof theory
  • sequent calculus
  • strict implication


Dive into the research topics of 'Unified correspondence and proof theory for strict implication'. Together they form a unique fingerprint.

Cite this