A lower bound for intuitionistic logic

We give an exponential lower bound on the number of proof-lines in intuitionistic propositional logic, I L , axiomatised in the usual Frege-style fashion; i.e., we give an example of I L -tautologies A 1 , A 2 , … s.t. every I L -proof of A i must have a number of proof-lines exponential in terms of the size of A i . We show that the results do not apply to the system of classical logic and we obtain an exponential speed-up between classical and intuitionistic logic.