Using the Fitch 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, go to Help with Language. The sole purpose of this help 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 premises and 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 either premise or assumption. Your sentence will now appear in Left. It will be appropriately numbered and given the appropriate justification. Note that anything entered as an assumption will be inset one column to the right of the sentence immediately above it. To prove a theorem one begins of course with an assumption. The theorem itself will appear in the main column, thereby indicating a derivation from the null set of premises. This will also be indicated in Top by the appearance of the sentence to the right of the |-. You can at any point remove the last line from Left by clicking on undo.

Next we need to know how to utilize the rules. Enter some conjunction in R1 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 clicking 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.

This system makes heavy use of reiteration. To reiterate a line you simply highlight it and click on Reit. You will receive an error message if the particular reiteration is disallowed. For example, you cannot reiterate a line in a discharged subderivation.

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.