Using the Lemmon Builder Applet

(this text by Steven DeHaven, Calgary, and Christian Gottschall, Vienna)

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 white areas. The long horizontal one at the top we shall call 'Top'. The single area below that on the left we will call 'Left'. The two white areas on the lower right will be called 'R1' and 'R2'. Top is an area in which, for example, error messages will appear if you attempt to do something that the system does not allow. Top does not allow of any user input. Left is the area in which the derivation you are attempting will appear. It does allow of user input. Clicking on a line will highlight it. Clicking on an unhighlighted line will remove the highlighting. Clicking on the Unselect button will also remove highlighting, while clicking Undo will remove the lowest line in Left. We will return to a discussion of Left later.

R1 is the area in which one enters assumptions. Move your mouse to R1 and click. A blinking cursor will appear. You can now make entries in this area. Try entering some sentence of the formal language in R1. Once you have entered the sentence click on the A (assumption) button. Your sentence will now appear in Left. It will be appropriately numbered and given the appropriate justification.

Next we need to know how to utilize the rules. Enter some conjunction in as a premise, for example, 'P & Q'. We want to apply &E to this line. First move your mouse to Left and click on the sentence. It will now be highlighted. You can eliminate the highlighting by clicking on the highlighted line or clicking on Unselect. But, in general, you highlight a sentence or sentences to which you wish to apply a rule and click on the relevant rule button. Generally error messages will appear in Top if you attempt to do something that is not allowed by the system. In this case click on &E. Note that both P and Q will appear in R2. This indicates that the application of a rule could lead to more than one result. You have to decide which result you want. You select the result by double-clicking in R2 on that result. It will then be added as a line with the correct number and appropriate justification.

Any other difficulty you may have will most likely be caused by a lack of familiarity with the particular traits of this system. The system is complete so in principle you can derive anything that follows. As is true in virtually all systems not everything which obviously follows is easy to derive.