The relative efficiency of propositional proof systems

TLDR

The known upper bound for the shortest proof length of a propositional tautology is exponential in the tautology length, regardless of the proof system. The study aims to determine whether any propositional proof system can bound the shortest proof length of a tautology polynomially in the tautology length. The authors employ extended Frege systems that use iterative abbreviations to prevent exponential growth of formula length in proofs. Relative to other systems, standard Hilbert/Frege and natural deduction systems are polynomially equivalent in minimum proof length, and extended Frege systems can keep each proof line length linearly bounded by the formula length.

Abstract

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results. In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.