Post History

What is a “first-order substructural logic that has a cut-free sequent calculus”?

Is a first order sub-structural logic a synonym for a fragment of first order logic? Ie just some restriction on syntactic allowances, so we know we have a theory whose sentences are a subset of the theory of FOL?

I read that in sequent calculus, a cut rule is a rather trivial sounding rule that if you have A proves B, and B proves C, you can write A proves C.

Why would eliminating the cut rule be significant? Even without the cut rule, if A proves B, and B proves C, shouldn’t it be possible to show a direct proof of C from A, without the “cut rule”, which sounds like a mere convenience method? What are examples of theorems that cannot be proven without the cut rule?