lo.logic - cut elimination

Cut elimination is indispensable for studying fragments of arithmetic. Consider for example the classical Parsons–Mints–Takeuti theorem:

Theorem If $ISigma_1vdashforall x,exists y,phi(x,y)$ with $phiinSigma^0_1$, then there exists a primitive recursive function $f$ such that $mathrm{PRA}vdashforall x,phi(x,f(x))$.

The proof goes roughly as follows. We formulate $Sigma^0_1$-induction as a sequent rule
$$frac{Gamma,phi(x)longrightarrowphi(x+1),Delta}{Gamma,phi(0)longrightarrowphi(t),Delta},$$
include axioms of Q as extra initial sequents, and apply cut elimination to a proof of the sequent $longrightarrowexists y,phi(x,y)$ so that the only remaining cut formulas appear as principal formulas in the induction rule or in some axiom of Q. Since other rules have the subformula property, all formulas in the proof are now $Sigma^0_1$, and we can prove by induction on the length of the derivation that existential quantifiers in the succedent are (provably in PRA) witnessed by a primitive recursive function given witnesses to existential quantifiers in the antecedent.

Now, why did we need to eliminate cuts here? Because even if the sequent $philongrightarrowpsi$ consists of formulas of low complexity (here: $Sigma^0_1$), we could have derived it by a cut
$$frac{philongrightarrowchiqquadchilongrightarrowpsi}{philongrightarrowpsi}$$
where $chi$ is an arbitrarily complex formula, and then the witnessing argument above breaks.

To give an example from a completely different area: cut elimination is often used to prove decidability of (usually propositional) non-classical logics. If you show that the logic has a complete calculus enjoying cut elimination and therefore subformula property, there are only finitely many possible sequents that can appear in a proof of a given formula. One can thus systematically list all possible proofs, either producing a proof of the formula, or showing that it is unprovable. Again, cut elimination is needed here to have a bound on the complexity of formulas appearing in the proof.

Sigfpe wrote above in his answer that cut elimination makes proofs more complex, but that’s not actually true: cut elimination makes proofs longer, but more elementary, it eliminates complex concepts (formulas) from the proof. The latter is often useful, and it is the primary reason why so much time and energy is devoted to cut elimination in proof theory. In most applications of cut elimination one does not really care about having no cuts in the proof, but about having control of which formulas can appear in the proof.