3.5 Cut Elimination
The cut rule allows a proof to introduce an intermediate formula and then eliminate it, and while this rule can shorten derivations by reusing previously proved statements, it is not essential for the power of the sequent calculus, and its elimination reveals a deeper structural property of proofs. The Cut Rule The cut rule has the form: $$ \frac{\Gamma \vdash \Delta, A \qquad \Gamma, A \vdash \Delta}{\Gamma \vdash \Delta} $$...