Unified correspondence and proof theory for strict implication

Abstract

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.