A lower bound for intuitionistic logic

We give an exponential lower bound on number of proof-lines in intuitionistic propositional logic, IL, axiomatised in the usual Frege-style fashion; i.e., we give an example of IL-tautologies A1, A2, . . . s.t. every IL-proof of Ai 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.

• Type: Journal
• Year: 2007
• Where: APAL
• Authors: Pavel Hrubes
• Keywords: APAL 2007, Intuitionistic Propositional Logic, Lower Bound, Usual Frege-style Fashion