A lower bound for intuitionistic logic (Q876385)

The paper proves unconditional exponential lower bounds on the number of proof lines in the Frege system for intuitionistic propositional logic, which solves an outstanding open problem in propositional proof complexity. The main tool is a variant of feasible monotone interpolation for the intuitionistic Frege system, which is proved using a translation to the modal logic K, and a modification of a monotone interpolation theorem for K given earlier by the author [``Lower bounds for modal logics'', J. Symb. Log. (2007), to appear]. This monotone interpolation is then applied to give two examples of hard intuitionistic tautologies. It is also shown that these tautologies have polynomial-size classical Frege proofs.