. 32
( 107 .)


Suppose you have decided that the argument is valid, but are having trou-
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

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
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
We can summarize our strategy advice with a seven step procedure for
approaching problems of this sort.


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-

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.


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


. 32
( 107 .)