Inception Display Calculi

TL;DR

This paper extends display calculi for LE-logics to include a broader class of axioms, enabling uniform rule generation and encompassing all Sahlqvist axioms.

Contribution

It introduces an extended framework for display calculi that handles inductive axioms beyond analytic inductive, covering a wider range of logics.

Findings

Extended display calculus framework includes non-analytic inductive axioms.

Unified correspondence and ALBA algorithm generate analytic rules for new axiomatic extensions.

Framework captures the entire acyclic substructural hierarchy.

Abstract

Display calculi were introduced by Nuel Belnap in `Display logic' (1982) as a natural extension of Gentzen's sequent calculi, as a uniform and modular framework capable of encompassing broad classes of logics. In `Unified correspondence as a proof-theoretic tool', the properly displayable (D)LE-logics are syntactically characterized as the logics axiomatised by analytic inductive axioms for any signature. We extend the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class of axioms covers and properly extends all Sahlqvist axioms. The present framework takes inspiration from Schroeder-Heister's calculus of Higher-Level Rules and captures the whole acyclic fragment of the substructural hierarchy when generalized to arbitrary signatures. We apply unified correspondence theory and the algorithm ALBA to uniformly generate analytic rules for the aforementioned axiomatic extensions.