Post History

The structural rules of sequent calculus are:

- Weakening: $$\dfrac{Γ ⊢ C}{Γ, A ⊢ C}$$

- Contraction: $$\dfrac{Γ, A, A ⊢ C}{Γ, A ⊢ C}$$

- Exchange: $$\dfrac{Γ, A, B ⊢ C}{Γ, B, A ⊢ C}$$

Substructural logics omit at least one of these rules.

As for cut elimination, part of the point is that it _is_ a proof that the cut rule is merely a 'convenience.' That requires actual proof, not just 'seeming.' Also, the cut rule is a bit more complicated than you've stated. It is more like:

- Cut: $$\dfrac{Γ,A,Γ' ⊢ C \qquad Δ ⊢ A}{Γ,Δ,Γ' ⊢ C}$$

So, for instance, let's also consider substructural logics. How certain are you, exactly, that cutting like that in the _middle_ of a context never expands into a cut-free proof that makes use of the "exchange" rule to reorder the premises in the context?

If the consequent were instead $$Γ,Γ',Δ ⊢ C$$ then we'd pretty easily be able to derive exchange, and cut could not be eliminated without the exchange rule. So that is a sort of contrived example of why a cut-like rule would not be able to be eliminated. There are other 'bad' ways to design sequent rules that prevent eliminating cut as well. So proving cut elimination is sort of a check that you have designed your proof rules in a good way, so that cut is "just" a convenience.

_However_, do also note that in the presence of contraction, cut-free proofs can easily be exponentially larger than the original. So it can be a _very_ significant convenience. One _could_ even argue that it is _not_ realistic to imagine that cut can be eliminated for this reason, because some cut-free proofs would be too large to write down. But, this is usually not a concern in the idealized setting used for analyzing logics.