zbMATH — the first resource for mathematics

The complexity of propositional proofs. (English) Zbl 0845.03025
“The classical propositional calculus has an undeserved reputation among logicians as being essentially trivial. I hope to convince the reader that it presents some of the most challenging and interesting problems in modern logic.” So begins this survey article, whose main theme is to compare which proof system can(not) simulate which others in polynomial time. The systems considered include Frege systems, Gentzen systems, tableaux, resolutions, and truth tables, and the author provides a full page chart showing their relations. Not merely citing results, he reproduces proofs and thus presents “some of the techniques that have proved successful in deriving lower bounds on the complexity of proofs”. An instance is \(k\)-valuation that is employed by Pudlák et al. in giving exponential lower bounds on proofs of the pigeonhole principle in bounded-depth Frege systems. One area left out is bounded arithmetic and its connection with complexity theory. (The reader is referred to J. Krajíček’s recent monograph [Bounded arithmetic, propositional logic, and complexity theory (1995; Zbl 0835.03025)].) With a number of open problems and references to an extensive bibliography, this is a survey worthy of its name. Whether the kinds of problems referred to are “most challenging and interesting…in modern logic” is a decision for the reader to make.

03F20 Complexity of proofs
03B05 Classical propositional logic
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
Full Text: DOI Link