Logic seminar

Feasible disjunction property for intuitionistic modal logics

In this talk, we present a uniform method to prove feasible disjunction property (DP) for various intuitionistic modal logics. More specifically, we prove that if the rules in a sequent calculus for a modal intuitionistic logic have a special form, then the sequent calculus enjoys feasible DP. Our method is essentially an adaptation of the method used by Hrubes in his lower bound proof for the intuitionistic Frege system. As a consequence, we uniformly prove that the sequent calculi for intuitionistic logic, the intuitionistic version of several modal logics such as K, T, K4, S4, S5, their Fisher-Servi versions, propositional lax logic, and many others have feasible DP. Our method also provides a way to prove negative results: we show that any intermediate modal logic without DP does not have a calculus of the given form. This talk is based on a joint work with Amir Tabatabi.