One important property of many logical systems is that a certain
rule, called the *Cut* rule, is admissible, in the sense
that its addition to the system does not extend the range of theorems
that can be proved, but just allows the proofs to be shorter or
simpler. Gentzen's *Hauptsatz, Main theorem* or *Cut
elimination theorem,* says just this about (e.g.) certain sequent
calculus formulations of classical or intuitionistic logic.

In the search for a proof of a sequent, one usually relies
on just looking at the formulae involved, breaking them up syntactically:
the tactic corresponding to the *Cut* rule, however, requires
one to have insight by picking an appropriate formula, the *Cut
formula,* out of thin air. This rule's presence makes the automatic
search for proofs rather hard - so it is better if it is not a
necessary part of the formal system. MacLogic is therefore designed
to be used without a *Cut* rule.

However, no convenient formulation of the modal logic S5 is
known to be cut-free. It is therefore necessary to be able to
use the *Cut* rule (or, rather, its corresponding tactic),
when working in S5. There is therefore a tactic for *Cut*,
accessible via the **...** radio
button from the **Tactic choice** dialog.

Technically, the *Cut* rule is a rule of the sequent calculus.
Its use translates into the use of a natural deduction rule which
we call "Substitution", since it corresponds to the
substitution of a proof of the cut-formula A
in place of an assumption of A. The
notion of a *Cut* can be defined for natural deduction, and
some then talk about *Cut-elimination;* we prefer to talk
of *proof normalisation.*