On the complexity of the disjunction property in intuitionistic and modal logics
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino · ACM Transactions on Computational Logic · 2005
In this article we study the complexity of disjunction property for intuitionistic logic, the modal logicsS4,S4.1, Grzegorczyk logic, Gödel-Löb logic, and the intuitionistic counterpart of the modal logicK. ForS4we even prove the feasible interpolation theorem and we provide a lower bound for the length of proofs. The techniques we use do not require proving structural properties of the calculi in hand, such as the cut-elimination theorem or the normalization theorem. This is a key point of our approach, since it allows us to treat logics for which only Hilbert-style characterizations are known.