5/23/2015
Using Tactics
[Tactics are available for each of the logical systems. There are small inessential differences between these. The explanation being given here is in terms of System 1, but the principles apply to the other systems also.]
Tactics are a simple yet extremely powerful problem solving heuristic. Further, Deriver is able to display and run Tactics in an effortless and unobstrusive way.
The idea behind Tactics is as follows. Say we are trying to prove A∧B,C ∴ B∧C. We think of the premise or premises, assumptions, and lines that we have proved so far, as the facts that we have, and the conclusion as the problem that we are trying to solve. There may be facts which are compound propositions containing connectives; in which case we can use the tactic of employing logical Rules which remove connectives to extend the facts. In the example, A∧B is among the facts and the Rule ∧E can be applied to this to extend the facts to A∧B, C, A, B. Turning now to the problem. It may be a compound proposition containing a connective; in which case we can use the tactic of employing logical Rules which introduce connectives to anticipate sub-problems which have to be solved before the final problem. In the example B∧C is a compound proposition and we can guess that the Rule ∧I, applied to B and C separately, was used to obtain it; and thus the problem B∧C is removed and B and C become subproblems to be solved. A subproblem is solved by being or becoming one of the facts. And a proof is complete when there are no further problems or subproblems.
Deriver displays and implements all fact extending tactics with little or no difference from the standard production of proofs. You select the line or lines you wish to apply the Tactic to, and click the appropriate elimination Rule. For example, to extend the fact A∧B you select the conjunction and click on ∧E. The small differences are as follows. The Rules ∨E and EI require selecting both lines and sub-proofs. The Tactic here generates the sub-proofs automatically, so there is no need to have or select those (of course, you still have to select the disjunction or the existential formula).
Deriver displays and implements all problem reducing tactics with one large difference from the standard production of proofs. Since there is only one conclusion or only one problem under consideration at a time, it is unique. So there is no point in selecting it, and there is no need for you to do so. All you do is to click the appropriate connective introducing Rule. For example, with the conclusion B∧C click ∧I. When a tactic is used to reduce a problem to more than one sub-problem, the question arises as to which sub-problem to consider first (since always only one problem is under consideration at one time). The usual approach here is to have a default. One can always look at the last available sub-problem first (and do a proof backwards). Or one can look at the first available sub-problem first (and do a proof forwards). Deriver allows you to change problems (merely by clicking on the appropriate question mark), so you are free to do as you wish. But, if there is no intervention from the User, Deriver will do proofs forwards.
To see Tactics in action, follow this example through... [If you have the downloaded application you can actually do it. Select and start a derivation of ∴(∃x)(Fx ∨ Gx) ≡(∃x)(Fx) ∨ (∃x)(Gx). Switch on Tactics under the Wizard Menu.]
Now click ≡I, the display will change to
What has happened here is that you have used the Tactic for ≡I, and this reduces the problem to the two separate problems indicated by question marks. It lays out the assumptions you have to make and the sub-proofs you have to complete. The << points to line 2 which is to say the present problem is that of proving (∃x)Fx∨(∃x)Gx . (Of course, if you would rather do the other problem first, that option is available to you.) Now select line 1 and click EI . The display will change to
We have used the Tactic for EI on line 1. Notice that what we are doing is virtually automatic. When we started we had only one line, so we used a tactic on it; that gave us some other lines and we are using tactics on those one at a time. You can guess what is going to happen next. Select line 2 and click ∨E.
At this stage the << is level with line 4. Tactics have been used on lines 1 and 2, and line 3 is atomic and not open to a Tactic. That leaves only line 5. Click ∨I to get
The Tactic for ∨I has been programmed defensively. Theoretically, the pure Tactic for ∨I is to have one or the other of the disjuncts as a subproblem. But usually at the time you use the ∨I Tactic you do not know which one you want—it would be foolish to make you choose. Deriver gives you both sub-problems, and, when the choice is clear, you can use its editing facilities to cut out the one that you do not want. You can see that you can prove line 5 by simple existential generalization from line 3 so we will cut line 7 by selecting it and using Cut Proofline.
Just click ∨I again to get
And line 5 is obtained from line 3 by existential generalization mentioned earlier.
We have to do a similar thing for the sub-proof from lines 6 to 8, but we know how to do it now—do an ∨I and an existential generalization
And thus the first half of the proof is complete (the second half is left as an exercise...)