# 13.5 Proof Length and Complexity

## 13.5 Proof Length and Complexity

Proof theory can ask not only whether a formula is provable, but also how hard it is to prove. This leads to the study of proof length and proof complexity.

A formal proof is a finite object, so it has a size. We may count the number of lines, the number of inference steps, the total number of symbols, or the size of the proof tree.

For a formula $A$, we may ask:

$$
\text{What is the length of the shortest proof of } A?
$$

This question turns proof theory into a quantitative subject.

### Measuring Proof Length

Different proof systems measure proof size in slightly different ways.

| Measure      | Meaning                                |
| ------------ | -------------------------------------- |
| Line count   | number of formulas in a sequence proof |
| Step count   | number of inference rule applications  |
| Symbol count | total number of symbols in the proof   |
| Tree size    | number of nodes in a proof tree        |
| DAG size     | size after sharing repeated subproofs  |

For example, a proof written as a tree may duplicate the same subproof several times. If repeated subproofs are shared, the same proof may be represented as a directed acyclic graph, or DAG, and become much smaller.

So proof length depends partly on representation.

### Shortest Proofs

Let $S$ be a proof system. The proof length of $A$ in $S$ may be written:

$$
\ell_S(A)
$$

This means the length of the shortest proof of $A$ in system $S$.

If $A$ has no proof in $S$, then $\ell_S(A)$ is undefined or treated as infinite.

The main question is how $\ell_S(A)$ grows as the formulas become larger.

Some formulas have short proofs. Others may be true but require very long proofs in a given system.

### Comparing Proof Systems

Two proof systems may prove the same formulas but differ greatly in proof length.

Suppose systems $S_1$ and $S_2$ prove the same theorems. It may still happen that some formulas have short proofs in $S_1$ and only very long proofs in $S_2$.

We say that $S_1$ **polynomially simulates** $S_2$ if every proof in $S_2$ can be translated into a proof in $S_1$ with only polynomial growth in size.

Informally:

$$
\ell_{S_1}(A) \leq p(\ell_{S_2}(A))
$$

for some polynomial $p$.

If no such efficient translation exists, then one proof system may be genuinely stronger in proof efficiency.

### Proof Complexity

Proof complexity studies the size of proofs, especially for propositional tautologies.

A propositional formula $A$ is a tautology if:

$$
\models A
$$

A sound and complete proof system can prove every tautology:

$$
\models A \quad \Longrightarrow \quad \vdash A
$$

But completeness only says that a proof exists. It does not say the proof is short.

Proof complexity asks whether certain tautologies require large proofs in a given system.

### Resolution

One important proof system in proof complexity is **resolution**.

Resolution works with clauses. A clause is a disjunction of literals, such as:

$$
p \lor ¬q \lor r
$$

The resolution rule is:

$$
\frac{A \lor p \qquad B \lor ¬p}{A \lor B}
$$

The idea is that one clause says $A$ is true unless $p$ fails, and the other says $B$ is true unless $p$ holds. Resolving eliminates $p$.

Resolution is central because it is closely related to SAT solving.

To prove that a CNF formula is unsatisfiable, resolution derives the empty clause:

$$
\Box
$$

The empty clause represents contradiction.

### Example of Resolution

Suppose we have the clauses:

$$
p \lor q
$$

and:

$$
¬p \lor r
$$

Resolving on $p$ gives:

$$
q \lor r
$$

because the complementary literals $p$ and $¬p$ are removed.

Another example:

$$
p
$$

and:

$$
¬p
$$

resolve to:

$$
\Box
$$

This means the clauses are jointly inconsistent.

### Lower Bounds

A lower bound says that every proof of a certain kind must be large.

For example, one may show that a family of tautologies requires resolution proofs of exponential size.

The general form is:

$$
\ell_S(A_n) \geq 2^{cn}
$$

for some constant $c>0$.

This means that as $n$ grows, proofs in system $S$ become exponentially long.

Lower bounds are difficult but important. They show that some proof systems cannot efficiently prove certain valid formulas.

### Connection with Complexity Theory

Proof complexity is closely related to computational complexity.

A proof system for propositional tautologies can be viewed as a certificate system. If a tautology has a short proof, then the proof can be checked efficiently.

This connects to the class $\mathrm{NP}$, where solutions can be verified efficiently.

The complement problem, propositional tautology, is related to $\mathrm{coNP}$. A major open question is whether every tautology has a short proof in some reasonable proof system.

This is closely connected to:

$$
\mathrm{NP} \stackrel{?}{=} \mathrm{coNP}
$$

If every tautology had polynomial-size proofs in a suitable proof system, that would imply a major collapse in complexity theory.

### Automated Reasoning

Proof length matters in practice.

Automated theorem provers and SAT solvers do not merely need proofs to exist. They need proofs that can be found and checked within reasonable time and memory.

A formula may be valid, but if every proof is enormous, automated reasoning may fail in practice.

This is why proof systems are compared not only by correctness but also by proof efficiency.

### Compression and Sharing

Large proofs often contain repeated subarguments. Sharing can compress them.

A tree proof may repeat a lemma many times. A DAG proof can store the lemma once and reuse it.

This reflects ordinary mathematics. We prove a lemma once, then cite it repeatedly.

Formal proof systems can model this using derived rules, lemmas, abbreviations, and proof terms.

Compression changes proof size, so any serious study of proof length must specify the representation carefully.

### Why This Matters

Proof length measures the cost of reasoning.

Soundness tells us that proofs are reliable. Completeness tells us that all valid formulas are provable. Proof complexity asks whether those proofs are feasible.

This adds a third dimension to formal logic:

$$
\text{truth}
\qquad
\text{provability}
\qquad
\text{proof size}
$$

A mature theory of proof must account for all three.