2.1 Checking a Proof

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.