On the Complexity of the Propositional Calculus

Summary

Abstract

We show that research into the complexity of propositional proofs is related to various problems in other branches of mathematics. A nondeterministic procedure for a coNP-complete can be viewed as a propositional proof system. We survey several proof systems which were proposed for problems in integer linear programming, algebra and graph theory. Then we consider a general method of proving lower bounds on the lengths of propositional proofs which is based on a property of some systems called effective interpolation. This means that the circuit complexity of interpolating boolean functions f(x) of an implication ø(x, y) →φ(x, z) can be bounded by a polynomial in the length of a proof of the implication. We shall prove such a theorem for a system for integer linear programming proposed by Lovász and Schrijver [34] and show a relation between a problem on the complexity of linear programming and a problem of proving lower bounds on the lengths of proofs in this system. We shall consider the lengths of proofs in nonclassical logics, in particular monotone and intuitionistic logics, and, in a similar way, show a relation to the complexity of sorting networks.