3.6 Cut rule

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.