11/16/06
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. On rare occasions it is useful (consider how Fx,Ga ∴ (∀x)Ga is proved-- the problem here is that x is free in an assumption, although not in one that is actually used, and this excludes the use of Universal Generalization; the derivation is done by proving Ga ∴ (∀x)Ga and adding the assumption Fx last.)
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 can be configured to use the propositional constant Absurd (this is the usual configuration for beginning logicians).
With Absurd in use, 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
Absurd n+2,n+4 AbsI n+6 ∼<formula> n+5 ∼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).
If Absurd is not in use, 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).
There are two forms to this.
If there is a formula, starting with a double negation, among the body of the proof, and the User selects it, this tactic acts exactly like the standard rule (ie it removes the double negation).
If no formula or line is selected, and yet ∼E is chosen off the Rules Menu, this tactic acts as a problem reducing tactic and lays out the derivation as though the User had proved the last line by ∼E.
So the transformation is:
before the tactic ∼E
? ? << n <formula> ?
after the tactic ∼E
? ? << n ∼∼<formula> ? n+1 <formula> n ∼E
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 <variable>is not free in the assumptions of the target line, thus
? ? << n (∀<variable>)<scope> ? <variable> is not free in the assumptions of line n
If displays:
n ? ? << n+1 <scope> ? n+2 (∀<variable>)<scope> n+1 UG
It checks the facts. If <scope> is available, then lines n and n+1 are omitted.
This behaves the same as the Rules.
This Tactic can be employed when both the current target has the form (∃<variable>)<scope> , thus
? ? << n (∃<variable>)<scope> ?
You will be asked which <term> was generalized on and, provided the <variable> is free for the <term> in the <scope>, matters will proceed.
It checks the facts. If <scope> [<term>/<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> [<term>/<variable>] is not available it displays:
? ? << n <scope> [<term>/<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> [<term>/<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> ?
where the <variable> is not free either in the <target> or in the assumptions of the <target>, line n.
It displays all or part of:
n
<scope> 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.