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

In this paper we study the complexity of disjunction property for Intuitionistic Logic, the modal logics S3, 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 to prove 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.