following inference results from two uses of double negation, each applied to a part of the whole

sentence:

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)

Dodec(f)

¬(SameRow(d, f) § Cube(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

P

.

.

.

Q

R

.

.

.

S

T

.

.

.

Subproofs begin with the introduction of a new assumption, in this exam-

ple R. The reasoning within the subproof depends on this new assumption,

discharging

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

correct.

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

Remember

—¦ 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.

Exercises

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

A∨B A∨B A∨B

‚ ‚ ‚

¬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.