Proof Complexity

Suppose you want to convince someone that a logic formula has no satisfying assignment — that it's a tautology in negation, or equivalently that its negation is unsatisfiable. You write down a proof. How long does that proof have to be?

For simple cases the answer is short. But for carefully chosen formulas, every proof in a given system must be exponentially long — no matter how clever the strategy. That is the central discovery of proof complexity: some true statements are hard to certify, not just hard to discover.

The field was born in 1979 when Stephen Cook and Robert Reckhow formalized the question. They showed that proving NP ≠ co-NP is equivalent to showing that no proof system can always produce short proofs of tautologies. So proof complexity is not just about logic — it sits at the heart of the deepest open problem in computer science.

Resolution is the simplest proof system for unsatisfiability. Its one rule: from clause $(A \lor x)$ and clause $(B \lor \neg x)$ derive $(A \lor B)$ — the resolvent. A refutation is a resolution proof that derives the empty clause $\bot$, showing the formula is unsatisfiable.

<p class="hint">
  {{hint}}
</p>
<div class="controls">
  <label for="formula-select">{{formula_label}}</label>
  <select id="formula-select">
    <option value="0">{{opt_php21}}</option>
    <option value="1">{{opt_php32}}</option>
    <option value="2">{{opt_2cnf}}</option>
  </select>
</div>
<div class="proof-area">
  <div class="clause-list" id="clause-list"></div>
</div>
<div class="step-info" id="step-info">{{press_next}}</div>
<div class="btns">
  <button id="btn-prev" type="button" class="ghost" disabled>{{btn_prev}}</button>
  <button id="btn-next" type="button">{{btn_next}}</button>
  <button id="btn-all" type="button" class="ghost">{{btn_all}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<div class="stats" id="stats"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .6rem; line-height: 1.45; }
.controls { display: flex; align-items: center; gap: .5rem; margin-bottom: .6rem; flex-wrap: wrap; }
label { font-weight: 600; font-size: .88rem; }
select { font-size: .88rem; padding: .3rem .5rem; border: 1px solid #adb1b8; border-radius: 6px;
         background: #f5f7fa; cursor: pointer; }
.proof-area { border: 1px solid #cdd9e3; border-radius: 8px; background: #f8fafc;
              padding: .5rem .7rem; min-height: 120px; max-height: 220px; overflow-y: auto;
              margin-bottom: .5rem; }
.clause-list { display: flex; flex-direction: column; gap: 3px; }
.clause-row { display: flex; align-items: baseline; gap: .5rem; font-size: .85rem;
              padding: 2px 0; }
.clause-row.axiom  { color: #1d3557; }
.clause-row.derived { color: #0a7d33; }
.clause-row.empty-clause { color: #c92f3c; font-weight: 700; }
.clause-row.new { animation: fadeIn .3s ease; }
@keyframes fadeIn { from { opacity: 0; transform: translateY(-4px); } to { opacity: 1; } }
.row-num { color: #888; font-size: .75rem; min-width: 24px; text-align: right; flex-shrink: 0; }
.clause-text { font-family: ui-monospace, monospace; }
.justification { color: #777; font-size: .75rem; font-style: italic; }
.step-info { font-size: .9rem; font-weight: 600; margin: .4rem 0; min-height: 1.4em;
             color: #1d3557; }
.btns { display: flex; gap: .4rem; flex-wrap: wrap; margin-bottom: .4rem; }
button { font: 600 13px system-ui, sans-serif; padding: .4rem .8rem;
         border: 1px solid #1d3557; background: #1d3557; color: #fff;
         border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .4; cursor: not-allowed; }
.stats { font-size: .82rem; color: #555; min-height: 1.2em; }

// Code not found

Watch how the number of steps (lines in the proof) grows as the formula changes. PHP(2,1) needs 5 steps, PHP(3,2) needs 21 — and for PHP(n+1, n) in general, resolution needs at least $2^{\Omega(n)}$ steps (proven by Haken, 1985). The 2-CNF clash formula collapses to just 7 steps because it has a small proof in resolution too — but for harder formulas, no shortcut exists inside weak systems.

Proof complexity ranks proof systems by the lengths they require:

• Resolution is the weakest widely studied system. It operates on clauses (disjunctions of literals) and derives new clauses by the single resolution rule. Armin Haken (1985) proved that the pigeonhole principle — "you can't fit $n+1$ pigeons into $n$ holes without sharing" — requires exponentially many resolution steps. This was the field's first superpolynomial lower bound.
• Ben-Sasson and Wigderson (2001) gave an elegant reformulation: proof length in resolution is controlled by clause space and clause width. Their Width–Size theorem connects these three measures and gives a clean recipe for proving lower bounds.
• Frege systems (sequent calculus, natural deduction) are far more powerful: they can manipulate arbitrary formulas, not just clauses. No superpolynomial lower bound is known for any Frege system. Proving one would separate NP from co-NP.
• Extended Frege adds the power to introduce abbreviations (extension variables). It is conjectured to be polynomially equivalent to circuit-based proof systems. Its complexity is entirely open.
• The Cook–Reckhow theorem (1979): a propositional proof system $P$ can always produce short (polynomial-length) proofs of all tautologies if and only if the language of tautologies is in NP — which happens exactly when NP = co-NP. So finding a proof system with short proofs for everything would resolve a major open problem.

The landscape: resolution is weak and well understood; Frege is strong and mysterious; everything in between is an active frontier.

Proof complexity is not just abstract logic — it shapes the tools that power modern computer science:

• SAT solvers and CDCL: modern SAT solvers use Conflict-Driven Clause Learning, which implicitly builds resolution proofs as they search. The strength of CDCL is captured by a fragment of resolution called pool resolution, and understanding proof length explains why some instances are hard for solvers.
• Automated theorem proving: every theorem prover must choose a proof calculus. Proof complexity tells us which calculi can be efficiently complete and which will inevitably bloat.
• Cryptography: some proof-of-work schemes require hard instances where short proofs of satisfiability exist but are hard to find. Proof complexity provides the theoretical grounding.
• Circuit lower bounds: there is a deep connection between proof complexity and circuit complexity. Proving lower bounds for Frege systems would likely require breakthroughs in understanding the power of $\mathsf{TC}^0$ circuits.
• The NP vs co-NP question: as Cook and Reckhow showed, a proof system with polynomial-size proofs for all tautologies would collapse NP and co-NP — one of the most important open questions alongside P vs NP.

Proof complexity teaches a sobering lesson: correctness and certifiability are different things. A formula can be unsatisfiable — provably, absolutely false — yet every proof of that fact in a given system must be exponentially long. Resolution is provably weak; Frege systems remain a mystery after decades of effort.

The question of whether there is a proof system that is always efficient is equivalent to NP = co-NP, which is itself implied by P = NP. So the shortest path to the P vs NP Millennium Prize may run straight through proof complexity — through the unavoidable length of proofs we write every day.