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