7/29/26
Disabling rules you do not wish to use
Several of the exercises in the book consist of proving a rule using only other rules. Steven Stegeman in his book proves each of the individual rules of inference from the others so, for example, he derives Modus Ponens P, P ⊃ Q ∴ Q from the other rules (i.e. he writes P, P ⊃ Q as premises and Q as the conclusion and derives the conclusion from the premises, but without using the rule of MP). He does this for all his rules. No doubt some Users will want to do the same. Of course, they can do this already on an 'honor system', by just avoiding any rule they are not supposed to use. But the software does provide support. The software can disable any menu item the User does not want to use, for example, MP. If a proof is 'started' from an empty selection, the proof panel is clear but the Menu bar is available and in particular the Rules menu is there and will open. It will look like this:
Mouse clicks on any Rules menu item toggles it on and off. A single mouse click on MP, for example, will disable it and the entire menu will look like this:
Once a real derivation is started, and the proof panel has contents, the configuration remains frozen. Then, clearing the proof panel allows further changes to the configuration (back to default or whatever is desired). Of course, if, for example, the Rules Menu item for MP is disabled, the User has no way of using MP in a derivation.