The Drawing Panel
6/7/08
The Drawing Panel is used for semantics.
Drawing
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).
Unary functions are depicted by lines with arrow-heads (just like binary relations). You can supply a function-- by selecting a line on the palette and typing a function name (usually any lower case letter, 'f', for example). Or you can use a function already displayed in the palette. The program assumes that displayed functions 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 with itself as the function value, 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 unary function between individuals, but not a unary function in empty space. Similarly if you have a unary functions between individuals you can select and cut that unary function to leave the individuals, but you cannot select and cut either individual (for that would leave a unary function with at least one end in empty space).
Binary relations and unary functions have many similarities to each other, and you can use the template in the palette for one to draw the other (just remember that upper -case, say 'F', is a relation and lower-case, say 'f', is a function). The templates differ in where the name is drawn (in one it is above the line, and in the other it is below the line). This should allow you to draw several relations or functions between the same two individuals without the names on the lines obscuring each other.
Objects in the Universe can have several names. An object in the Universe has the first name used to describe it displayed within its circle. This, so to speak, is the individual's baptismal name (and it is the name used when describing the Interpretation). Any subsequent names or 'aliases' are introduced by means of labelled lines to the individual. The thought here is that constants are zero-ary functions; that is, functions which have a value but which have no arguments. So if these are to be depicted by directed lines, then the arrow head should be on the value, but the arrow tail can start anywhere. A drawing can thus be produced to depict the truth of a statement like 'a=b'. (But you cannot give the same name or alias to two separate individuals.)
You now know the constraints: no name can name two distinct individuals, and 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.
Truth, Satisfiability, and Semantic Invalidity
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, Gf(a)∧Hg(b) 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 referred to by the value of the function f applied to a and there is an individual b in the drawing and there is a property rectangle for H which surrounds the individual referred to by the function g applied to b.
A design decision was made which throws light on examples similar to the last one. In ordinary life, functions can be partial or total; for example, the function 'eldest son of..' may have a value for Mary if Mary has an eldest son, but no value for Tom if Tom has no children. In standard semantics, though, functions have to be total, and this motivated a design decision which will be explained now. In semantics, when you have relations, individuals may or may not possess them, so with a universe {a,b,c} and a binary relation R, perhaps none of the pairs of the individuals have the relation and R might be empty and ={} ; but when you have a function that function must be total, that is, every individual in the universe must have a value defined for that function so f, for instance, cannot be empty and must equal something like f¡={<ab>,<bb>,<ca>}. This means that drawn lines can be used to depict relations somewhat more easily than they can be used to depict functions.
In the systems used here, there are 26 unary functions (a()..z()) and each of these must be shown to be total in the drawing, so each individual in the drawing should have 26 drawn lines emanating from it. This would be a mess. The choice was made to adopt a default which is not depicted by drawn lines. Each function is taken by default to be identity, and each instance of each function is taken to be an identity pair. No drawing is used to show this. However if a function line is drawn between individuals that line instance overrides the default identity instance. This sounds worse than it is. To run through an example, consider whether the formula Hf(a) is true in a given drawing... first we have to find which individual is referred to by f(a) and to do this we look at a and see if there is a function line labelled f that comes from a and goes to an individual; if so that individual is the one referred to by f(a); if not we fall back to the default and f(a) is taken to refer to a itself; having found the individual all we have to do is to see whether it is in an H-rectangle and that will tell us whether Hf(a) is true.
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.
In the downloadable program (and with the relevant applets), 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.)