1. (B § A) ∨ (A § C)

2. B § A

3. A § Elim: 2

4. A § C

5. A § Elim: 4

6. A ∨ Elim: 1, 2“3, 4“5

The citation for step 6 shows the form we use when citing subproofs. The

citation “n“m” is our way of referring to the subproof that begins on line n

and ends on line m.

Sometimes, in using disjunction elimination, you will ¬nd it natural to use

the reiteration rule introduced in Chapter 3. For example, suppose we modify

the above proof to show that A follows from (B § A) ∨ A.

1. (B § A) ∨ A

2. B § A

3. A § Elim: 2

4. A

5. A Reit: 4

6. A ∨ Elim: 1, 2“3, 4“5

Here, the assumption of the second subproof is A, exactly the sentence we

want to prove. So all we need to do is repeat that sentence to get the subproof

into the desired form. (We could also just give a subproof with one step, but

it is more natural to use reiteration in such cases.)

You try it

................................................................

1. Open the ¬le Disjunction 1. In this ¬le, you are asked to prove

Medium(c) ∨ Large(c)

from the sentence

(Cube(c) § Large(c)) ∨ Medium(c)

Section 6.2

152 / Formal Proofs and Boolean Logic

We are going to step you through the construction of the following proof:

1. (Cube(c) § Large(c)) ∨ Medium(c)

2. Cube(c) § Large(c)

3. Large(c) § Elim: 2

4. Medium(c) ∨ Large(c) ∨ Intro: 3

5. Medium(c)

6. Medium(c) ∨ Large(c) ∨ Intro: 5

7. Medium(c) ∨ Large(c) ∨ Elim: 1, 2“4, 5“6

2. To use ∨ Elim in this case, we need to get two subproofs, one for each

of the disjuncts in the premise. It is a good policy to begin by specifying

both of the necessary subproofs before doing anything else. To start a

subproof, add a new step and choose New Subproof from the Proof

menu. Fitch will indent the step and allow you to enter the sentence you

want to assume. Enter the ¬rst disjunct of the premise, Cube(c) § Large(c),

as the assumption of this subproof.

3. Rather than work on this subproof now, let™s specify the second case before

we forget what we™re trying to do. To do this, we need to end the ¬rst

subproof and start a second subproof after it. You end the current subproof

by choosing End Subproof from the Proof menu. This will give you a

new step outside of, but immediately following the subproof.

4. Start your second subproof at this new step by choosing New Subproof

from the Proof menu. This time type the other disjunct of the premise,

Medium(c). We have now speci¬ed the assumptions of the two cases we

need to consider. Our goal is to prove that the conclusion follows in both

of these cases.

5. Go back to the ¬rst subproof and add a step following the assumption. (Fo-

cus on the assumption step of the subproof and choose Add Step After

from the Proof menu.) In this step use § Elim to prove Large(c). Then

add another step to that subproof and prove the goal sentence, using ∨

Intro. In both steps, you will have to cite the necessary support sentences.

6. After you™ve ¬nished the ¬rst subproof and all the steps check out, move

the focus slider to the assumption step of the second subproof and add a

new step. Use ∨ Intro to prove the goal sentence from your assumption.

Chapter 6

Disjunction rules / 153

7. We™ve now derived the goal sentence in both of the subproofs, and so are

ready to add the ¬nal step of our proof. While focussed on the last step of

the second subproof, choose End Subproof from the Proof menu. Enter

the goal sentence into this new step.

8. Specify the rule in the ¬nal step as ∨ Elim. For support, cite the two

subproofs and the premise. Check your completed proof. If it does not

check out, compare your proof carefully with the proof displayed above.

Have you accidentally gotten one of your subproofs inside the other one?

If so, delete the misplaced subproof by focusing on the assumption and

choosing Delete Step from the Proof menu. Then try again.

9. When the entire proof checks out, save it as Proof Disjunction 1.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

Default and generous uses of the ∨ rules

There are a couple of ways in which Fitch is more lenient in checking ∨ Elim

than the strict form of the rule suggests. First, the sentence S does not have

to be the last sentence in the subproof, though usually it will be. S simply has

to appear on the “main level” of each subproof, not necessarily as the very

last step. Second, if you start with a disjunction containing more than two

disjuncts, say P ∨ Q ∨ R, Fitch doesn™t require three subproofs. If you have

one subproof starting with P and one starting with Q ∨ R, or one starting

with Q and one starting with P ∨ R, then Fitch will still be happy, as long as

you™ve proven S in each of these cases.

Both disjunction rules have default applications, though they work rather default uses of

disjunction rules

di¬erently. If you cite appropriate support for ∨ Elim (i.e., a disjunction

and subproofs for each disjunct) and then check the step without typing a

sentence, Fitch will look at the subproofs cited and, if they all end with the

same sentence, insert that sentence into the step. If you cite a sentence and

apply ∨ Intro without typing a sentence, Fitch will insert the cited sentence

followed by ∨, leaving the insertion point after the ∨ so you can type in the

rest of the disjunction you had in mind.

You try it

................................................................

1. Open the ¬le Disjunction 2. The goal is to prove the sentence

(Cube(b) § Small(b)) ∨ (Cube(b) § Large(b))

Section 6.2

154 / Formal Proofs and Boolean Logic

The required proof is almost complete, though it may not look like it.

2. Focus on each empty step in succession, checking the step so that Fitch

will ¬ll in the default sentence. On the second empty step you will have to

¬nish the sentence by typing in the second disjunct, (Cube(b) § Large(b)),

of the goal sentence. (If the last step does not generate a default, it is

because you have not typed the right thing in the ∨ Intro step.)

3. When you are ¬nished, see if the proof checks out. Do you understand the

proof? Could you have come up with it on your own?

4. Save your completed proof as Proof Disjunction 2.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

Exercises

6.1 If you skipped any of the You try it sections, go back and do them now. Submit the ¬les Proof

‚ Conjunction 1, Proof Conjunction 2, Proof Conjunction 3, Proof Conjunction 4, Proof Disjunction

1, and Proof Disjunction 2.

6.2 Open the ¬le Exercise 6.2, which contains an incomplete formal proof. As it stands, none of

‚ the steps check out, either because no rule has been speci¬ed, no support steps cited, or no

sentence typed in. Provide the missing pieces and submit the completed proof.

Use Fitch to construct formal proofs for the following arguments. You will ¬nd Exercise ¬les for each

argument in the usual place. As usual, name your solutions Proof 6.x.

6.3 6.4

a= b§b = c§c = d (A § B) ∨ C

‚ ‚

a= c§b = d C∨B

6.5 6.6

A § (B ∨ C) (A § B) ∨ (A § C)

‚ ‚

(A § B) ∨ (A § C) A § (B ∨ C)

Section 6.3

Negation rules

Last but not least are the negation rules. It turns out that negation introduc-

tion is our most interesting and complex rule.

Chapter 6

Negation rules / 155

Negation elimination

The rule of negation elimination corresponds to a very trivial valid step, from

¬¬P to P. Schematically:

Negation Elimination (¬ Elim):

¬¬P

.

.

.

P

Negation elimination gives us one direction of the principle of double nega-

tion. You might reasonably expect that our second negation rule, negation

introduction, would simply give us the other direction. But if that™s what you

guessed, you guessed wrong.

Negation introduction

The rule of negation introduction corresponds to the method of indirect proof

or proof by contradiction. Like ∨ Elim, it involves the use of a subproof, as

will the formal analogs of all nontrivial methods of proof. The rule says that

if you can prove a contradiction ⊥ on the basis of an additional assumption

P, then you are entitled to infer ¬P from the original premises. Schematically:

Negation Introduction (¬ Intro):

P

.

.

.

⊥

¬P

There are di¬erent ways of understanding this rule, depending on how

we interpret the contradiction symbol ⊥. Some authors interpret it simply

as shorthand for any contradiction of the form Q § ¬Q. If we construed the

schema that way, we wouldn™t have to say anything more about it. But we

will treat ⊥ as a symbol in its own right, to be read “contradiction.” This

has several advantages that will become apparent when you use the rule. The

one disadvantage is that we need to have rules about this special symbol. We

introduce these rules next.

Section 6.3

156 / Formal Proofs and Boolean Logic

⊥ Introduction

The rule of ⊥ Introduction (⊥ Intro) allows us to obtain the contradiction

symbol if we have established an explicit contradiction in the form of some

sentence P and its negation ¬P.

⊥ Introduction (⊥ Intro):

P

.

.

.

¬P

.

.

.

⊥

Ordinarily, you will only apply ⊥ Intro in the context of a subproof, to

show that the subproof™s assumption leads to a contradiction. The only time

you will be able to derive ⊥ in your main proof (as opposed to a subproof) is