#### 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.