On the Lengths of Proofs in the Propositional Calculus (Preliminary Version)
One of the most important open questions in the field of computational complexity is the question of whether there is a polynomial time decision procedure for the classical propositional calculus.
 The purpose of the present paper is to study a question related to the complexity of decision procedures for the propositional calculus; namely, the complexity of proof systems for the propositional calculus. The fundamental issue here is whether there exists any proof system, and a polynomial p(n) such that every valid formula has a proof of length not exceeding p(n), where n is the length of the formula. Theorem 1 below helps establish the importance of this question. For the purposes of this theorem, we give the following definitions.