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 Ai. 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. (c) 2007 Elsevier B.V. All rights reserved.