Using the Hilbert-Style Proof Builder Applet

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 message area) 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 the derivation area 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 "Axiom", "Assertion", and "Modus ponendo ponens" button, the builder adds the respective line to your proof and, hence, to the large derivation area at the left. If, on the other hand, you want to apply the rule, modus ponendo ponens, to two lines of your prove, you need to select the respective lines in this area. Similarly, if you want to apply a definition to an existing line, you will have to select the respective line. Note that selecting one or more lines is done with the mouse, multiple selection sometimes requiring an additional key to be pressed (depending on what operating system you are using).

The area at the upper right is the axiom and definition area where the available axioms and definitions are displayed. You may change the axiomatic system by choosing the "Setup" button. Doing so will automatically start a new derivation.)

• If you want to add an instance of an axiom to your derivation, you have to follow the following steps:
  1. Select the desired axiom in the axiom/definition list. As soon as you have done so, the builder shows a new area just below the axiom list: This is the substitution editor where you may enter which proposition to substitute for the atoms of the selected axiom.
  2. Enter your desired substitution. If, for example, you want to substitute the proposition "P & Q" for the atom "P", edit the text field labelled "substitution for P" such that it contains the desired substitution, "P & Q".
  3. When your substitution looks right, finally select the button labelled "Axiom". The builder will add the substitution instance of the selected axiom to the derivation area.
• If you want to apply a definition to a line of your derivation, you will have to do the following:
  1. Select the line you want to apply the definition to in the derivation area.
  2. Select the definition you want to apply in the axiom/definition list. (You may swap these steps.)
  3. If the definition is applicable to the respective line, a list of possible substitution instances appears in place of the substitution editor, i.e. below the axiom/definition list. This requires no user interaction.
  4. Select the desired substitution instance and select the button labelled "Definition". Alternatively, you may simple double-click on the desired substitution instance. The builder will add the substitution instance of the selected definition to the derivation area.

You have already used the fourth area at the lower right: This is the control area where the buttons are. You are already familiar with the button labelled "Axiom". The other controls are the following:

• The "Assertion" button allows for introducing assertions into the derivation: For doing so, first enter the desired assertion in the text field to the right of the button; secondly, press the "Assertion" button. The desired assertion will be added to the derivation.
• The "Modus ponendo ponens" button applies the derivation rule of modus ponendo ponens (short: modus ponens). If you want to apply the modus ponendo ponens, first select the two lines of your derivation you want to apply the rule to. Secondly, select the "Modus ponendo ponens button". At the press of your fingertip, the rule will be applied, and the resulting proposition will be added to your derivation.
• The "Setup" button allows for using an axiomatic system of your own. After choosing "Setup", the builder will display a large text area containing the current axioms. You may at any time change them, replace them, or add axioms of your choosing. Note that the builder will not try to assure that your axioms are making sense - all they need to be is syntactically well-formed. To start using your newly entered axioms, select the "Accept" button. If you are experiencing second thoughts, you might prefer the button labelled "Reject" which will cancel your input and reset the builder to the most recently used axiomatic system.
• The checkbox labelled "Polish Notation" allows for switching to Lukasiewicz's ingenious bracket-free notation.
• All the "Print view" button does is showing your whole derivation in a separate window. This separate windows allows for copying, empowering you to "copy & paste" your derivation to any other program of your liking, e.g. a word processor. Since Java applets are not allowed to access the system clipboard themselves, this is the only way to get your derivation into another program.

An Example

Suppose, for example, that you want to derive P->P. First, you will have to instantiate axiom 2, substituting Q->P for Q and P for R. In the axiom area, select axiom 2. In the substitution area, change the content of the text field labelled "substitution for Q" to "Q->P", and the content of the text field labelled "substitution for R" to P. Then select the button labelled "Axiom". This will result in the following line to be added to the derivation area to the left:

1. (P -> ((Q -> P) -> P)) -> ((P -> (Q -> P)) -> (P -> P)), Ax 2

Next, you will want to instantiate axiom 1, substituting Q->P for Q. First, select the axiom in the axiom area to the right; then enter the substitution, "Q->P", in the text field labelled "subsitution for Q". After doing so, again select the "Axiom" button. A second line will be added to the derivation:

1. (P -> ((Q -> P) -> P)) -> ((P -> (Q -> P)) -> (P -> P)), Ax 2
2. P -> ((Q -> P) -> P), Ax 1

Now, by applying the modus ponendo ponens to these two lines, you may derive the proposition ((P -> (Q -> P)) -> (P -> P)). For doing so, first select both lines of the derivation. Then select the button labelled "Modus ponendo ponens". This will result in the desired third line to be added to the derivation:

1. (P -> ((Q -> P) -> P)) -> ((P -> (Q -> P)) -> (P -> P)), Ax 2
2. P -> ((Q -> P) -> P), Ax 1
3. (P -> (Q -> P)) -> (P -> P), 1, 2, MPP

For deriving the desired result, P > P, you will need two more steps: First, use axiom 1 for getting the antecedent of the proposition shown in line 3. Secondly, apply modus ponendo ponens to these two lines. After these two steps, your derivation will be the following:

1. (P -> ((Q -> P) -> P)) -> ((P -> (Q -> P)) -> (P -> P)), Ax 2
2. P -> ((Q -> P) -> P), Ax 1
3. (P -> (Q -> P)) -> (P -> P), 1, 2, MPP
4. P -> (Q -> P), Ax 1
5. P -> P, 3, 4, MPP

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