[Proof Complexity] Preprint

[Raheleh Jalali]

Dear Colleagues,

A new preprint "Universal Proof Theory: Feasible Admissibility in
Intuitionistic Modal Logics" is available on arxiv:

https://arxiv.org/abs/2209.08911

Any comments, suggestions and corrections are most welcome.

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 CK, 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 IPC has a constructive
sequent calculus.

Best regards,
Raheleh.