<< Предыдущая стр. 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
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

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

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.
 << Предыдущая стр. 31(из 107 стр.)ОГЛАВЛЕНИЕ Следующая >>