Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics

MaRDI QIDQ6411191zbMATH OpenFDO

Authors Amirhossein Akbar Tabatabai, Raheleh Jalali

Publication date 19 September 2022

Abstract: In this paper, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi emph{constructive}, we show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser's rules, i.e., there is a polynomial time algorithm that reads a proof of the premise of a Visser's rule and provides a proof for its conclusion. As a positive application, we show the feasible admissibility of Visser's rules in several sequent calculi for intuitionistic modal logics, including $mathsfCK$, $mathsfIK$ and their extensions by the modal axioms $T$, $B$, $4$, $5$, the modal axioms of bounded width and depth and the propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser's rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than $mathsfIPC$ has a constructive sequent calculus.

This page was built for publication: Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6411191)