Proof Complexity

Origin. Cook and Reckhow initiated proof complexity (1979). Studies lengths of proofs in various systems. Lower bounds: some tautologies require long proofs. Connects to computational complexity (P vs NP). Propositional proof systems as central objects.

Models. Measuring proof difficulty. Propositional proof system: polynomial-time checkable proofs of tautologies. Proof length: bits to write proof. Lower bound: tautology requires exponential proof in system P. Separations: system P stronger than Q.

Formalism.

Proof system: P: Σ* → Tautologies (surjective, poly-time computable) P(π) = φ means π is P-proof of φ.

Proof length: |π|_P = length of proof π in system P. Complexity: min{|π| : P(π) = φ}.

Hierarchy of systems: Weaker → Stronger (simulating with polynomial overhead): Resolution < Cutting Planes < Frege < Extended Frege

Resolution: Clauses, resolution rule: (A ∨ x) ∧ (B ∨ ¬x) → A ∨ B Exponential lower bounds known (pigeonhole principle).

Frege systems: Standard propositional proof systems. No exponential lower bounds known.

Extended Frege: Frege + extension rule: new variables abbreviating formulas. If Extended Frege were polynomially bounded then NP = coNP — the relevant collapse is NP = coNP, not P = NP, and only that one direction is known. Whether EF is polynomially bounded is open.

Cutting planes: Integer linear inequalities. Stronger than resolution for some formulas.

Proof complexity and NP vs coNP: Cook–Reckhow: NP = coNP iff some propositional proof system is polynomially bounded. The programme is therefore to prove superpolynomial lower bounds for stronger and stronger systems; proving them for all systems would separate NP from coNP, and hence P from NP.

Symbols.

Symbol	Unicode	Name	Meaning
π	U+03C0	Pi / Proof	A candidate proof, the string a system decodes
\|π\|	—	Length	Size of the proof π, in bits
φ	U+03C6	Phi / Formula	The tautology being proved
Σ	U+03A3	Sigma / Alphabet	Σ*, the strings that may encode proofs
*	U+002A	Asterisk / Kleene star	Σ*, all finite strings over the alphabet
→	U+2192	Rightwards arrow / Function arrow	P : Σ* → Tautologies
∨	U+2228	Logical or	Clause formation in the resolution rule
∧	U+2227	Logical and	Joins the two premises of a resolution step
¬	U+00AC	Not sign	The complementary literal resolved upon
<	U+003C	Less-than sign	Strict simulation order between proof systems
⊢_P	—	Provable in P	Derivability in the proof system P
P	—	Proof system	Polynomial-time computable surjection onto TAUT
Res	—	Resolution	Clause-based refutation system
CP	—	Cutting planes	Integer linear inequality system
F	—	Frege	Standard textbook propositional calculus
EF	—	Extended Frege	Frege plus the extension rule for new variables

Metatheory. Cook and Reckhow (1979) defined a propositional proof system as a polynomial-time computable surjection from strings onto the tautologies, and proved the theorem the field is organized around: NP = coNP if and only if some proof system is polynomially bounded. Superpolynomial lower bounds for successively stronger systems are therefore a programme for separating NP from coNP. Haken (1985) gave the first, exponential for the pigeonhole principle in resolution; Ben-Sasson and Wigderson (2001) unified the resolution bounds through a size-width tradeoff. Pudlák (1997) obtained exponential lower bounds for cutting planes by monotone interpolation, and Ajtai (1988), sharpened by Krajíček, Pudlák, and Woods and independently by Pitassi, Beame, and Impagliazzo, showed the pigeonhole principle requires exponential-size bounded-depth Frege proofs. The programme stops there: no superpolynomial lower bound is known for Frege, let alone Extended Frege. Resolution is also the system SAT solvers implicitly search — Pipatsrisawat and Darwiche (2011) showed CDCL with restarts polynomially simulates it — so the lower bounds are statements about solvers.

Applies to. SAT solving (resolution basis). Computational complexity. Automated theorem proving. Foundations of mathematics. Algorithm analysis. Cryptography (proof of work).

Limitations. The method reaches only weak systems. Superpolynomial bounds exist for resolution, cutting planes, and bounded-depth Frege, and stop precisely at Frege, where the best known bound is quadratic; a superpolynomial bound for Extended Frege would be a step toward separating NP from coNP and is not expected to be easier than that problem. Bounds do not transfer upward, and the simulation order is only partially known — many pairs of systems are incomparable, so each system requires its own technique rather than an application of a general one. What the measure captures is proof size, not the cost of finding a proof, so a polynomial upper bound need not describe any algorithm: Atserias and Müller (2020) showed that automating resolution is NP-hard, meaning short resolution proofs can exist while no efficient procedure locates them. The whole framework is propositional, so first-order and arithmetic proof lengths need the separate machinery of bounded arithmetic.