.

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