Unified Correspondence and Proof Theory for Strict Implication

TL;DR

This paper develops a unified correspondence and proof theory framework for strict implication logics, extending them conservatively to Lambek Calculi and creating analytic, cut-free sequent calculi.

Contribution

It specializes the unified correspondence theory to strict implication logics and constructs analytic, cut-free sequent calculi for BDFNL and its extensions.

Findings

Many strict implication sequents can be transformed into analytic rules.

A conservative extension of strict implication logics to Lambek Calculi is established.

Cut-free sequent calculi are developed for BDFNL and its extensions.

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 $\msf{ALBA}$. Gentzen-style cut-free sequent calculi for BDFNL and its extensions with analytic rules which are transformed from strict implication sequents, are developed.