6/11/07 Under construction
a) Learning further propositional rules of inference. Carrying out simple propositional derivations using some of the Rules of Inference.
b) Learning elementary Tactics.
Tactics will help you to do derivations.
a)
Thus far we have encountered 6 propositional rules of inference: Simplification, Conjunction, Addition, Modus Ponens, Modus Tollens, and Hypothetical Syllogism. If we write these out as forms or patterns, these are the kinds of inferences they permit.
Modus Ponens (MP)
p⊃q,
p
∴
qModus Tollens (MT)
p⊃q,
~q
∴
~pHypothetical Syllogism (HS)
p⊃q,
q⊃r
∴
p⊃rSimplication (Simp)
p.q
∴
pConjunction (Conj)
p,
q
∴
p.qAddition(Add)
p
∴
p∨q
Now we introduce the last three of these plain rules.
Disjunctive Syllogism(DS)
p∨q,
~p
∴
qConstructive Dilemma (CD)
(p⊃q).(r⊃s),
p∨r
∴
q∨sAbsorption (Abs)
p⊃q
∴
p⊃(p.q)
Here are some examples of those three rules at work (press the Proof buttons, and select Derive It from the Wizard menu).
Proof applet
Example 1 (F.H)∨(F⊃G),~(F.H) ∴ (F⊃G)
Example 2 (B.C)∨D,((B.C)⊃(Z.~A)).(D⊃M) ∴ (Z.~A)∨M
Example 3 F⊃G,G⊃H,K ∴ K.(G⊃(G.H))
b)
What is often mysterious is how skilled logicians manage to do difficult derivations. Fortunately something useful can be said about this. Heuristics-- the study of how to solve problems-- has a history that is thousands of years old. Heuristics, in its modern guise, in this context, is what we will call Tactics.
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 ∴ A.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 Simplification can be applied to this to extend the facts to A.B, C, A. Turning now to the problem. It may be a compound formula 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 A.C is a compound proposition and we can guess that the Rule Conjunction, applied to A and B separately, was used to obtain it; and thus the problem A.C is removed and A 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 Rule. For example, to extend the facts A .B, C.A, B you select a conjunction (the first one or the second one) and click on Simp.
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 Conj.. 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.
For these you do not use Derive It. You do them yourself! Select the appropriate lines, choose the rules, and do the proof. [If you are truly stuck use Next Line or Derive It.]
Each of the derivations in the following Exercise can be done using the Disjunctive Syllogism (DS), and the rules learned previously.
If a formula in a line of a derivation has the form
<formula1> ∨ <formula2>
and a formula in a line of a derivation has the form
~<formula1>
the Rule of Disjunctive Syllogism allows you to add
<formula2>
In English, if you have A or B and not-A you are entitled to B.
Show each of the following arguments to be valid.
If you are stuck, ask the program to do one line for you (choose Next Line under the Wizard Menu); then, having seen what the next line is, go to the Edit Menu click Undo Next Line and try to do it yourself.
(a) (X≡H)∨X,~(X≡H) ∴ X
(b) ~(F.H), K, (F.H)∨(K⊃G)∴ K⊃G
(c) (~M∨(N.I)).J,~M∴ N.I
Proofs
Each of the derivations in the following Exercise can be done using the Rule of Constructive Dilemma (CD), and the rules learned previously.
If a formula in a line of a derivation has the form
(<formula1> ⊃ <formula2>).(<formula3> ⊃ <formula4>)
and a formula in a line of a derivation has the form
<formula1> ∨ <formula3>
the Rule of Constructive Dilemma allows you to add
<formula2> ∨ <formula4>
This is the rule known as Constructive Dilemma. In English, if you have (If A then B)and(If C then D) and you have A or C you are entitled to B or D .
Show each of the following arguments to be valid.
a) (~(X≡Y) ⊃ ~W).((X∨Y) ⊃ V),~(X≡Y) ∨ (X∨Y)∴~W ∨ V
b) J ∨ ~K,(J ⊃ L).(~K ⊃ (M≡N)) ∴L ∨ (M≡N)
c) A ⊃ F,C⊃ G,A ∨C∴(F∨G) ∨H
(If you auto-Derive this one, you will see a long and apparently bizarre proof. We can learn from this. If there is a proof of a conclusion from some premises, there are infinitely many different proofs of the same conclusion from the same premises. (We can see this, in a trivial case, by using Conj. to 'and' a line with itself then Simp. to go back to the original line-- the result is a proof that is a perfectly good proof but is two lines longer than the original. We can do this over and over to get as many proofs as we wish. Importantly, often there are 'significantly different' proofs of the same thing. ) Given that there are many different proofs, there is the problem of finding a 'good' proof or the 'best proof'. Often the notion of a 'good' proof amounts to a short proof (certainly one without pointlesss Conj and SImp steps back to the same formula), sometimes a 'good' proof might be one with some kind of special insight into the structure of the premises and how they relate to the conclusion. The theorem prover here has found a proof which is not the shortest one (its proof also uses several rules that we have not met yet). That happens. The task of finding a proof at all is plenty difficult enough in itself, let alone the problem of finding the best proof. In this case you should be able to find a better proof than the theorem prover. Don't be too pleased with yourself, though, as the proofs get more difficult almost certainly the theorem prover will, from time to time, find better proofs than you.)
Proofs
The derivation in the following Exercise can be done using the Rule of Absorption (Abs), and the rules learned previously.
If a formula in a line of a derivation has the form
<formula1> ⊃ <formula2>
then Absorption allows you to add
<formula1> ⊃ (<formula1>.<formula2>)
This rule is an oddity. You will almost never meet it in English. Were you to do so it would suggest: if you have If A then B you are entitled to If A then (A and B). It is included with the other rules merely to ensure that the rules, as a whole, are powerful enough to permit the proof of any valid argument that starts from premises. However, there are plenty of valid arguments that have no premises at all (for example, ∴ A ∨ A is a valid argument). The nine rules we have cannot, collectively, prove these (because every rule in the nine needs premises). Shortly we will meet a different kind of rule, Conditional Proof, which does not require premises. Once we have Conditional Proof, and the Replacement Rules, which are to come, we won't really need the rule of Absorption.
a) A ⊃ B ∴ A ⊃ (A.B)
Proofs
After you have started the proof switch on 'Tactics' under the Proof Wizard menu, and do the derivations in the following way. If any of the lines you wish to obtain has a connective in it, click the appropriate 'Introduction' rule (that is, a rule that puts a connective in, eg Conjunction or Addition). If any of the lines you have obtained has a connective in it, use an 'Elimination' rule to take it out (rules like Simplification).
(a) F.H,G ∴F.G
(b) F.H,G ∴F∨K
Proofs