ble ¬nding an informal proof. Or suppose you can™t see how your informal

proof can be converted into a proof that uses just the rules of F. The second

strategy is helpful in either of these cases. It is known as “working backwards.” working backwards

What you do is look at the conclusion and see what additional sentence or

sentences would allow you to infer that conclusion. Then you simply insert

these steps into your proof, not worrying about exactly how they will be jus-

ti¬ed, and cite them in support of your goal sentence. You then take these

intermediate steps as new goals and see if you can prove them. Once you do,

your proof will be complete.

Let™s work through an example that applies both of these strategies. Sup-

pose you are asked to give a formal proof of the argument:

Section 6.5

168 / Formal Proofs and Boolean Logic

¬P ∨ ¬Q

¬(P § Q)

You™ll recognize this as an application of one of the DeMorgan laws, so you

know it™s valid. But when you think about it (applying our maxim) you may

¬nd that what convinces you of its validity is the following observation, which

is hard to formalize: if the premise is true, then either P or Q is false, and

that will make P § Q false, and hence the conclusion true. Though this is

a completely convincing argument, it is not immediately clear how it would

translate into the introduction and elimination rules of F .

Let™s try working backwards to see if we can come up with an informal

proof that is easier to formalize. Since the conclusion is a negation, we could

prove it by assuming P § Q and deriving a contradiction. So let™s suppose

P § Q and take ⊥ as our new goal. Now things look a little clearer. For the

premise tells us that either ¬P or ¬Q is true, but either of these cases directly

contradicts one of the conjuncts of our assumption. So proof by cases will

allow us to derive a contradiction. For the record, here is how we would state

this as an informal proof:

Proof: We are given ¬P ∨ ¬Q and want to prove ¬(P § Q). For pur-

poses of reductio, we will assume P § Q and attempt to derive a con-

tradiction. There are two cases to consider, since we are given that

either ¬P or ¬Q is true. But each of these contradicts the assump-

tion P § Q: ¬P contradicts the ¬rst conjunct and ¬Q contradicts the

second. Consequently, our assumption leads to a contradiction, and

so our proof is complete.

In the following, we lead you through the construction of a formal proof

that models this informal reasoning.

You try it

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

1. Open the ¬le Strategy 1. Begin by entering the desired conclusion in a new

step of the proof. We will construct the proof working backwards, just

like we found our informal proof. Add a step before the conclusion you™ve

entered so that your proof looks something like this:

1. ¬P ∨ ¬Q

2. . . . Rule?

3. ¬(P § Q) Rule?

Chapter 6

Strategy and tactics / 169

2. The main method used in our informal proof was reductio, which corre-

sponds to negation introduction. So change the blank step into a subproof

with the assumption P § Q and the contradiction symbol at the bottom.

Also add a step in between these to remind you that that™s where you still

need to ¬ll things in, and enter your justi¬cation for the ¬nal step, so you

remember why you added the subproof. At this point your proof should

look roughly like this:

1. ¬P ∨ ¬Q

2. P § Q

3. . . . Rule?

4. ⊥ Rule?

5. ¬(P § Q) ¬ Intro: 2“4

3. Our informal proof showed that there was a contradiction whichever of ¬P

or ¬Q was the case. The formal counterpart of proof by cases is disjunction

elimination, so the next step is to ¬ll in two subproofs, one assuming ¬P,

the other assuming ¬Q, and both concluding with ⊥. Make sure you put

in the justi¬cation for the step where you apply ∨ Elim, and it™s a good

idea to add empty steps to remind yourself where you need to continue

working. Here™s what your proof should look like now:

1. ¬P ∨ ¬Q

2. P § Q

3. ¬P

4. . . . Rule?

5. ⊥ Rule?

6. ¬Q

7. . . . Rule?

8. ⊥ Rule?

9. ⊥ ∨ Elim: 1, 3“5, 6“8

10. ¬(P § Q) ¬ Intro: 2“9

4. Filling in the remaining steps is easy. Finish your proof as follows:

Section 6.5

170 / Formal Proofs and Boolean Logic

1. ¬P ∨ ¬Q

2. P § Q

3. ¬P

4. P § Elim: 2

5. ⊥ ⊥ Intro: 4, 3

6. ¬Q

7. Q § Elim: 2

8. ⊥ ⊥ Intro: 7, 6

9. ⊥ ∨ Elim: 1, 3“5, 6“8

10. ¬(P § Q) ¬ Intro: 2“9

5. Save your proof as Proof Strategy 1.

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

Working backwards can be a very useful technique, since it often allows

you to replace a complex goal with simpler ones or to add new assumptions

from which to reason. But you should not think that the technique can be

pitfalls of working

backwards applied mechanically, without giving it any thought. Each time you add new

intermediate goals, whether they are sentences or subproofs, it is essential

that you stop and check whether the new goals are actually reasonable. If

they don™t seem plausible, you should try something else.

Here™s a simple example of why this constant checking is so important.

Suppose you were asked to prove the sentence A ∨ C from the given sentence

(A § B) ∨ (C § D). Working backwards you might notice that if you could

prove A, from this you could infer the desired conclusion by the rule ∨ Intro.

Sketched in, your partial proof would look like this:

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

2. A Rule?

3. A ∨ C ∨ Intro

The problem with this is that A does not follow from the given sentence,

and no amount of work will allow you to prove that it does. If you didn™t no-

tice this from the outset, you could spend a lot of time trying to construct an

impossible proof! But if you notice it, you can try a more promising approach.

(In this case, disjunction elimination is clearly the right way to go.) Work-

ing backwards, though a valuable tactic, is no replacement for good honest

thinking.

Chapter 6

Strategy and tactics / 171

When you™re constructing a formal proof in Fitch, you can avoid trying

to prove an incorrect intermediate conclusion by checking the step with Taut

Con. In the above example, for instance, if you use Taut Con at the second checking with Con

mechanisms

step, citing the premise as support, you would immediately ¬nd that it is

hopeless to try to prove A from the given premise.

Many of the problems in this book ask you to determine whether an argu-

ment is valid and to back up your answer with either a proof of consequence

or a counterexample, a proof of non-consequence. You will approach these

problems in much the same way we™ve described, ¬rst trying to understand

the claims involved and deciding whether the conclusion follows from the

premises. If you think the conclusion does not follow, or really don™t have a

good hunch one way or the other, try to ¬nd a counterexample. You may

succeed, in which case you will have shown the argument to be invalid. If you

cannot ¬nd a counterexample, trying to ¬nd one often gives rise to insights

about why the argument is valid, insights that can help you ¬nd the required

proof.

We can summarize our strategy advice with a seven step procedure for

approaching problems of this sort.

Remember

In assessing the validity of an argument, use the following method:

1. Understand what the sentences are saying.

2. Decide whether you think the conclusion follows from the premises.

3. If you think it does not follow, or are not sure, try to ¬nd a counterex-

ample.

4. If you think it does follow, try to give an informal proof.

5. If a formal proof is called for, use the informal proof to guide you in

¬nding one.

6. In giving consequence proofs, both formal and informal, don™t forget

the tactic of working backwards.

7. In working backwards, though, always check that your intermediate

goals are consequences of the available information.

One ¬nal warning: One of the nice things about Fitch is that it will give

you instant feedback about whether your proof is correct. This is a valuable

Section 6.5

172 / Formal Proofs and Boolean Logic

learning tool, but it can be misused. You should not use Fitch as a crutch,

using Fitch as a crutch

trying out rule applications and letting Fitch tell you if they are correct. If

you do this, then you are not really learning the system F . One way to check

up on yourself is to write a formal proof out on paper every now and then. If

you try this and ¬nd you can™t do it without Fitch™s help, then you are using

Fitch as a crutch, not a learning tool.

Exercises

6.21 If you skipped the You try it section, go back and do it now. Submit the ¬le Proof Strategy 1.

‚

6.22 6.23

Give a formal proof mirroring the in- Give an informal proof that might have

‚

formal proof on page 136 of ¬(b = c) been used by the authors in construct-

from the premises Cube(c) ∨ Dodec(c) ing the formal proof shown on page 165.

and Tet(b). You may apply Ana Con

to literals in establishing ⊥.

In each of the following exercises, give an informal proof of the validity of the indicated argument. (You

should never use the principle you are proving in your informal proof, for example in Exercise 6.24,

you should not use DeMorgan in your informal proof.) Then use Fitch to construct a formal proof that

mirrors your informal proof as much as possible. Turn in your informal proofs to your instructor and

submit the formal proof in the usual way.

6.24 6.25

¬(A ∨ B) ¬A § ¬B

‚| ‚|

¬A § ¬B ¬(A ∨ B)

6.26 6.27

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

‚| ‚|

¬B ∨ ¬C ∨ D (B § C) ∨ (D § E)

A∨D C ∨ (A § E)

In each of the following exercises, you should assess whether the argument is valid. If it is, use Fitch to

construct a formal proof. You may use Ana Con but only involving literals and ⊥. If it is not valid,

use Tarski™s World to construct a counterexample.

6.28 6.29

Cube(c) ∨ Small(c) Larger(a, b) ∨ Larger(a, c)

‚ ‚

Dodec(c) Smaller(b, a) ∨ ¬Larger(a, c)

Small(c) Larger(a, b)

Chapter 6

Proofs without premises / 173