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.