10/15/14 under construction
[Deriver works in the form either of javascript widgets, which appear directly in a web page viewed through a web browser, or as a downloadable java application, which runs like any other application (usually off the desktop on your computer).]
With the widgets in web pages, it should be fairly clear what the possibilities are. The downloaded application offers more, but at the cost of being more complex.)
Video on the Application (useful also for understanding the Web Page Widgets)
The widgets (which usually are embedded in web pages)
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 (in the widgets that appear in a web page this is done automatically for you). 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.
An example of the Symbolization Widget. [For some reason, the Mac Safari browser is not now (10/15/2014) accepting click and drag to select text here. One workaround is to click and release at the start of your intended selection, then press the shift key and click and release at the end of your intended selection. Unbelievable!]
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.
An example of the Drawing Panel.
[For some reason, the Mac Safari browser is not now (10/15/2014) accepting click and drag to select text here. One workaround is to click and release at the start of your intended selection, then press the shift key and click and release at the end of your intended selection. Unbelievable!]
This panel is used for dealing with the semantics of formulas; roughly, for dealing with questions of reference and of truth and falsity.
The panel portrays an interpretation. In the supplied drawing there are two individuals a and b and a has the property F (but lacks the property G) and b has the property G (but lacks the property F).
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 Fa is taken to say that a has the property F (which it does) and so the formula is true. On the other hand Fb 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).
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.
(Try doing some drawing. The drawing is constrained to be well presented (e.g. you cannot have two separate individuals with the same name (though you can have one individual with several names, you'll have to look up Identity in the Notes for that))
You can colour or shade your properties as you wish.
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.
An example of the Proof Panel (press Pr1 for the above argument)
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, which 'toggles' it on, then click on the second line, which will toggle it on. 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.
There are also widgets for Trees, see, for example, Tree Widget . The above video on the Application shows how these are manipulated (the one difference is that selecting is by toggling (click-on click-off) largely because these widgets were designed to run on tablets, e.g. iPads.
Deriver's purpose is to help the User to learn how to symbolize, how to produced counter-examples, and how to produce derivations and trees.