. 29
( 107 .)


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


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):


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):



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):


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


. 29
( 107 .)