3.4 Sequent Introduction

In practice, few proofs are done just by means of the primitive rules of inference corresponding to the logical constants: one appeals to previously proved results. MacLogic provides a mechanism for making such an appeal. It is limited to the use of results from zero-order logic.

For example, suppose you are using classical logic, and have already shown that formulae o the form AÎÒA are provable therein: and then you have a problem of deriving C from the two implications BÁC, ÒBÁC. You can proceed to use the primitive rules, but it is more natural to quote the result BÎÒB, and then use Î-Elimination. This step of quoting a(n instance of) a previously proved result is called "Sequent Introduction" (S.I.).

S.I. can only be used if some theorems are in the database, having been proved already, either in the same session (and kept) or in a previous session (and loaded). If you try to use it when no theorems are in the database, you have the opportunity to load some. The mode of use varies according to which of Check mode and Construct mode you are in.

In Check mode, S.I. is accessed via the ... radio button on the Next Line dialog box. Before using this button you may wish to look at the Theorems window to see which theorem you are going to use. There is then a dialog, asking you to choose a theorem. The premisses cited by number in the Premiss Nos. field must be, in order, the (substitution instances of the) assumptions in the theorem being used: the formula in the Formula field must be the appropriate instance of the consequent of this theorem. The assumptions listed in your Assumption Nos. box must be all the assumptions needed in all the premisses to which you refer.

In Construct mode, suppose your current problem is to prove C from a list F of formulae, and that a problem GD has already been solved and kept as a theorem. Then you can construct a substitution instance G'D' of this theorem, and then try and solve the new sub-problems of trying to show, from F, each in turn of the assumptions in G', and then, adding D' to F, of trying to show C. In many cases, the theorem is chosen to make most of these steps trivial, and one might think the tactic could be more simple to use: but for completeness, this rather general form is required, alas. The tactic for S.I. is accessed via the ... button.

Use of the S.I. rule thus gives you the right to use, very much as if it were an extra rule of inference, any previously proved zero-order result. (Not all correct rules can be represented in this way: for example, those involving discharge of assumptions cannot be so represented.)