The cut proof rule first proves an new formula P on one branch and then assumes P on another branch. This can be useful to first prove a lemma P and then assume it for the rest of the proof. Just like an Edit, cuts are also useful to transform formulas: edit("x>5",1).

Cuts with unprovable assumptions can also be useful to hypothetically study whether an extra assumption would help or to get more pleasant counterexamples.

Learning resources