Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics

TL;DR

This paper develops a general framework for sequent calculi in intuitionistic modal logics, proving feasible admissibility of Visser's rules in many systems and establishing limitations for constructive calculi.

Contribution

It introduces a family of constructive sequent calculi for intuitionistic modal logics and proves feasible admissibility of Visser's rules in these systems.

Findings

Feasible admissibility of Visser's rules in several intuitionistic modal calculi.

Constructive sequent calculi exist for many intuitionistic modal logics.

Limitations on the existence of constructive calculi for certain logics.

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 $\mathsf{CK}$, $\mathsf{IK}$ 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 $\mathsf{IPC}$ has a constructive sequent calculus.