. 31
( 107 .)


‚ for one another, even when they occur in the context of a larger sentence. For example, the
following inference results from two uses of double negation, each applied to a part of the whole
P § (Q ∨ ¬¬R)
¬¬P § (Q ∨ R)

How would we prove this using F, which has no substitution rule? Open the ¬le Exercise 6.8,
which contains an incomplete formal proof of this argument. As it stands, none of the proof™s
steps check out, because no rules or support steps have been cited. Provide the missing justi-
¬cations and submit the completed proof.

Evaluate each of the following arguments. If the argument is valid, use Fitch to give a formal proof using
the rules you have learned. If it not valid, use Tarski™s World to construct a counterexample world. In
the last two proofs you will need to use Ana Con to show that certain atomic sentences contradict one
another to introduce ⊥. Use Ana Con only in this way. That is, your use of Ana Con should cite
exactly two atomic sentences in support of an introduction of ⊥. If you have di¬culty with any of these
exercises, you may want to skip ahead and read Section 6.5.

6.9 6.10
Cube(b) Cube(a) ∨ Cube(b)
‚ ‚
¬(Cube(c) § Cube(b)) ¬(Cube(c) § Cube(b))
¬Cube(c) ¬Cube(c)

6.11 6.12
Dodec(e) Dodec(e)
‚ ‚
Small(e) ¬Small(e)
¬Dodec(e) ∨ Dodec(f) ∨ Small(e) ¬Dodec(e) ∨ Dodec(f) ∨ Small(e)
Dodec(f) Dodec(f)

6.13 6.14
Dodec(e) SameRow(b, f) ∨ SameRow(c, f)
‚ ‚
Large(e) ∨ SameRow(d, f)
¬Dodec(e) ∨ Dodec(f) ∨ Small(e) ¬SameRow(c, f)
FrontOf(b, f)
¬(SameRow(d, f) § Cube(f))

Chapter 6
The proper use of subproofs / 163

In the following two exercises, determine whether the sentences are consistent. If they are, use Tarski™s
World to build a world where the sentences are both true. If they are inconsistent, use Fitch to give a
proof that they are inconsistent (that is, derive ⊥ from them). You may use Ana Con in your proof,
but only applied to literals (that is, atomic sentences or negations of atomic sentences).

6.15 6.16
¬(Larger(a, b) § Larger(b, a)) Smaller(a, b) ∨ Smaller(b, a)
‚ ‚
¬SameSize(a, b) SameSize(a, b)

Section 6.4
The proper use of subproofs
Subproofs are the characteristic feature of Fitch-style deductive systems. It
is important that you understand how to use them properly, since if you are
not careful, you may “prove” things that don™t follow from your premises. For
example, the following formal proof looks like it is constructed according to
our rules, but it purports to prove that A § B follows from (B § A) ∨ (A § C),
which is clearly not right.

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

2. B § A
3. B § Elim: 2
4. A § Elim: 2
5. A § C
6. A § Elim: 5
7. A ∨ Elim: 1, 2“4, 5“6
8. A § B § Intro: 7, 3

The problem with this proof is step 8. In this step we have used step
3, a step that occurs within an earlier subproof. But it turns out that this
sort of justi¬cation”one that reaches back inside a subproof that has already
ended”is not legitimate. To understand why it™s not legitimate, we need to
think about what function subproofs play in a piece of reasoning.
A subproof typically looks something like this:

Section 6.4
164 / Formal Proofs and Boolean Logic


Subproofs begin with the introduction of a new assumption, in this exam-
ple R. The reasoning within the subproof depends on this new assumption,
assumptions by ending together with any other premises or assumptions of the parent proof. So in
subproofs our example, the derivation of S may depend on both P and R. When the
subproof ends, indicated by the end of the vertical line that ties the subproof
together, the subsequent reasoning can no longer use the subproof™s assump-
tion, or anything that depends on it. We say that the assumption has been
discharged or that the subproof has been ended.
When an assumption has been discharged, the individual steps of its sub-
proof are no longer accessible. It is only the subproof as a whole that can be
cited as justi¬cation for some later step. What this means is that in justifying
the assertion of T in our example, we could cite P, Q, and the subproof as a
whole, but we could not cite individual items in the subproof like R or S. For
these steps rely on assumptions we no longer have at our disposal. Once the
subproof has been ended, they are no longer accessible.
This, of course, is where we went wrong in step 8 of the fallacious proof
given earlier. We cited a step in a subproof that had been ended, namely,
step 3. But the sentence at that step, B, had been proven on the basis of the
assumption B § A, an assumption we only made temporarily. The assumption
is no longer in force at step 8, and so cannot be used at that point.
This injunction does not prevent you from citing, from within a subproof,
items that occur earlier outside the subproof, as long as they do not occur in
subproofs that ended before that step. For example, in the schematic proof
given above, the justi¬cation for S could well include the step that contains Q.
This observation becomes more pointed when you are working in a sub-
proof of a subproof. We have not yet seen any examples where we needed to
have subproofs within subproofs, but such examples are easy to come by. Here
is one, which is a proof of one direction of the ¬rst DeMorgan law.

Chapter 6
The proper use of subproofs / 165

1. ¬(P § Q)

2. ¬(¬P ∨ ¬Q)

3. ¬P
4. ¬P ∨ ¬Q ∨ Intro: 3
5. ⊥ ⊥ Intro: 4, 2
6. ¬¬P ¬ Intro: 3“5
7. P ¬ Elim: 6
8. ¬Q
9. ¬P ∨ ¬Q ∨ Intro: 8
10. ⊥ ⊥ Intro: 9, 2
11. ¬¬Q ¬ Intro: 8“10
12. Q ¬ Elim: 11
13. P§Q § Intro: 7, 12
14. ¬(P § Q) Reit: 1
15. ⊥ ⊥ Intro: 13, 14
16. ¬¬(¬P ∨ ¬Q) ¬ Intro: 2“15
17. ¬P ∨ ¬Q ¬ Elim: 16

Notice that the subproof 2“15 contains two subproofs, 3“5 and 8“10. In
step 5 of subproof 3“5, we cite step 2 from the parent subproof 2“15. Similarly,
in step 10 of the subproof 8“10, we cite step 2. This is legitimate since the
subproof 2“15 has not been ended by step 10. While we did not need to in
this proof, we could in fact have cited step 1 in either of the sub-subproofs.
Another thing to note about this proof is the use of the Reiteration rule at
step 14. We did not need to use Reiteration here, but did so just to illustrate
a point. When it comes to subproofs, Reiteration is like any other rule: when
you use it, you can cite steps outside of the immediate subproof, if the proofs
that contain the cited steps have not yet ended. But you cannot cite a step
inside a subproof that has already ended. For example, if we replaced the
justi¬cation for step 15 with “Reit: 10,” then our proof would no longer be
As you™ll see, most proofs in F require subproofs inside subproofs”what
we call nested subproofs. To create such a subproof in Fitch, you just choose nested subproofs
New Subproof from the Proof menu while you™re inside the ¬rst subproof.
You may already have done this by accident in constructing earlier proofs. In
the exercises that follow, you™ll have to do it on purpose.

Section 6.4
166 / Formal Proofs and Boolean Logic


—¦ In justifying a step of a subproof, you may cite any earlier step con-
tained in the main proof, or in any subproof whose assumption is still
in force. You may never cite individual steps inside a subproof that
has already ended.

—¦ Fitch enforces this automatically by not permitting the citation of
individual steps inside subproofs that have ended.


6.17 Try to recreate the following “proof” using Fitch.

1. (Tet(a) § Large(c)) ∨ (Tet(a) § Dodec(b))

2. Tet(a) § Large(c)
3. Tet(a) § Elim: 2
4. Tet(a) § Dodec(b)
5. Dodec(b) § Elim: 4
6. Tet(a) § Elim: 4
7. Tet(a) ∨ Elim: 1, 2“3, 4“6
8. Tet(a) § Dodec(b) § Intro: 7, 5

What step won™t Fitch let you perform? Why? Is the conclusion a consequence of the premise?
Discuss this example in the form of a clear English paragraph, and turn your paragraph in to
your instructor.

Use Fitch to give formal proofs for the following arguments. You will need to use subproofs within
subproofs to prove these.

6.18 6.19 6.20
‚ ‚ ‚
¬B ∨ C A∨C
A ∨ ¬¬B
A∨C A ∨ (B § C)

Chapter 6
Strategy and tactics / 167

Section 6.5
Strategy and tactics
Many students try constructing formal proofs by blindly piecing together a se-
quence of steps permitted by the introduction and elimination rules, a process
no more related to reasoning than playing solitaire. This approach occasion-
ally works, but more often than not it will fail”or at any rate, make it harder
to ¬nd a proof. In this section, we will give you some advice about how to
go about ¬nding proofs when they don™t jump right out at you. The advice
consists of two important strategies and an essential maxim.
Here is the maxim: Always keep ¬rmly in mind what the sentences in your an important maxim
proof mean! Students who pay attention to the meanings of the sentences avoid
innumerable pitfalls, among them the pitfall of trying to prove a sentence that
doesn™t really follow from the information given. Your ¬rst step in trying to
construct a proof should always be to convince yourself that the claim made
by the conclusion is a consequence of the premises. You should do this even if
the exercise tells you that the argument is valid and simply asks you to ¬nd a
proof. For in the process of understanding the sentences and recognizing the
argument™s validity, you will often get some idea how to prove it.
After you™re convinced that the argument is indeed valid, the ¬rst strategy
for ¬nding a formal proof is to try giving an informal proof, the kind you might try informal proof
use to convince a fellow classmate. Often the basic structure of your informal
reasoning can be directly formalized using the rules of F. For example, if
you ¬nd yourself using an indirect proof, then that part of the reasoning will
probably require negation introduction in F . If you use proof by cases, then
you™ll almost surely formalize the proof using disjunction elimination.


. 31
( 107 .)