11/16/06
The Drawing Panel is used for semantics.
The Drawing Panel is similar in behaviour to many drawing and painting programs-- most of the selecting, sketching, dragging, cutting, pasting, undo-ing operations are there. Differences in behaviour stem from the meaning given to the drawing and the need to be faithful to that meaning.
The meaning given to the drawing is that of depicting a universe or world which contains individuals, and these individuals perhaps have properties, perhaps have aliases, and perhaps bear relations to other individuals.
The small circles containing letters are taken to be individuals with constant proper names. You can supply a name-- by selecting the circle on the palette and typing a constant (usually a small letter early in the alphabet, 'c', for example). Or the program will automatically produce a name for you. Each circle has to have its own name and each name has to be different. Because of this you cannot use a name that is already there (nor can you, for example, select an individual, copy it, and paste it in a second time).
A minor point to be wary of is that selected items are not considered to be part of the drawing. When you first draw an individual it is selected and thus is not displayed as being part of the Universe. If you click down anywhere else that action de-selects the individual and you will see the individual become part of the Universe.
Properties are portrayed by rectangles. You can supply a property-- by selecting a rectangle on the palette and typing a predicate (usually any upper case letter, 'Q', for example). Or you can use the property already displayed in the palette. If an individual is within a property rectangle it is taken to have that property (and if an individual does not have a property it lacks that property). The program assumes that displayed properties have to be instantiated. So you can draw a rectangle around an individual, but not a rectangle in empty space. Similarly if you have a rectangle around an individual you can select and cut that rectangle to leave the individual, but you cannot select and cut the individual (for that would leave a rectangle in empty space). You can color or shade the rectangles as you wish.
Binary relations are depicted by lines with arrow-heads. You can supply a relation-- by selecting a line on the palette and typing a relation name (usually any upper case letter, 'M', for example). Or you can use a relation already displayed in the palette. The program assumes that displayed relations have to be instantiated-- both ends of the line have to be on an individual. You must click on an individual to start (and hold the mouse-button down). What will be displayed initially is a large circle (showing the individual related to itself, which is acceptable); as the mouse is moved away the circle will change to a line and the end of the line must be latched on to a second individual (once you have done this, release the mouse-button). So you can draw a relation between individuals, but not a relation in empty space. Similarly if you have a relation between individuals you can select and cut that relation to leave the individuals, but you cannot select and cut either individual (for that would leave a relation with at least one end in empty space).
You now know the constraints: displayed properties and displayed relations and functions have to be instantiated. The standard drawing operations are altered to meet these constraints. So, for example, if you have a single individual within a rectangle and you try to drag that individual outside the rectangle (thus leaving an uninstantiated property) the individual will hop back inside the rectangle to preserve propriety.
Selected formulas (or lists of formulas) in the Journal Panel or a Text Panel are taken to refer to the current drawing in a Drawing Panel.
A formula is true (in the drawing or interpretation) iff aspects of the drawing are as the formula asserts them to be. So, for example, a formula Fa is true in the drawing iff there is an individual a in the drawing and there is a property rectangle for F which surrounds a. And, as another example, Ga∧Hb is true in the drawing iff there is an individual a in the drawing and there is a property rectangle for G which surrounds the individual and there is an individual b in the drawing and there is a property rectangle for H which surrounds b.
There are some unusual or borderline cases concerning truth in an interpretation. It may be that the given formula, Fc for example, contains a constant term, c, for which there is no individual in the Universe of the drawing; the drawing's Universe may contain only {a,b}. Here the question of the formula's truth is not entirely appropriate-- if there is no c how can we discuss whether c possesses F? The program will just give an error warning asking for the Universe to contain c. Some formulas contain free variables, Fx, for example, contains a free x. Whether this formula is true depends on which individual x refers to. The program will ask you to value x and thus indicate which individual x refers to. Valuations are given by following a formula with a pair of square brackets containing, for example a/x , and this means that x is valued to be a. For example, Fx[a/x] means the formula Fx with a as the value of x.
A formula is satisfiable iff there is an interpretation (or drawing) in which it is true.
Selecting a formula and clicking Satisfiable invites the program to answer this. The question may take time (pressing command period stops the program considering it). The program will try to answer the question, and then do the drawing for you.
The program will not do the drawing if there is already a drawing there (you should Clear the existing drawing).
There are limits on what the program can draw: no more than about twenty individuals ('a' through to 't'), no more than three different predicates, no more than twenty six different relations ('A' through to 'Z'). But it will do what it can.
In some cases it does not complete the drawing, and behaves apparently incorrectly. If the program knows that a formula is satisfiable in an infinite universe, it will try to produce a finite drawing of this and usually the drawing will be incomplete. Take the formula for Everything loves something namely, (∀x)(∃y)Lxy. The program will think about this as follows:- let's start with aRTHUR, he has to love say bERYL, and in turn she has to love cHARLES, and so on ....; this is satisfiable in an infinite Universe; I cannot draw an infinite Universe; but I can draw aRTHUR loving bERYL and so I will.... What the program does not think about is that, sadly, aRTHUR loving bERYL does not satisfy (∀x)(∃y)Lxy because bERYL does not love anybody in this interpretation. What is needed is for the extra relation of bERYL loving aRTHUR to be added. This extra relation forms a cycle-- a loves b and b loves a (and the program has been taught to avoid these). The program will give a warning that the interpretation is incomplete because it has used an infinite universe and it will suggest that you complete the interpretation by forming suitable cycles. (The program is being taught how to form cycles, but for the moment you will have to do it by hand.)