<<

. 39
( 107 .)



>>

.
.
P
.
.
.
Q

The corresponding introduction rule is the formal counterpart of the method
of conditional proof. As you would expect, it requires us to construct a sub-
proof. To prove a statement of the form P ’ Q we begin our subproof with
the assumption of P and try to prove Q. If we succeed, then we are allowed
to discharge the assumption and conclude our desired conditional, citing the
subproof as justi¬cation. Schematically:

Conditional Introduction (’ Intro):

P
.
.
.
Q
P’Q

Strategy and tactics

The strategy of working backwards usually works extremely well in proofs
that involve conditionals, particularly when the desired conclusion is itself a



Chapter 8
Formal rules of proof for ’ and ” / 207



conditional. Thus if the goal of a proof is to show that a conditional sentence
P ’ Q is a consequence of the given information, you should sketch in a working backwards
subproof with P as an assumption and Q as the ¬nal step. Use this subproof
as support for an application of ’ Intro. When you check your proof, Q will
become your new intermediate goal, and in proving it you can rely on the
assumption P.
Let™s work through a simple example that involves both of the rules for
the conditional and illustrates the technique of working backwards.


You try it
................................................................

1. We will step you through a formal proof of A ’ C from the premise
(A ∨ B) ’ C. Use Fitch to open the ¬le Conditional 1. Notice the premise
and the goal. Add a step to the proof and write in the goal sentence.

2. Start a subproof before the sentence A ’ C. Enter A as the assumption of
the subproof.

3. Add a second step to the subproof and enter C.

4. Move the slider to the step containing the goal sentence A ’ C. Justify
this step using the rule ’ Intro, citing the subproof for support. Check
this step.

5. Now we need to go back and ¬ll in the subproof. Add a step between the
two steps of the subproof. Enter A ∨ B. Justify this step using ∨ Intro,
citing the assumption of the subproof.

6. Now move the slider to the last step of the subproof. Justify this step using
the rule ’ Elim, citing the premise and the step you just proved.

7. Verify that your proof checks out, and save it as Proof Conditional 1.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations
Once we have conditional introduction at our disposal, we can convert
any proof with premises into the proof, without premises, of a corresponding
conditional. For example, we showed in Chapter 6 (page 156) how to give a
formal proof of ¬¬A from premise A. We can can now use the earlier proof to
build a proof of the logically true sentence A ’ ¬¬A.




Section 8.2
208 / The Logic of Conditionals




1. A

2. ¬A
3. ⊥ ⊥ Intro: 1, 2
4. ¬¬A ¬ Intro: 2“3
5. A ’ ¬¬A ’ Intro: 1“4

Notice that the subproof here is identical to the original proof given on
page 156. We simply embedded that proof in our new proof and applied con-
ditional introduction to derive A ’ ¬¬A.

Default and generous uses of the ’ rules

The rule ’ Elim does not care in which order you cite the support sentences.
The rule ’ Intro does not insist that the consequent be at the last step of
the cited subproof, though it usually is. Also, the assumption step might be
the only step in the subproof, as in a proof of a sentence of the form P ’ P.
The default applications of the conditional rules work exactly as you would
default uses of
conditional rules expect. If you cite supports of the form indicated in the rule statements, Fitch
will ¬ll in the appropriate conclusion for you.


You try it
................................................................

1. Open the ¬le Conditional 2. Click on the goal icon to see what sentence we
are trying to prove. Then focus on each step in succession and check the
step. On the empty steps, try to predict what default Fitch will supply.

2. When you are ¬nished, make sure you understand the proof. Save the
checked proof as Proof Conditional 2.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations




Chapter 8
Formal rules of proof for ’ and ” / 209



Rules for the biconditional
The rules for the biconditional are just what you would expect, given the rules
for the conditional. The elimination rule for the biconditional can be stated
schematically as follows:

Biconditional Elimination (” Elim):

P ” Q (or Q ” P)
.
.
.
P
.
.
.
Q


This means that you can conclude Q if you can establish P and either of the
biconditionals indicated.
The introduction rule for the biconditional P ” Q requires that you give
two subproofs, one showing that Q follows from P, and one showing that P
follows from Q:

Biconditional Introduction (” Intro):

P
.
.
.
Q
Q
.
.
.
P
P”Q


Here is a simple example of a proof using biconditional introduction. It
shows how to derive the double negation law within the system F .




Section 8.2
210 / The Logic of Conditionals




1. P

2. ¬P
3. ⊥ ⊥ Intro: 1, 2
4. ¬¬P ¬ Intro: 2“3
5. ¬¬P
6. P ¬ Elim: 5
7. P ” ¬¬P ” Intro: 1“4, 5“6


Strategy and tactics

When you are constructing a proof whose conclusion is a biconditional, it
is particularly important to sketch in the proof ahead of time. Add the two
required subproofs and the desired conclusion, citing the subproofs in support.
Then try to ¬ll in the subproofs. This is a good idea because these proofs
sometimes get quite long and involved. The sketch will help you remember
what you were trying to do.

You try it
................................................................
1. Open the ¬le Conditional 3. In this ¬le, you are asked to prove, without
premises, the law of contraposition:
(P ’ Q) ” (¬Q ’ ¬P)

2. Start your proof by sketching in the two subproofs that you know you™ll
have to prove, plus the desired conclusion. Your partial proof will look like
this:



1. P ’ Q
2. ¬Q ’ ¬P Rule?
3. ¬Q ’ ¬P
4. P ’ Q Rule?
5. (P ’ Q) ” (¬Q ’ ¬P) ” Intro: 1“2, 3“4



Chapter 8
Formal rules of proof for ’ and ” / 211




3. Now that you have the overall structure, start ¬lling in the ¬rst subproof.
Since the goal of that subproof is a conditional claim, sketch in a condi-
tional proof that would give you that claim:



1. P ’ Q

2. ¬Q
3. ¬P Rule?
4. ¬Q ’ ¬P ’ Intro: 2“3
5. ¬Q ’ ¬P
6. P ’ Q Rule?
7. (P ’ Q) ” (¬Q ’ ¬P) ” Intro: 1“4, 5“6

4. To derive ¬P in the subsubproof, you will need to assume P and derive a
contradiction. This is pretty straightforward:



1. P ’ Q

2. ¬Q

3. P
4. Q ’ Elim: 1, 3
5. ⊥ ⊥ Intro: 4, 2
6. ¬P ¬ Intro: 3“5
7. ¬Q ’ ¬P ’ Intro: 2“6
8. ¬Q ’ ¬P
9. P ’ Q Rule?
10. (P ’ Q) ” (¬Q ’ ¬P) ” Intro: 1“7, 8“9

5. This completes the ¬rst subproof. Luckily, you sketched in the second
subproof so you know what you want to do next. You should be able to
¬nish the second subproof on your own, since it is almost identical to the
¬rst.



Section 8.2
212 / The Logic of Conditionals




<<

. 39
( 107 .)



>>