Cut Rule

The cut rule is a Structural Rule in most Sequent Calculi that essentially lets you introduce Let Bindings.

The most general form of the cut rule that works even in Substructural Logics is

Γ⊢Δ1,A,Δ2Θ1,A,Θ2⊢ΨΘ1,Γ,Θ2⊢Δ1,Ψ,Θ2provesΓsubscriptΔ1𝐴subscriptΔ2subscriptΘ1𝐴subscriptΘ2provesΨprovessubscriptΘ1ΓsubscriptΘ2subscriptΔ1ΨsubscriptΘ2\par\frac{\Gamma\vdash\Delta_{1},A,\Delta_{2}\qquad\Theta_{1},A,\Theta_{2}% \vdash\Psi}{\Theta_{1},\Gamma,\Theta_{2}\vdash\Delta_{1},\Psi,\Theta_{2}}

Cut and Structural Rules

In the presence of structural rules (in particular, Exchange), we can simplify the rule to

Γ⊢Δ,AΘ,A⊢ΨΓ,Θ⊢Δ,ΨprovesΓΔ𝐴Θ𝐴provesΨprovesΓΘΔΨ\par\frac{\Gamma\vdash\Delta,A\qquad\Theta,A\vdash\Psi}{\Gamma,\Theta\vdash% \Delta,\Psi}

Moreover, in a system based off of Natural Deduction, then we can simplify further to:

Γ⊢AΔ,A⊢BΓ,Δ⊢BprovesΓ𝐴Δ𝐴proves𝐵provesΓΔ𝐵\par\frac{\Gamma\vdash A\qquad\Delta,A\vdash B}{\Gamma,\Delta\vdash B}

Moreover, in the presence of a Weakening Rule, we can further reduce the natural deduction rule to

Γ⊢AΓ,A⊢BΓ⊢BprovesΓ𝐴Γ𝐴proves𝐵provesΓ𝐵\par\frac{\Gamma\vdash A\qquad\Gamma,A\vdash B}{\Gamma\vdash B}

When working with dependent types, this rule is literally the rule for Let Bindings

Γ⊢e1:AΓ,x:A⊢e2:BΓ⊢𝗅𝖾𝗍⁢x=e1⁢𝗂𝗇⁢e2:B⁢[e1/x]provesΓsubscript𝑒1:𝐴Γ𝑥:𝐴provessubscript𝑒2:𝐵provesΓ𝗅𝖾𝗍𝑥subscript𝑒1𝗂𝗇subscript𝑒2:𝐵delimited-[]subscript𝑒1𝑥\par\frac{\Gamma\vdash e_{1}:A\qquad\Gamma,x:A\vdash e_{2}:B}{\Gamma\vdash% \mathsf{let}\;x=e_{1}\;\mathsf{in}\;e_{2}:B[e_{1}/x]}