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 (abbreviations). P = NP iff Extended Frege has polynomial proofs for all tautologies? (Open)

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

Proof complexity and P vs NP: If some system has polynomial proofs for all tautologies → coNP = NP.

Symbols.

Symbol	Unicode	Name	Meaning
\|π\|	—	Length	Proof size
P	—	System	Proof system
Res	—	Resolution	Resolution system
CP	—	Cutting planes	Linear system
F	—	Frege	Standard propositional
EF	—	Extended Frege	With extensions
⊢_P	—	Provable	Derivable in P

Metatheory. Resolution lower bounds: exponential (Haken). Cutting planes: exponential for some (Pudlák). Frege: no superpolynomial lower bounds known. Extended Frege: even harder. Proof complexity hierarchy not fully understood.

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

Limitations. Lower bounds hard to prove. Frege lower bounds major open problem. Gap between systems and practice. Highly technical. Limited direct applications. Theoretical focus.