6/23/07
An unfinished derivation can be thought of as being a collection of 'facts' that you have and a collection of 'problems' that remain to be solved. The standard way of approaching a proof consists of extending the facts, essentially doing the proof in a forwards direction, until no problems remain. But it is also possible to do a proof, or parts of a proof, by looking at the problems, and reducing these to earlier problems, essentially doing the proof in a backwards direction, again until no problems remain.
Tactics are a means of allowing the User to adopt a flexible approach to a proof, by doing it forwards, backwards, or a mixture of both. Tactics are switched on from the Wizard menu (and they can be toggled on and off while a proof is in progress, if that is what the User wants).
Most of the Tactics are problem solving or backwards tactics. And these work with the current problem, that is with the next target line or the insertion point. Now, since this line is unique, there is no need to select it. So most the Tactics do not need any selection of lines in the proof, they just need to user to invoke the appropriate Menu item. Some Tactics, particularly fact extending ones, do need the selection of lines. Just which lines need to be selected is noted in the documentation below.
This behaves the same as the Rules.
It is unusual to make an assumption while using tactics (because that assumption can never be dropped)-- so this tactic is discouraged.
This Tactic can be employed when the current target has the form ~<formula> , thus
? ? << ∼<formula> ?
That is, the formula you are trying to obtain has a ∼ as its main connective-- the formula you are trying to obtain has the form ∼<formula>.
The Tactic asks for the <positive horn> of the contradiction. (It also gives you a bit of a hint here; it lists all candidate Positive Horns; you just have to choose the right one...) [Explanation of the terminology:- When you have a contradiction say A and ∼A , one of the formulas (the one without the negation in front) is known as the 'positive horn' of the contradiction, and the other, the 'negative horn'. So, to give a further example, with the contradiction ∼(∀x)∼Gx and (∀x)∼Gx, the positive horn is (∀x)∼Gx and the negative horn ∼(∀x)∼Gx.]
The program lays out all or part of
n
<formula> Ass n+1
? ? n+2
<positive horn> ? n+3
? ? n+4
<negative horn> ? n+5 ∼<formula> n+2, n+4∼I
It checks the facts. If <positive horn> is available, then lines n+1 and n+2 are omitted (and the line numbers adjusted). If <negative horn> is available, then lines n+3 and n+4 are omitted (and the line numbers adjusted).
This is similar to ~I (its underlying reasoning is reductio ad absurdum) but it is more general. This Tactic can be employed when the current target has any form, say <formula>, thus
? ? << <formula> ?
The Tactic asks for the <positive horn> of the contradiction. (It also gives you a bit of a hint here; it lists all candidate Positive Horns; you just have to choose the right one...) [Explanation of the terminology:- When you have a contradiction say A and ∼A , one of the formulas (the one without the negation in front) is known as the 'positive horn' of the contradiction, and the other, the 'negative horn'. So, to give a further example, with the contradiction ∼(∀x)∼Gx and (∀x)∼Gx, the positive horn is (∀x)∼Gx and the negative horn ∼(∀x)∼Gx.]
The program lays out all or part of
n
~<formula> Ass n+1
? ? n+2
<positive horn> ? n+3
? ? n+4
<negative horn> ? n+5 <formula> n+2, n+4∼E
It checks the facts. If <positive horn> is available, then lines n+1 and n+2 are omitted (and the line numbers adjusted). If <negative horn> is available, then lines n+3 and n+4 are omitted (and the line numbers adjusted).
This Tactic can be employed when the current target has the form <formula1>&<formula2> , thus
? ? << n <formula1>&<formula2> ?
It displays all or part of
n ? ? << n+1 <formula1> ? n+2 ? ? n+3 <formula2> ? n+4 <formula1>&<formula2> n+1,n+3∧I
It checks the facts. If <formula1> is available, then lines n and n+1 are omitted (and the line numbers adjusted). If <formula2> is available, then lines n+2 and n+3 are omitted (and the line numbers adjusted).
This behaves the same as the Rules (and so you need to select a conjunction from among the 'facts').
This Tactic can be employed when the current target has the form <formula1>∨<formula2>, thus
? ? << n <formula1>∨<formula2> ?
It checks the facts. If either <formula1> or <formula2> is available, as line k, say, then it justifies the current target displaying
? ? << n <formula1>∨<formula2> k ∨I
and moves on to the next problem.
If neither are available it displays:
n ? ? << n+1 <formula1> ? n+2 ? ? n+3 <formula2> ? n+4 ? ? n+5 <formula1>∨<formula2> k ∨I
The idea here is that you derive one of these and edit out the other one; you do not have to choose at this point which one you wish to prove. (If you are completely confident as to which you will prove, edit out the other straight away and click ∨I a second time.)
This Tactic can be employed with a selected disjunct formula, from among the facts, and any current target, thus
k <left-formula>∨<right-formula> Selected! ? <perhaps other lines of proof> ? ? ? << n <target> ?
It displays all or part of:
n
<left-formula> Ass n+1
? ?<< n+2
<target> ? n+3
<right-formula> ? n+4
? ? n+5
<target> ? n+6 <target> k, n+2, n+5 ∨E
It checks the facts. If <target> is available at the first stage, then lines n+1 and n+2 are omitted. If <target> is available at the second stage, then lines n+4 and n+5 are omitted.
This Tactic can be employed when the current target has the form <left-formula>⊃<right-formula> , thus
? ? << n <left-formula>⊃<right-formula> ?
It displays all or part of
n
<left-formula> Ass n+1
? ? n+2
<right-formula> ? n+5 <left-formula>⊃<right-formula> n+2 ⊃I
It checks the facts. If <right-formula> is available, then lines n+1 and n+2 are omitted (and the line numbers adjusted).
This behaves the same as the Rules.
This Tactic can be employed when the current target has the form <left-formula>≡<rightformula>, thus
? ? << n <left-formula>≡<rightformula> ?
It displays all or part of:
n
<left-formula> Ass n+1
? ?<< n+2
<right-formula> ? n+3
<right-formula> ? n+4
? ? n+5
<left-formula> ? n+6 <left-formula>≡<rightformula> n+2, n+5 ≡I
It checks the facts. If <right-formula> is available at the first stage, then lines n+1 and n+2 are omitted. If <left-formula> is available at the second stage, then lines n+4 and n+5 are omitted.
This behaves the same as the Rules.
This Tactic can be employed when the current target has the form (∀<variable>)<scope>, and <constant>does not occur in the assumptions of the target line, thus
? ? << n (∀<variable>)<scope> ? <constant> is not free in the assumptions of line n
It asks you which constant you wish to use, then displays:
n ? ? << n+1 <<scope>[<constant>/<variable>]> ? n+2 (∀<variable>)<scope> n+1 UG
It checks the facts. If <<scope>[<constant>/<variable>]> is available, then lines n and n+1 are omitted.
This behaves the same as the Rules.
This Tactic can be employed when the current target has the form (∃<variable>)<scope> , thus
? ? << n (∃<variable>)<scope> ?
You will be asked which <constant> was generalized on.
It checks the facts. If <scope> [<constant>/<variable>] is available, say at line k, then it justifies the current target displaying
n (∃<variable>)<scope> k EG
and moves on to the next problem.
If <scope> [<constant>/<variable>] is not available it displays:
? ? << n <scope> [<constant>/<variable>] ? ? ? (∃<variable>)<scope> ?
The idea here is that you may not know which term was generalized on; you can make a guess and, perhaps, edit out later and make another guess... When you are able to derive <scope> [<constant/<variable>] you merely have to use the Tactic for EG again to complete this step. (This is similar to the Tactic for ∨I.)
This Tactic can be employed with a selected existential formula (∃<variable>)<scope>, from among the facts, say at line k, and any current target, thus
k (∃<variable>)<scope> Selected! ? <perhaps other lines of proof> ? ? ? << n <target> ?
It will pick a new (suitable) constant for you.
It displays all or part of:
n
<scope>[<new constant>/<variable>] Ass n+1
? ?<< n+2
<target> ? n+3 <target> k, n+2 EI
It checks the facts. If <target> is available, then lines n+1 and n+2 are omitted.