Why Proof Complexity?

Introduction

I recently read the introductory lecture to COMS E6998 Proof Complexity and Applications (Spring’25) and thought I’d share this beautifully tantilizing result.

Proof complexity studies the resources required to prove logical statements in different proof systems. Its central questions resemble those of ordinary computational complexity:

• How long must a proof be?
• How difficult is it to find one?
• How do different proof systems compare?

The result I want to explain here connects the first of these questions directly to $\mathrm{NP}$ versus $\mathrm{coNP}$:

Equivalently, proving that no polynomially bounded proof system exists would separate $\mathrm{NP}$ from $\mathrm{coNP}$, and therefore also prove

See this lab page for information on P vs. NP.

The remarkable part is that, once the definitions are in place, the proof is almost immediate.

Boolean formulas and tautologies

We will work with propositional formulas built from Boolean variables and the usual connectives

A truth assignment assigns each variable either $0$ or $1$. A formula is satisfiable if it evaluates to true under at least one assignment, and it is a tautology if it evaluates to true under every assignment.

We write

The use of binary strings here is not especially profound. We simply choose some reasonable way to encode formulas as finite strings so that they can be given as input to an algorithm.

A formula $\varphi$ is a tautology precisely when its negation $\neg\varphi$ is unsatisfiable. Consequently, proving tautologies and refuting unsatisfiable formulas are two versions of the same task.

A very quick reminder about NP and coNP

A language $L$ belongs to $\mathrm{NP}$ when membership in $L$ has efficiently verifiable certificates. Formally, there must be a polynomial-time algorithm $V$ and a polynomial $q$ such that

The string $p$ is the certificate. It is not the verification algorithm; it is the object given to the verification algorithm.

For example, a satisfying assignment is a short certificate that a Boolean formula is satisfiable. Given the assignment, we can simply evaluate the formula.

The class $\mathrm{coNP}$ consists of the complements of languages in $\mathrm{NP}$:

Since $\mathrm{SAT}$ is $\mathrm{NP}$-complete, its complement $\mathrm{UNSAT}$ is $\mathrm{coNP}$-complete. Equivalently, $\mathrm{TAUT}$ is $\mathrm{coNP}$-complete.

Informally:

• $\mathrm{NP}$ contains problems whose yes-instances have short, efficiently checkable certificates;
• $\mathrm{coNP}$ contains problems whose no-instances have short, efficiently checkable certificates.

The question $\mathrm{NP}=\mathrm{coNP}$ therefore asks, among other things, whether every tautology has some polynomial-size certificate of being a tautology.

This is where proof complexity enters.

Propositional proof systems

Ordinarily, a proof system is described by axioms and inference rules. For complexity theory, Cook and Reckhow gave a wonderfully general definition that forgets the internal syntax and remembers only what matters computationally: proofs must be efficiently checkable.

A propositional proof system is a polynomial-time algorithm

such that, for every encoded formula $x$,

Here:

• $x$ is the encoding of the formula;
• $p$ is the encoding of a purported proof;
• $V$ is the proof verifier.

The two directions of the equivalence encode the familiar logical requirements.

Soundness

If the verifier accepts a proof, then the formula really is a tautology:

A sound proof system never proves a false statement.

Completeness

Every tautology has some proof that the verifier accepts:

A complete proof system can prove every statement it is supposed to prove.

Thus soundness and completeness together say

Resolution, Frege systems and many algebraic proof systems can all be encoded in this form.

Efficient verification does not mean short proofs

The verifier $V$ must run in time polynomial in the lengths of both its inputs:

This does not imply that verification takes polynomial time in $|x|$ alone. The proof $p$ might itself be exponentially long.

For example, there is a trivial truth-table proof system. To prove that a formula in $n$ variables is a tautology, the proof can contain its entire truth table. The verifier checks every row and confirms that the formula always evaluates to true.

This proof is efficiently checkable relative to its own length, but it may have $2^n$ rows. The system is sound and complete, but its proofs need not be short.

This leads to the central definition.

Polynomially bounded proof systems

A propositional proof system $V$ is polynomially bounded if there exists a polynomial $q$ such that every tautology $x$ has an accepted proof of length at most $q(|x|)$:

The distinction is essential:

• every propositional proof system has efficiently verifiable proofs;
• a polynomially bounded proof system would give every tautology a polynomial-length proof.

We can now state the result that makes this definition so exciting.

The Cook—Reckhow theorem

Theorem. There exists a polynomially bounded propositional proof system if and only if

$$\mathrm{NP}=\mathrm{coNP}.$$

Equivalently,

Despite its significance, the proof is remarkably short.

Polynomially bounded proofs imply $\mathrm{NP}=\mathrm{coNP}$

Suppose that a polynomially bounded propositional proof system $V$ exists.

Then membership in $\mathrm{TAUT}$ has polynomial-size certificates: on input $x$, guess a polynomial-length proof $p$ and run $V(x,p)$.

Therefore,

But $\mathrm{TAUT}$ is $\mathrm{coNP}$-complete. Hence every problem in $\mathrm{coNP}$ can be reduced to a problem in $\mathrm{NP}$, and so

Taking complements gives the reverse inclusion:

Consequently,

$\mathrm{NP}=\mathrm{coNP}$ implies polynomially bounded proofs

Conversely, suppose

We already know that

Under our assumption, this means

By the certificate characterization of $\mathrm{NP}$, there must therefore exist a polynomial-time verifier $V$ and a polynomial $q$ such that

But this is exactly a polynomially bounded propositional proof system.

Therefore,

This proves both directions.

Why this would separate P from NP

The class $\mathrm P$ is closed under complementation. Therefore, if

then

Taking the contrapositive gives

Combining this with the Cook—Reckhow theorem, we obtain

What remains far beyond us is a lower bound against every polynomial-time verifiable proof system at once.

Very cool.