How Many Times do We Need an Assumption to Prove a Tautology in Minimal Logic? Examples on the Compression Power of Classical Reasoning

In this article we present a class of formulas ϕn,0≤n, that need at least 2n assumption occurrences of other formula βn in any normal proof in Natural Deduction for purely implicational minimal propositional logic (M→). In classical implicational logic, each ϕn have normal proofs using at most one assumption occurrence. As a consequence, normal proofs of ϕn have exponential lower bound in M→ and linear lower bound in its classical version. In fact, 2n is the lower-bound for cut-free Sequent proofs too. The existence of this class of formulas have strong influence in designing automatic proof-procedures based in such systems. It is discussed proof-theoretically how tautologies in purely implicational classical logic can be proved by polynomially sized derivations when their minimal counterpart is exponentially sized.