Formal Proof Systems - Main Theorem

TheoremGentzen's Cut Elimination Theorem (Hauptsatz)

If a sequent $\Gamma \Rightarrow \Delta$ is provable in the sequent calculus LK (possibly using the cut rule), then it is provable in LK without using the cut rule.

Moreover, if the original proof has height $h$ and maximum cut formula complexity $c$ , then the cut-free proof has height bounded by a function of $h$ and $c$ .

The cut rule in sequent calculus is:

\frac{\Gamma \Rightarrow \Delta, \phi \quad \phi, \Gamma' \Rightarrow \Delta'}{\Gamma, \Gamma' \Rightarrow \Delta, \Delta'} \text{(cut)}

This rule corresponds to using a "lemma": from proving $\phi$ and using $\phi$ to prove the conclusion, we derive the conclusion directly. Cut elimination shows that such lemmas are always eliminable—we can prove the conclusion directly without intermediate steps.

Significance: Cut elimination is one of the most important results in proof theory for several reasons:

Subformula Property: In a cut-free proof, every formula is a subformula of the conclusion or assumptions. This drastically constrains the search space for proofs.
Consistency: The unprovability of the empty sequent $\Rightarrow$ can be shown directly by induction on cut-free proofs, providing a consistency proof for first-order logic.
Decidability: For propositional logic and some fragments of first-order logic, the subformula property yields decision procedures.
Computational Interpretation: Cut elimination corresponds to normalization in typed lambda calculus and to program optimization (removing unnecessary intermediate computations).

ExampleApplying Cut Elimination

Consider proving transitivity of implication: $(p \to q), (q \to r) \vdash p \to r$ .

With cut: Prove $\Rightarrow p \to q$ and $\Rightarrow q \to r$ separately, use $q$ as a cut formula.

Cut-free: Build a direct proof that doesn't explicitly mention $q$ as an intermediate lemma:

\frac{ \frac{ \frac{\text{axiom}}{p \Rightarrow p} }{p \to q, p \Rightarrow q} \to\text{-L} \quad \frac{ \frac{\text{axiom}}{r \Rightarrow r} }{q \to r, q \Rightarrow r} \to\text{-L} }{(p \to q), (q \to r), p \Rightarrow r} \to\text{-L}

The cut-free proof is more complex but has the subformula property.

Remark

The cost of cut elimination is that proofs can become exponentially longer. There exist sequents with short proofs using cut but whose shortest cut-free proof is exponentially larger. This trade-off between proof length and structural properties is fundamental in proof complexity.

TheoremHerbrand's Theorem

A universal first-order sentence $\forall x_1 \cdots \forall x_n \, \phi$ (where $\phi$ is quantifier-free) is valid if and only if there exist terms $t_1^1, \ldots, t_1^n; \ldots; t_k^1, \ldots, t_k^n$ such that the propositional formula:

\phi[x_1/t_1^1, \ldots, x_n/t_1^n] \lor \cdots \lor \phi[x_1/t_k^1, \ldots, x_n/t_k^n]

is a propositional tautology.

Herbrand's theorem reduces first-order validity to propositional validity by systematically instantiating universal quantifiers. The theorem is the foundation of many automated theorem-proving techniques.

Remark

Together, cut elimination and Herbrand's theorem provide deep insights into the structure of first-order proofs. They show that first-order reasoning can be reduced to:

Systematic search for instantiation terms (Herbrand's theorem)
Structural manipulation without lemmas (cut elimination)

These results bridge syntactic proof theory and semantic model theory, revealing why first-order logic is so computationally well-behaved despite being undecidable.