On lengths of proofs in non-classical logics

We give proofs of the effective monotone interpolation property for the system of modal logic K , and others, and the system I L of intuitionistic propositional logic. Hence we obtain exponential lower bounds on the number of proof-lines in those systems. The main results have been given in [P. Hrubeš, Lower bounds for modal logics, Journal of Symbolic Logic 72 (3) (2007) 941–958; P. Hrubeš, A lower bound for intuitionistic logic, Annals of Pure and Applied Logic 146 (2007) 72–90]; here, we give considerably simplified proofs, as well as some generalisations.