MacLogic is designed to help you both to check proofs and to
construct them. There are two modes in MacLogic: *Check*
mode, which allows you to check proofs for errors, and *Construct*
mode, which helps you to build the proofs in a more organised
manner. This section will take you through a sample session with
the *Check* mode of MacLogic. You will meet *Construct*
mode in section 2.2 below.

Suppose you are set the task of solving the problem PÁ(QÁR)(PÁQ)Á(PÁR). Open the MacLogic application by double clicking on the MacLogic icon. While it is loading, a small cursor containing 0s and 1s is shown. After a little while, the menu bar

should appear, followed by a modal dialog box such as:

You must respond to this dialog box before doing anything else.
Just click on **Ok**, and respond to the next dialog box in
the same way. Note that the latter is telling you that you can
start work by using the **Problem** menu, and gives instructions
on how to interrupt MacLogic if it gets stuck thinking about whether
it can solve your problem by itself.

By clicking on the **Options** menu header, you can see
whether *Check* mode is on by verifying that **Checking**
is ticked. If it isn't, select it by dragging down till **Checking**
is selected, then release the mouse button:

The **Logic** menu allows you to choose a particular logic.
(MacLogic defaults to classical logic. You can explore the other
logics later.) Note that in the **Options** menu, you can set
the modes to save your proof to a file, to a window, or to keep
the problem just solved as a theorem. Make sure all three of these
are ticked, so you can see later what they do, that **Classical**
is ticked in the **Logic** menu, and that all other items in
that menu are unticked.

You can now start your proof by going into the **Problem**
menu and selecting **Dialog... **: this is one of the
ways of entering a problem. The other ways are to select a problem
from the front window, to choose one from a problem library, and
**Test run**, that tries all the problems in the library, automatically.

Once you have selected **Dialog...**, a modeless dialog
box will appear looking like this:

This is the box into which you will type your problem. Note
that it is prefilled with a very simple problem, just to show
where things go: you will try something a bit harder! You can
use the mouse or the tab button to move between the **Assumptions**
field and the **Goal** field. If there is more than one assumption,
they should be separated by commas, as in A,
B.

First, type PÁ(QÁR).
(Note that Á is, at least
on British keyboards, typed as Shift Option Y.) Press the **Tab**
key --- that takes you to the **Goal** field: now type (PÁQ)Á(PÁR). Once
you have typed in the problem, the **Problem Entry** dialog
box should look like this:

At this point, click on** Ok**. If you have not typed in
a well-formed formula, you will be informed by an error message
and must then correct your entries. You are now ready to begin
the proof: the screen displays a **Proof** window, where your
proof will be displayed, and a **Next Line** dialog box, into
which you enter instructions for forming the next proof line.
The screen will look roughly like this:

Your first step is to put in any assumptions you might have.
For the present problem, the only assumption is PÁ(QÁR),
and so you fill in various parts of the **Next Line** dialog
box like this:

Remember you may use **Tab** to move from one field to another
(you can also use the mouse, if you wish). Notice that because
no premisses are needed for an assumption, the **Premiss Nos**.
field is left blank. Once your **Next Line** dialog box has
been completed in this fashion, click on **Ok**. The **Proof**
window will change to look like this:

Your assumption line appears in the **Proof** window in
a standard proof style (that of Lemmon), provided you have typed
everything in correctly. If you haven't, an appropriate error
message will appear and you must correct the fault. Notice that
if your line is correct and it appears in the **Proof** window,
the **Next Line** box is cleared, ready for the next line.
Now you know the basics of entering assumptions. You will need
two more assumptions, PÁQ
and P, for this proof --- put them
in now, one by one.

The next step after these assumptions is a use of the **Á-Elimination** rule. It is abbreviated
as **ÁE** in the **Next
Line** box: all these buttons represent the rules which you
can use. You will be learning all of them later: so far you should
know **Ass**, **ÁE **and
**ÁI** (**Á-Introduction**).
The **ÁE** step will look
like this:

You can see that you must now enter references to two premisses,
as the **Á-Elimination**
step uses two previous lines as premisses. The premisses here
are lines 2 and 3, and the new line depends on the assumptions
made on lines 2 and 3. [Note that the premisses must be cited
in order, with the major premiss, i.e. the line containing the
formula with the **'Á'**
being "eliminated", first. Here this premiss is line
2. You can enter the assumption numbers, however, in any order.]
Now click on **Ok**.

You can work through this proof line by line, entering them
as you have been shown. You need only use **Ass**, **ÁE** and **ÁI**.
The proof will continue to appear line by line in the **Proof**
window. Once you have filled in the middle bit, you will find
that entry of the last line looks like this:

When you now press **Ok**, the proof will be finished and
you will be congratulated with a "Well done!" message.
Your completed proof looks like that illustrated on the first
page of this manual.

Should you ever want to go back and see the proofs you've done
in the present session, go to the **Windows** menu and select
**Previous Proofs**. You will see the proof you have just completed,
as well as any others you may have saved to the window in this
session.

You may print this proof; to do so, select **Print visible
windows...** from the **File** menu: this will print all
the windows presently on the screen. Remember first to hide any
windows on the screen which you don't want to print, by clicking
in their "close boxes".

If you make a mistake, note that you can undo it: just click
on the **Backtrack** button in the **Next Line** dialog.
Repeated clicking on this undoes the lines, one at a time, until
you are back at the start. Note that you can use the **Edit**
menu to copy formulae from the **Proof** window into the dialog
box. You can't paste them into the **Proof** window, lest you
construct incorrect proofs! Try all items on the **Edit** menu!

If you get tired of doing a proof, you can abandon it by clicking
the **Stop** button. You will be asked to confirm your decision.
Any work you have done on the proof will be lost---but you can
always copy the text in the **Proof** window to a window such
as the **Jotter** to remind yourself what steps you took.