Admissibility of Visser's rules in intuitionistic modal logics

Raheleh Jalali^1
1 Czech Academy of Sciences

We study the connection between the form of the primitive rules of a proof system and the rules the system admits. We introduce a general and syntactically defined family of sequent-style calculi over the modal language and its fragments as an approximate formalization for “constructively acceptable” systems. We call these calculi constructive and show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser’s rules. This means that there exists a polynomial-time algorithm that, given a proof of the premise of a Visser’s rule, provides a proof for its conclusion.

As a positive application, we establish the feasible admissibility of Visser’s rules in several sequent calculi for intuitionistic modal logics, including $\sf CK$, $\sf IK$, and their extensions by the modal axioms $\sf T$, $\sf B$, $\sf 4$, $\sf 5$, and the axioms for bounded width and depth, and 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 $\sf IPC$ has a constructive sequent calculus.

(Download the slides.)

 Overview