I'd like to better understand the role of the contraction rule in Gentzen's $\mathsf{LK}$. I would like to have an example of a derivable sequent that is no longer derivable if the contraction rule is replaced by "derive $\Sigma, A \wedge B \vdash \Delta$ from $\Sigma, A ,B \vdash \Delta$ and "derive $\Sigma \vdash A \vee B , \Delta$ from $\Sigma \vdash A, B, \Delta$". I am particularly interested in the formulation of $\mathsf{LK}$ without the cut rule.
eliminating contraction
Andre Kornell
- 974
- 4
- 15