10/16/14 under construction
Video on the Standalone Application
In Logic, typically you will be presented with an argument in English, have to symbolize it, have to form a view as whether it is valid or invalid, and then produce a proof to back up your view (or produce a counter example).
Deriver allows you to symbolize English as follows. You select whether you want to work at propositional level or at predicate level. Then by selecting an entire English sentence and clicking to symbols the program will do one step of the translation and leave you something which is akin to a formula with only its main connective symbolized and the other parts in English. By selecting the parts in English and repeating the process you can symbolize the entire formula. For example, at propositional level,
Forests are widespread and it is not the case that hills are rare.
will transform to
(Forests are widespread ∧ it is not the case that hills are rare)
and then to
(F ∧ it is not the case that hills are rare)
and then to
(F ∧ ~ (hills are rare))
and finally to
(F ∧ ~ (H))
Similarly for translating symbolized formulas back to English.
If the program cannot translate, it will do nothing. There are two separate cases where the program cannot translate. First when it does not know the grammar, parts of speech, or propositions—the program can be taught these (the documentation explains how to do this). Second when the User makes a slip.... the program's ability to translate English into symbols works on English, it does not work translating symbols into symbols or a mixture of English and symbols into symbols... so part way through a translation when you obtain something like
(F ∧ ~ (hills are rare))
you have to be sure to select the 'hills are rare' and not the whole thing ('hills are rare' is in English, the whole string of logical symbols and English is not). Similar considerations apply for retranslating back from symbols into English.
Eventually you will have your symbolized argument....
An argument is valid iff it is not possible for all the premises to be true and the conclusion false at one and the same time. Alternatively, an argument is invalid iff it is possible for all the premises to be true and the conclusion false at one and the same time. An argument can be proved to be valid by producing a suitable derivation for it. And an argument can be proved to be invalid by exhibiting a counter-example in which all the argument's premises are true and its conclusion false. Your best strategy for forming a view is to: a) first assume that the argument is invalid and try, quickly, to produce a counter-example to it , b) if this search does not succeed, abandon it without expending too much time, and instead assume that the argument is valid and try to produce a derivation of it, c) if the search for a derivation does not succeed, abandon it and start again through (a) and (b), but this time giving more time to each.
Deriver allows you both to produce counter-examples and to produce derivations. Let us see this at work with some examples. Take the argument
If Arthur is wearing a green tie, he will stand out in a crowd. Arthur stands out in a crowd. Therefore, Arthur is wearing a green tie.
which symbolizes to
Ga⊃Sa, Sa ∴ Ga
You have to decide whether this argument is valid or invalid. Let us tentatively assume that it is invalid, and let us see if it is possible for all the premises to be true and the conclusion false at one and the same time. To discuss the truth of statements like Ga⊃Sa, Sa, Ga we need something for the 'a' to refer to. Let us imagine a Universe which has an individual a in it. We are aiming to have Sa true (as it is one of the premises) and Ga false (since it is the conclusion). So, suppose our a in the Universe has the property S but lacks the property G. In such a scenario, the other premise Ga⊃Sa also comes out to be true ( for it is an 'if-then' statement with an 'if-clause' that is false and a 'then-clause' which is true). The argument Ga⊃Sa, Sa ∴ Ga is definitely invalid, and a counter-example to it is a Universe with an a in it which has property S but does not have property G.
Deriver's Drawing Panel allows you to display such counter-examples.
This panel is used for dealing with the semantics of formulas; roughly, for dealing with questions of reference and of truth and falsity.
Individuals are circles, properties are rectangles which may or may not surround a particular individual, and relations are lines which connect individuals.
If an individual is within a property rectangle; it is considered to have that property. If it is not, it does not. So if you have an individual 'a', and no property 'P' , then a is taken to lack P and so the formula Pa is false. Similarly if R connects a and b then Rab is true, but if there is no S connecting a and b then Sab is false.
Formulas are taken to be about the Drawing panel. So a formula Sa is taken to say that a has the property S (which it does) and so the formula is true. On the other hand Ga is false.
The Current Interpretation is shown on the Interpretation panel (which starts top left in the drawing, although the User can put it wherever they wish). With some configurations, especially in the standalone Application, there will be a Current Interpretation command, under the Semantics Menu—this writes the current interpretation out to the Journal Panel.
Some formulas whose truth interests us contain free variables, for example Fx—these need to be 'valued'. This is done by writing Fx[a/x] which tells us that the free variable x is understood to denote the individual a. With some configurations, especially in the standalone Application, there will be a Current Valuation command, under the Semantics Menu—this writes the current interpretation out to the Journal Panel.
(Try doing some drawing. Click on the circle in the palette, click on the point you want it in the window, move it slightly (to show your clicks are really intended), then release. This will leave you a little circle, probably with four blobs on it. The blobs mean that the individual is still selected. Selected items are not considered to be genuine parts of the drawing. Click down somewhere else in the drawing. This will stop c being selected, and thus add it. Up in the top left corner is a description of the drawing. You should see that c is now part of the Universe. Try the same for properties and relations. The drawing is constrained to be well presented. An individual may or may not have a property. So you can draw (or move) individuals almost anywhere. But properties must apply to at least one individual-- you can draw a property around an individual, but not in empty space. Similarly for relations.)
Individuals are named by constant terms. If you want to call one, say 'g', just select on the palette to draw an individual and type 'g', then draw it. If you are not fussed about which individual you want, one will be supplied for you.
Similarly for properties,relations, and functions. If you want a property called 'Q', select on the palette, type 'Q' and draw. If you want a relation called 'A', click on a relation in the palette, type 'A' and draw.
You can colour or shade your properties as you wish.
If you wish, the program will argue with you about the truth of formulas (Game Theoretical Semantics). To take a simple example. Consider
form a view as to whether it is true. If you think it is, you will select it and press Endorse (off the Semantics Menu). If you think it false, select it and Deny it. (Then keep selecting formulas and Endorsing or Denying as directed.) If you Endorse it you will lose quickly, like this
Consider a second argument.
If Arthur is wearing a green tie, he will stand out in a crowd. Arthur is wearing a green tie. Therefore, Arthur stands out in a crowd.
which symbolizes to
Ga⊃Sa, Ga ∴ Sa
Let us tentatively assume that it is invalid, and let us see if it is possible for all the premises to be true and the conclusion false at one and the same time. Let us imagine a Universe which has an individual a in it. We are aiming to have Ga true (as it is one of the premises) and Sa false (since it is the conclusion). So, suppose our a in the Universe has the property G but lacks the property S. In such a scenario, the other premise Ga⊃Sa now comes out to be false ( for it is an 'if-then' statement with an 'if-clause' that is true and a 'then-clause' which is false). This scenario does not form a counter-example-- we have not displayed a Universe in which all the premises are true and the conclusion false.
Let us try again... we wish to have Ga true, so suppose a has the property G, we wish to have Ga⊃Sa true and the only way that can be, if Ga is true, is if Sa is true, so suppose a has the property S, but we also wish to have the conclusion Sa false, but it is true if a has the property S ... At this point we abandon the search for a counter-example and instead guess that the argument is valid and attempt to find a derivation of it.
Deriver's Proof Panel allows us to find and display derivations.
The Proof panel contains a number of items. There is the proof itself. There are the premises, a ? to indicate the missing proof, and the target conclusion. Each line has its justification on the right-hand side. Notice that the justification of one of the lines has << next to it; this means that any new lines will be added here. Lines are selected by clicking on them. To select two lines, you click on the first, then, while pressing the command-key (which is the clover leaf key on the Macintosh), click on the second line. On the Rules menu are 'menu items' for the Rules of Inference. You first select the desired lines, then click the Rule.
Some Rules of Inference require you to make a choice. For example, ∧I with A and B permits A∧B or B∧A, and you have to choose which you want. You will be asked for a choice.
Some Rules of Inference require you to supply a new formula. For example, ∨I with A permits (A∨<newformula> ) for any well formed formula <newformula>. Supplying a new formula is similar to making a choice, but you have to enter the new formula. Of course, your addition has to be a proper formula. If it is gobbledegook, you will be told so. Usually you have either to supply a proper formula, or Cancel. Entering new formulas is mildly awkward because you have to use the proper symbols, which do not appear on the keyboard. There are several techniques. While doing a proof, clicking on a line will load the formula of that line into an entry panel-- which you can then edit to get what you want. You can copy and paste (or drag and drop) from the symbol palette (and any text that has the proper symbols).
You will notice that much of the time when the program writes messages (for example, error messages) to you those messages will be selected-- this means that you merely have to type anything for the (now unwanted) message to disappear. Another tip: whenever you click on a formula in the Proof Panel it appears in the Entry rectangle (if there is one). This makes entering formulas easier. Many times what you want is similar to a formula already in the derivation, so just click on that formula then Edit the result in the Entry rectangle. For example, if you want to Enter the negation of an existing long and complicated formula, just click on that formula, and enter a negation sign in front of the displayed text.
The Rewrite Rules menu choice opens up rules for rewriting formulas-- see rewrite rules.
The derivations can be done intelligently.
Deriver's Tree Panel allows you to do trees. The above Video illustrates a tree being constructed.
Deriver's purpose is to help the User to learn how to symbolize, how to produced counter-examples, how to produce derivations, and how to produce tree proofs or tree counter-examples.