3.5 Use of tautologies

Rather as in the above explanation about the S.I. rule, there is another method for avoiding unnecessary work: the appeal to a problem's being obviously solvable. For example, when one is learning the rules and tactics of first-order logic, it is irritating to have to work with the zero-order rules rather than concentrating on the first-order difficulties, so one would like to dismiss the zero-order sub-problems as trivial. One may of course be able to quote an earlier result, but one's library of theorems is usually deficient. One therefore often just uses the rule or tactic labelled Tautology, and relies on the theorem-provers built into MacLogic to check that this is justified.

To use the Tautology rule in Check mode, use the ... button to get at it. The provability (in zero-order logic) of your conclusion (in the Formula box) from the premisses cited is checked by the theorem-prover. The assumptions quoted should be all the assumptions on which any of the premisses depends. See below for details of what the theorem-prover can do: it is good at problems in various first-order logics, but not allowing the rules for equality or modal operators.

To use the tactic for Tautology in Construct mode, use the ... button to get at it. You must then enter the precise sequent being appealed to in a dialog box. (The box may be pre-filled with a suggestion.) This is checked by the theorem-prover for being provable in zero-order logic: if it is accepted, its assumptions are taken, one by one, as new goals in the current context, and its conclusion added to the current context for proving the old goal. Derivations built in this way are transformed to proofs using the Tautology rule described above.