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?
1 answer
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.
0 comment threads
0 comment threads