This help does not explain the deductive system used. It presupposes familiarity with that. If you need help with the rules go to Help with Rules. If you need help with the formal language, read Help with Language. The sole purpose of this text is to explain the "mechanics" of the use of the builder.

Unless you have closed it the builder should be displaying in another window. Note that there are four important areas. In the long horizontal one at the top the proof builder displays error messages, informations and, in the progress of derivation, the argument you have derived so far.

The large area to the left is where your proof goes. It does not allow for direct user input. Instead, the prover keeps this area up-to-date for you. Whenever you add another line to your proof using the "Proposition entry" field and the rule buttons, the builder adds the respective line to your proof and, hence, to the large area at the left.

The area to the right is where user input takes place. It consists of a text field labelled "Proposition entry" and of six buttons, one for each derivation rule. For adding a line to your derivation (proof), you have to follow the following steps:

- Enter the proposition you want to derive in the text field labelled "Proposition entry".
- Select the line of the proof from which you want to derive the proposition you have entered. Certain rules do not need a line to be selected, namely the "Assertion" rule.
- Select the rule by which you want to derive the proposition you have entered.

If the derivation step you have entered by following these steps is valid, the builder adds it to the derivation on the left side. If it is invalid, it displays an error message in the top area. This message gives an indication, hopefully helpful, of why the attempted derivation is not valid.

Suppose, for example, that you want to derive
`P(P(Q)) |- Q`

(modus ponens). As a first step,
you will have to assert the premiss, `P(P(Q))`

. Do so
by entering it in the text field labelled "Proposition entry". Then
select the rule button "Assertion", thereby indicating that you
actually want to assert the proposition entered. Do you notice the
first line of your derivation, `1. P(P(Q)) Premiss`

,
being added to the proof?

As a next step in this derivation, you probably want to remove the
inner occurrance of "P" by deiterating it. This will lead to
`P((Q))`

. So, enter `P((Q))`

in the "Proposition
entry" field. Then, select the line you want to derive `P((Q))`

from - in this case, you want to derive it from the first and
only line. Note that you need not actually select line 1 because
the builder automatically selects the most recently added line;
selecting it a second time does no harm, either. Finally, tell the
proof builder that you intend to derive the proposition entered,
`P((Q))`

, from the line selected, 1, by the rule of
deiteration. To do so, select the button labelled "R4 deiteration".
At this stage, the proof should look as follows:

```
1. P(P(Q)) Premiss
```

2. P((Q)) 1, by R4

The next step probably will consist in removing the outer "P", leading
to `((Q))`

. This may be done with the rule of erasure (R1), because
the outer P is surrounded by an even number of cuts (more precisely,
it is surrounded by no cuts at all, zero being considered an even
number for purposes of R1). So, enter the desired result, `((Q))`

,
in the "Proposition entry" field, select line 2 (or omit this step,
having in mind that 2 as the most recently added line is preselected
automatically), and select the rule button "R1 Erasure". At this stage,
your proof looks as follows:

```
1. P(P(Q)) Premiss
```

2. P((Q)) 1, by R4

3. ((Q)) 2, by R1

Finally, you want to remove the double cut arount Q, thereby reaching the desired conclusion. Just enter "Q" in the "Proposition entry" field, select the automatically preselected line 3 (or, again, skip this step), and finally push the rule button "R5 double cut". Now your proof is complete:

```
1. P(P(Q)) Premiss
```

2. P((Q)) 1, by R4

3. ((Q)) 2, by R1

4. Q 3, by R5

If you have had an eye at the top area of the builder, the message area, you will have noticed that with each step the argument derived so far is shown there. After the last step, the message area will contain the message "Up to now, you have proven that P(P(Q)) |- Q", surely removing any remaining doubt about the nature of the derived argument.

There are a few minor convenience functions that may be of some interest. One thing is, if you double-click on a line in your derivation, the proposition derived with this line is being copied into the input field, "Proposition entry". This feature may save a lot of key presses and decrease the likelihood of typos if the proposition you want to derive differs only slightly from an existing proposition.

In the lower part of the applet there are four buttons labelled
"Clear all", "Undo", "Print view", and "Graphical view", respectively.
The *"Clear all"* button is dangerous: It clears the whole input,
i.e. it removes the whole argument. This may be used for starting
a new argument. The *"Undo"* button removes the line most recently
added to the derivation (there is no "redo" feature, so this button
should be treated with some care, too). The *"Print view"*
button opens up a new window that shows the whole derivation in a
copyable text field. This allows for copying the argument and for
pasting it into a different application, e.g. a word processor.
This may be useful if you want to print the derivation or if you
want to save it. (Remember that Java applets are not allowed
directly to print or to save data, so this feature may come in
handy.) Finally, the *"Graphical view"* button shows the
proposition of the selected line of your proof in a separate
window in a more graphical form. This may come in handy if you are
loosing control over a heavily bracketed expression.

© Christian Gottschall / christian.gottschall@posteo.de / 2012-03-31 01:19:53