# Example of Cut in Natural Deduction and how to remove it

I have heard of the Cut in Sequent Calculus before, but it seems that it exists for Natural Deduction as well. Could you please provide a proof in Natural Deduction (propositional logic) that illustrates the use of a Cut?

Additionally, there is a theorem in Sequent Calculus that transforms proofs that use Cut into proofs that don't use it. Is there an equivalent theorem for Cuts in Natural Deduction? Could you provide the corresponding proof (of the one you have given for the above) which now does not make use of the Cut?

I have tried to find information on the Cut for Natural Deduction but it seems that most literature talks about it with regards to Sequent Calculus. Could this be because the Cut for Natural Deduction have a different name? Links to resources greatly appreciated but not necessary! Thank you very much for your responses in advance!

Edit: this question is more about simple examples that illustrate concepts involved, rather than the formal proofs of those concepts (and establishing the correct terminology regarding these concepts)

As you can see in Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 18, in Natural Deduction we have the substitution rule, which is a "derived rule" :

In natural deduction, if two derivations $$\Gamma \vdash A$$ and $$A, \Delta \vdash C$$ are given, we can join them together into a derivation $$\Gamma, \Delta \vdash C$$, through a substitution :

$${ \Gamma \vdash A \quad A, \Delta \vdash C \over \Gamma, \Delta \vdash C } \, \text{(Subst)}$$

The sequent calculus rule corresponding to this is cut :

$${ \Gamma \implies A \quad A, \Delta \implies C \over \Gamma, \Delta \implies C } \, \text{(Cut)}$$

Often cut is explained as follows: We break down the derivation of $$C$$ from some assumptions into "lemmas," intermediate steps that are easier to prove and that are chained together in the way shown by the cut rule.