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:- 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. - 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".
- 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.

- 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
- If you want to apply a
*definition*to a line of your derivation, you will have to do the following:- Select the line you want to apply the definition to in the derivation area.
- Select the definition you want to apply in the axiom/definition list. (You may swap these steps.)
- 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.
- 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.

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