Question

What is the cut rule? I don't mean the rule itself but an explanation of what it means and why are proof theorists always trying to eliminate it? Why is a cut-free system more special than one with cut?

Answer 1

Suppose I have a proof of B starting from assumption A. And a proof of C starting from assumption B. Then the cut rule says I can deduce C from assumption A.

But I didn't need the cut rule. If I was able to deduce B from A I could simply "inline" the proof of B from A directly into the proof of C from B to get a proof of C from A.

So the cut rule is redundant. That's a good reason to eliminate it.

But eliminating it comes at a price. The proofs become more complex. Here's a paper that quantifies just how much. So it's a hard rule to give up.

Answer 2

Another reason is proof search. Consider that a rule like $\frac{\Gamma \vdash p \quad \Gamma \vdash q}{\Gamma \vdash p \wedge q}$ can be read as "to find a proof for $\Gamma \vdash p \wedge q$, it suffices to find proofs for $\Gamma \vdash p$ and $\Gamma \vdash q$". Since $p$ and $q$ are subformulas of $p \wedge q$, finding proofs for them is simpler.

For cut rule you get "to find a proof for $\Gamma \vdash p$, it suffices to find proofs for $\Gamma \vdash q$ and $\Gamma, q \vdash p$ for some formula $q$". The problem is, how can you choose which $q$ to use? It needn't be a subformula of $p$ or any formula from $\Gamma$. This makes proof search intractable.

Answer 3

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

Theorem If $I\Sigma_1\vdash\forall x\,\exists y\,\phi(x,y)$ with $\phi\in\Sigma^0_1$, then there exists a primitive recursive function $f$ such that $\mathrm{PRA}\vdash\forall 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)\longrightarrow\phi(x+1),\Delta}{\Gamma,\phi(0)\longrightarrow\phi(t),\Delta},$$ include axioms of Q as extra initial sequents, and apply cut elimination to a proof of the sequent $\longrightarrow\exists 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 $\phi\longrightarrow\psi$ consists of formulas of low complexity (here: $\Sigma^0_1$), we could have derived it by a cut $$\frac{\phi\longrightarrow\chi\qquad\chi\longrightarrow\psi}{\phi\longrightarrow\psi}$$ 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.

Answer 4

To elaborate on Alexey's answer, for "usual" sequent calculi, the rules other than cut "build structure" in the proof: the left rules build up structure of the assumptions from smaller formulae, and the right rules build up structure in the conclusion(s). Thus cut-free proofs have a kind of recursive structure, and one can reason about the class of cut-free proofs to prove things like consistency, completeness, &c.

However, the cut-free proofs don't admit all of the usual ways we reason in logic; modus ponens being an example that needs cut to be modelled. So to move from the class of inferences that we want to work within to the class of inferences in which we can best reason about, we need the cut-elimination theorem. If we can't find a cut-elimination theorem, that is a sign that the "logic" is broken.