Using the Peirce Alpha Graph Proof Builder Applet

Open the applet in this window…

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.

An Example

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.

Additional Remarks

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.