Intelligent Editing
5/25/15
In the days before computer programs, logic derivations were done much as follows. There was the final product derivation, perhaps appearing line at a time flawlessly on a sheet of paper. There were all sorts of thought processes and conjectures concerning intermediate steps of the proof—such as, this middle line definitely follows from the initial lines and maybe it is of use to reach the final line, definitely this middle line leads to the last line and maybe it follows from the initial lines, maybe this ... Often these conjectures would be written in rough. (They certainly could not be written immediately as part of the final product for once committed they could not be crossed out and maybe some of them would not be needed.)
Deriver lets you display your thought processes, your rough work, and a tentative derivation and edit these to produce a final proof. It also allows you to work forwards or backwards or from lemma to lemma mid-proof.
Each of us works in different ways. Deriver just supplies the tools for you to use.
Here are some of the possibilities.
Example 1 A∧B ∴ B∨C which starts
and we can all see how to do this (split up the 'and' of line 1 taking the B and Or-introduce using the B to get B∨C) and probably the thought processes that gave us the insight were roughly: from A∧B, A follows and B follows, the last line B∨C probably comes from either B on its own or C on its own, it is the B that links these two (and neither the A nor the C are needed)... You can do the proof using those thought processes within Deriver. You can start
This represents the taking of A and B from A∧B. If you now see your way through, you can do the ∨I
This gives you a finished derivation, but not the best one. At this stage you can select line 2 and Cut Proofline which will give you
Alternatively you might just have used Prune which would have given you the same result. Now going back to
and considering the idea that the last line was obtained either from B or from C by Or-introduction. Click New Subgoal (off the Edit Menu) and take B as a subgoal; click New Subgoal and take C as a subgoal;
As a reminder: the question marks in the body of the proof represent missing proof segments; the double arrow head '<<' indicates which problem you are working on. The line after the one marked by '<<' is often called the current target. (Click on another question mark to work on a different problem, to change the current target). Now there are all sorts of possibilities. Starting from the top. You can Cut Proofline on line 2 to remove A (which is not needed); you can Cut Proofline on line 5 to remove B (which you already have as line 3); you can Cut Proofline on line 7 to remove C (which is not needed); you can Or-Introduce on the B's or line 5 to get the final line 9....
Cut Proofline cuts the selected line, if such a cut is permissible. Prune is a good deal more potent; it automatically cuts all prooflines that can be cut. Usually the best strategy is to use Prune only when a proof is finished; for in an unfinished proof almost all lines can be pruned (and that will leave you surprisingly little).
(Keep in mind the standard safety net; anything you do can be undone, provided you Undo it straight away.)
Cut Proofline, Prune, and New Subgoal are fine for most purposes. They are not entirely suitable when the subgoal is the outcome of a subproof. They need supplementing by the Tactics option; this lays out the missing pieces for sub-proofs. Consider, for example, a derivation of ∴((F∨F)⊃F)∧(F⊃(F∨F)). This starts
This is going to be two Conditional Proofs, the results of which are put together with conjunction. Let us use New Subgoal to put both the conjuncts.
Notice that I have (deliberately) made a typing error with line 4 and put in F⊃(F∧F) instead of F⊃(F∨F). Let us now start from the beginning by clicking on line 1 to change the current target from line 6 to line 2.
Maybe we are not clear how to do Conditional Proof (⊃I). If Tactics are switched on (under the Wizard Menu) and ⊃I clicked, the program lays out
Then line 1 can be selected and ∨E (with Tactics) used to get
If ⊃I is clicked now, for the second conditional proof, the program lays out
Suppose we realize at this point that a mistake has been made. Cut Proofline can be used here in a variety of ways. It can be used to cut line 5 (but really we want that one). It can be used to cut lines 8, 7 and 6 (which is where the mistakes are). We first click on line 10 to move the current target down and thus make line 9 selectable.
Select and cut line 9.
This cut will take lines 8,7,6 with it. We can now do the last line by the Tactic of ∧I.
Then the Tactic of ⊃I.
Finally the Tactic of ∨I.
A point to remember is that to use Cut Proofline you must first select a line; you can select lines only from before your current sub-goal; so you can use Cut Proofline only on lines before your current sub-goal. If you want to cut lines from after your current sub-goal, you must either move the current sub-goal to a later sub-goal and make the lines of interest before your new current sub-goal or finish the proof completely, removing all goals, then go back and cut the lines you do not want.
There is a trap here. If your taste is for doing proofs backwards and you are not very good at it, you can leave yourself with unwanted, but yet uncuttable, lines. Take the proof (in System 2) of F, F ⊃ G∴ G which starts
Suppose that I am convinced (somewhat bizarrely) that the last line has been obtained from G∧H by taking the ∧ out; I thus use New Subgoal to insert
so far so good, (or so bad), but if I now insist on doing that last step (which I am convinced is correct, but in fact is not) the result is:
and now line 4 cannot be cut because it can never be selected, further it can never be proved because it does not follow from the premises and previous lines (so the whole proof can never be completed). The entire proof will have to be done again.
Moral: if your taste is for doing proofs backwards and you are not very good at it, do not follow through on the very last step until last (that way you can correct your errors). (Thought was given to whether the program should prevent the User from the silliness that I displayed in the last example, and the decision was that it should not.)