Using the Hilbert-Style 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 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.)

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:

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@univie.ac.at / 2012-03-31 01:19:53