Example of Cut in Natural Deduction and how to remove it

Question

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)

Answer 1

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.

But see also [page 172] :

[Substitution] rule resembles cut, but is different in nature: Closure under substitution just states that substitution through the putting together of derivations produces a correct derivation. This is seen clearly from the proof of admissibility of substitution.

In natural deduction in sequent calculus style, there are no principal formulas in the antecedent, and therefore the substitution formula in the right premiss also appears in at least some premiss of the rule concluding the right premiss. Substitution is permuted up until the right premiss is an assumption.

Elimination of substitution is very different from the elimination of cut.