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)