# 3.5 Cut Elimination

The cut rule allows a proof to introduce an intermediate formula and then eliminate it, and while this rule can shorten derivations by reusing previously proved statements, it is not essential for the power of the sequent calculus, and its elimination reveals a deeper structural property of proofs.

### The Cut Rule

The cut rule has the form:
$$
\frac{\Gamma \vdash \Delta, A \qquad \Gamma, A \vdash \Delta}{\Gamma \vdash \Delta}
$$

This rule expresses that if a formula $A$ can be derived from $\Gamma$, and if $A$ together with $\Gamma$ allows one to derive the desired conclusion, then $A$ can be removed as an intermediate step.

The rule resembles substitution in algebra, where an expression is introduced and then replaced, and it captures a common pattern in informal reasoning where intermediate results are used temporarily.

### Role of Cut

The cut rule is powerful because it allows proofs to be modular, meaning that one can prove a lemma and then use it later without repeating its proof, and this often leads to shorter and more manageable derivations.

However, the presence of the cut rule also obscures the structure of proofs, because it introduces formulas that may not be directly related to the final conclusion.

### Theorem 3.13 (Cut Elimination)

Every proof in the sequent calculus that uses the cut rule can be transformed into a proof of the same sequent that does not use the cut rule.

This theorem shows that the cut rule is admissible, meaning that it does not increase the set of provable sequents, even though it may shorten proofs.

### Proof Idea

The proof proceeds by induction on the structure of derivations and by systematically removing instances of the cut rule.

Given a proof that contains a cut, one analyzes the position of the cut relative to the logical rules and replaces it with a sequence of simpler cuts or eliminates it entirely.

At each step, the complexity of the cut formula or the height of the proof is reduced, so that the process eventually terminates.

This transformation is intricate because it must consider all possible ways in which the cut formula interacts with the inference rules, but the key idea is that cuts can be pushed upward in the proof tree until they disappear.

### Consequences

Cut elimination has several important consequences for logic and proof theory.

One consequence is the subformula property, which states that in a cut free proof, every formula that appears is a subformula of the formulas in the final sequent.

This property shows that proofs do not introduce unrelated formulas and that their complexity is controlled by the structure of the original statement.

Another consequence is consistency, because if a contradiction were derivable, then there would be a cut free proof of the empty sequent, and analyzing such proofs shows that no contradiction can be derived in a consistent system.

Cut elimination also provides a form of normalization, since it transforms proofs into a canonical form that avoids unnecessary intermediate steps.

### Example 3.14

Suppose we have a proof that uses the cut rule with an intermediate formula $A$.

The proof first derives:
$$
\Gamma \vdash \Delta, A
$$

and then uses $A$ to derive:
$$
\Gamma, A \vdash \Delta
$$

The cut rule combines these into:
$$
\Gamma \vdash \Delta
$$

Cut elimination replaces this pattern by a proof that derives $\Gamma \vdash \Delta$ directly, without introducing $A$ as an intermediate formula.

The resulting proof may be longer, but it will have a simpler structure in which every step is directly related to the final conclusion.

### Lemma 3.15 (Admissibility of Cut)

If a sequent $\Gamma \vdash \Delta$ has a proof using the cut rule, then it also has a proof that does not use the cut rule.

Proof

This follows from the cut elimination theorem, since the theorem provides a method for transforming any proof into a cut free proof while preserving the final sequent.

### Relation to Other Systems

Cut elimination in the sequent calculus corresponds to normalization in natural deduction, where proofs are simplified by removing detours.

In both cases, the goal is to eliminate unnecessary intermediate steps and to reveal the essential logical structure of the proof.

These parallels show that different proof systems share deep structural properties, even though their surface forms may differ.

### Complexity Considerations

Although cut elimination simplifies the structure of proofs, it may increase their size, sometimes dramatically, because eliminating a cut can require duplicating parts of the proof.

This trade off between simplicity and size is an important aspect of proof theory, and it has implications for automated reasoning and computational complexity.

### Significance

Cut elimination is one of the central results of proof theory, because it shows that logical reasoning can be carried out without relying on intermediate lemmas, and it provides a foundation for many further developments, including consistency proofs, normalization results, and connections with computation.

By studying cut elimination, one gains a deeper understanding of the internal structure of proofs and the principles that govern formal deduction.