On the complexity of the disjunction property in intuitionistic and modal logics

n this article we study the complexity of disjunction property for intuitionistic logic, the modal logics S4, S4.1, Grzegorczyk logic, Godel-Lob logic, and the intuitionistic counterpart of the modal logic K. For S4 we 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