Skip to main content
3 of 3
added 1 character in body

eliminating contraction

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.