2.2 Constructing a Proof

Once you are acquainted with the Check mode of MacLogic, the next matter to tackle is Construct mode: this mode allows you actually to build a proof (more easily), and not simply to verify that a proof is correct. It works in what is called a root-first fashion; that is to say, it doesn't work forward from the assumptions to the conclusion in the way that we have done so far when working in Check mode, but requires you to consider the problem as a whole and use some more strategic thinking. The proof is a tree, and you construct first the data at the root of the tree, the point from which it grows, working towards the leaves. This way of working could be mirrored in a non-implemented variant of Check mode where one could work both down from the assumptions and up from the conclusion---in general, tactics for elimination rules correspond to rules working down from the assumptions, and tactics for introduction rules are used to work up from the conclusion.

Because of this difference in approach between Check and Construct mode, you will also notice a considerable difference in the style in which your work appears on your screen. To emphasize this difference, we put the record of what you do into a window called Derivation: when all the work is complete, this is transformed in a mechanical fashion (see section 4.3 for details) into a proof in the traditional style. You start with a problem consisting of (optional) assumptions leading to a conclusion, and working on this problem produces a series of sub-problems as you go along, which you must solve one by one.

Suppose we are set the task of solving the problem PÁ(Q&R)(PÁQ)&(PÁR). As you have done before, double-click on the MacLogic icon (unless MacLogic is already running), and select the item Constructing in the Options menu. Select Dialog... from the Problem menu, and fill in the Problem Entry box as follows:

Click on Ok, and you will find that a window called Derivation, another called Current Problem, and a dialog box called Tactic choice will appear. Derivation will display all the problems and sub-problems which you are to solve, and Tactic choice has a selection of buttons for tactics which you use to solve the current problem. (For a more complete description of what all these buttons do, see section 5.4.) The screen will look like this:

Note that the antecedent formula PÁQ&R appears without parentheses: there are some conventions (see section 5.2 below) about when parentheses can be omitted. Some small spaces are included (in this case on each side of the 'Á' symbol, telling you discreetly which operator is the principal operator of the formula.

Note also that you will always be told, in the Current Problem window, what the current problem (the sub-problem that you are working on) is. It is just a restatement of information in the Derivation window, in a more familiar layout style. Also, note the indentation of the current line, in the Derivation window: it will always show what level of sub-problem you are at. This should become clearer as you work through the proof.

Your first step is to choose a tactic. You will notice that there is much less typing involved here than in the Check mode. This is one of the reasons why Construct mode is far better for constructing proofs; also, you needn't worry about having explicitly to make assumptions; because of the way in which Construct mode works, they are made automatically for you, when necessary.

The natural place to start in this problem is with an &-Introduction step --- because it is an introduction rule, it will work backwards on the conclusion. The current problem displayed is to derive a conjunctive formula (PÁQ)&(PÁR) from PÁQ&R. So the appropriate choice is to use the tactic for &I to obtain it. The goal formula (PÁQ)&(PÁR) will be split up into the two conjuncts, and you will then have two major sub-problems to solve. Each of the sub-problems will have the same fact-list. We call the list of formulae (so far there is only one) to the left of the arrow, the fact-list, for it consists of "facts" on the basis of which we are trying to achieve the goal. The "facts" consist of assumptions plus what we derive from assumptions in elimination rules on our way to achieving the goal. We also call this list the antecedent of the problem and th goal the succedent.

The &I button is selected as shown, and confirmed by pressing Ok. You now have two sub-problems, with the same antecedent, arising from the two conjuncts, and we are set to work on the first, viz   PÁ(Q&R)PÁQ. (You will tackle the second, viz  PÁ(Q&R)PÁR, only after you have solved the first.). To solve the first, use an ÁI step:

This will bring the formula P back from the goal, PÁQ, into the antecedent as an assumption:

Notice that we are still working on the first major sub-problem, and that our second major sub-problem remains to be solved ahead. Now, if we examine the formulae in the antecedent, we can see that an ÁE step is in order. By clicking on ÁE and then on Ok, we get the following screen:

The black box indicates that you have just solved a trivial sub-problem: it is trivial because the formula, P, to be derived appears as one of the facts (actually, as one of the assumptions).

The next sub-problem consists in deriving Q from Q&R. For the first time we have a formula in our fact-list which is not an assumption, but is derived from the assumption PÁ(Q&R) by ÁE. This sub-problem is easily solved, using an &-Elimination step to split up the conjunction Q&R: this will leave us with Q both in the antecedent (on the left of the arrow) and as a goal (on the right): this sub-problem is now trivial.

We have now solved one of the two major sub-problems that we started out with (as indicated by the indentation on the left). The next sub-problem is almost of the same form, and is solved using the same steps of ÁI, Á E and &E. Try this now.

Once you have successfully completed these steps, you will be rewarded with a 'Well done!' message, as in the Check mode. You will then be asked if you wish to see the derivation transformed into a natural deduction proof:

SelectYes and the derivation will be mechanically transformed into a Lemmon-style natural deduction proof, displayed in the Proof window:

You can now go back and examine the strategy you used in the Derivation window, comparing it with the proof. As in Check mode, printing may be done using the Print visible windows... item from the File menu. You can print this proof now, or keep it in the file of proofs for printing later, as before.