<<

. 12
( 107 .)



>>

which step or steps are mistaken. This means you will never be in any doubt
about whether your formal proofs meet the standard of rigor demanded of
them. And, as a practical matter, you can make sure they are correct before
submitting them.
There are other ways in which Fitch makes life simpler, as well. One is that
Fitch is more ¬‚exible than the system F. It lets you take certain shortcuts
Fitch vs. F
that are logically correct but do not, strictly speaking, fall under the rules of
F. You can always go back and expand a proof in Fitch to a formally correct
F proof, but we won™t often insist on this.
Let us now use Fitch to construct a simple formal proof. Before going on,
you will want to read the ¬rst few sections of the chapter on how to use Fitch
in the manual.


You try it
................................................................
1. We are going to use Fitch to construct the formal proof of SameRow(b, a)
from premises SameRow(a, a) and b = a. Launch Fitch and open the ¬le
Identity 1. Here we have the beginnings of the formal proof. The premises
appear above the Fitch bar. It may look slightly di¬erent from the proofs
we have in the book, since in Fitch the steps don™t have to be numbered,
for reasons we™ll soon ¬nd out. (If you would like to have numbered steps,
you can choose Show Step Numbers from the Proof menu. But don™t
try this yet.)

2. Before we start to construct the proof, notice that at the bottom of the
proof window there is a separate pane called the “goal strip,” contain-
ing the goal of the proof. In this case the goal is to prove the sentence
SameRow(b, a). If we successfully satisfy this goal, we will be able to get
Fitch to put a checkmark to the right of the goal.

3. Let™s construct the proof. What we need to do is ¬ll in the steps needed
to complete the proof, just as we did at the end of the last section. Add



Chapter 2
Constructing proofs in Fitch / 59



a new step to the proof by choosing Add Step After from the Proof
menu. In the new step, enter the sentence a = b, either by typing it in or
by using the toolbar at the top of the proof window. We will ¬rst use this
step to get our conclusion and then go back and prove this step.

4. Once you have entered a = b, add another step below this and enter the
goal sentence SameRow(b, a). Use the mouse to click on the word Rule?
that appears to the right of SameRow(b, a). In the menu that pops up, go
to the Elimination Rules and select =. If you did this right, the rule name
should now say = Elim. If not, try again.

5. Next cite the ¬rst premise and the intermediate sentence you ¬rst entered.
You do this in Fitch by clicking on the two sentences, in either order. If
you click on the wrong one, just click again and it will be un-cited. Once
you have the right sentences cited, choose Verify Proof from the Proof
menu. The last step should now check out, as it is a valid instance of =
Elim. The step containing a = b will not check out, since we haven™t yet
indicated what it follows from. Nor will the goal check out, since we don™t
yet have a complete proof of SameRow(b, a). All in good time.

6. Now add a step before the ¬rst introduced step (the one containing a = b),
and enter the sentence b = b. Do this by moving the focus slider (the
triangle in the left margin) to the step containing a = b and choosing
Add Step Before from the Proof menu. (If the new step appears in
the wrong place, choose Delete Step from the Proof menu.) Enter the
sentence b = b and justify it by using the rule = Intro. Check the step.

7. Finally, justify the step containing a = b by using the = Elim rule. You
will need to move the focus slider to this step, and then cite the second
premise and the sentence b = b. Now the whole proof, including the goal,
should check out. To ¬nd out if it does, choose Verify Proof from the
Proof menu. The proof should look like the completed proof on page 57,
except for the absence of numbers on the steps. (Try out Show Step
Numbers from the Proof menu now. The highlighting on support steps
will go away and numbers will appear, just like in the book.)

8. We mentioned earlier that Fitch lets you take some shortcuts, allowing
you to do things in one step that would take several if we adhered strictly
to F . This proof is a case in point. We have constructed a proof that falls
under F but Fitch actually has symmetry of identity built into = Elim.
So we could prove the conclusion directly from the two premises, using a
single application of the rule = Elim. We™ll do this next.




Section 2.4
60 / The Logic of Atomic Sentences




9. Add another step at the very end of your proof. Here™s a trick you will ¬nd
handy: Click on the goal sentence at the very bottom of the window. This
puts the focus on the goal sentence. Choose Copy from the Edit menu,
and then click back on the empty step at the end of your proof. Choose
Paste from the Edit menu and the goal sentence will be entered into this
step. This time, justify the new step using = Elim and citing just the two
premises. You will see that the step checks out.

10. Save your proof as Proof Identity 1.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations
Since the proof system F does not have any rules for atomic predicates
other than identity, neither does Fitch. However, Fitch does have a mecha-
nism that, among other things, lets you check for consequences among atomic
sentences that involve many of the predicates in the blocks world language.1
This is a rule we call Analytic Consequence or Ana Con for short. Ana
Analytic Consequence
Con is not restricted to atomic sentences, but that is the only application
of the rule we will discuss at the moment. This rule allows you to cite some
sentences in support of a claim if any world that makes the cited sentences
true also makes the conclusion true, given the meaning of the predicates as
used in Tarski™s World. Let™s get a feeling for Ana Con with some examples.


You try it
................................................................
1. Use Fitch to open the ¬le Ana Con 1. In this ¬le you will ¬nd nine premises
followed by six conclusions that are consequences of these premises. Indeed,
each of the conclusions follows from three or fewer of the premises.

2. Position the focus slider (the little triangle) at the ¬rst conclusion following
the Fitch bar, SameShape(c, b). We have invoked the rule Ana Con but
we have not cited any sentences. This conclusion follows from Cube(b) and
Cube(c). Cite these sentences and check the step.

3. Now move the focus slider to the step containing SameRow(b, a). Since
the relation of being in the same row is symmetric and transitive, this
follows from SameRow(b, c) and SameRow(a, c). Cite these two sentences
and check the step.
1 This mechanism does not handle the predicates Adjoins and Between, due to the com-
plexity of the ways the meanings of these predicates interact with the others.




Chapter 2
Constructing proofs in Fitch / 61




4. The third conclusion, BackOf(e, c), follows from three of the premises. See
if you can ¬nd them. Cite them. If you get it wrong, Fitch will give you
an X when you try to check the step.

5. Now ¬ll in the citations needed to make the fourth and ¬fth conclusions
check out. For these, you will have to invoke the Ana Con rule yourself.
(You will ¬nd the rule on the Con submenu of the Rule? popup.)

6. The ¬nal conclusion, SameCol(b, b), does not require that any premises be
cited in support. It is simply an analytic truth, that is, true in virtue of
its meaning. Specify the rule and check this step.

7. When you are done, choose Verify Proof to see that all the goals check
out. Save your work as Proof Ana Con 1.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations
The Ana Con mechanism is not really a rule, technically speaking, though rules vs. Con
mechanisms
we will continue to call it that since it appears on the Rule? menu in Fitch.
This mechanism, along with the two others appearing on the Con submenu,
apply complicated procedures to see whether the sentence in question follows
from the cited sentences. As we will explain later, these three items try to ¬nd
proofs of the sentence in question “behind the scenes,” and then give you a
checkmark if they succeed. The proof they ¬nd may in fact apply many, many
di¬erent rules in getting from the cited steps to the target sentence.
The main di¬erence you will run into between the genuine rules in Fitch
and the mechanisms appearing on the Con menu is that the latter “rules”
will sometimes fail even though your step is actually correct. With the genuine
rules, Fitch will always give your step either a checkmark or an X, depending
on whether the rule is applied correctly. But with the Con mechanisms, Fitch
will sometimes try to ¬nd a proof of the target sentence but fail. In these
cases, Fitch will give the step a question mark rather than a check or an X,
since there might be a complicated proof that it just couldn™t ¬nd.
To mark the di¬erence between the genuine rules of F and the three con-
sequence mechanisms, Fitch displays the rule names in green and the conse-
quence mechanisms in blue. Because the Con mechanisms look for a proof
behind the scenes, we will often ask you not to use them in giving solutions to
homework problems. After all, the point is not to have Fitch do your home-
work for you! In the following problems, you should only use the Ana Con
rule if we explicitly say you can. To see whether a problem allows you to use
any of the Con mechanisms, double click on the goal or choose See Goal
Constraints from the Goal menu.



Section 2.4
62 / The Logic of Atomic Sentences



Remember

The deductive system you will be learning is a Fitch-style deductive sys-
tem, named F. The computer application that assists you in constructing
proofs in F is therefore called Fitch. If you write out your proofs on paper,
you are using the system F, but not the program Fitch.



Exercises


2.15 If you skipped the You try it sections, go back and do them now. Submit the ¬les Proof
‚ Identity 1 and Proof Ana Con 1.

2.16 Use Fitch to give a formal version of the informal proof you gave in Exercise 2.5. Remember,
‚ you will ¬nd the problem setup in the ¬le Exercise 2.16. You should begin your proof from this
saved ¬le. Save your completed proof as Proof 2.16.

In the following exercises, use Fitch to construct a formal proof that the conclusion is a consequence of
the premises. Remember, begin your proof by opening the corresponding ¬le, Exercise 2.x, and save your
solution as Proof 2.x. We™re going to stop reminding you.

2.17 2.18
SameCol(a, b) Between(a, d, b)
‚ ‚
b=c a=c
c=d e=b
SameCol(a, d) Between(c, d, e)

2.19 2.20
Smaller(a, b) RightOf(b, c)
‚ ‚
Smaller(b, c) LeftOf(d, e)
b=d
Smaller(a, c)
LeftOf(c, e)
You will need to use Ana Con in this
Make your proof parallel the informal
proof. This proof shows that the pred-
proof we gave on page 52, using both
icate Smaller in the blocks language is
an identity rule and Ana Con (where
transitive.
necessary).




Chapter 2
Demonstrating nonconsequence / 63



Section 2.5
Demonstrating nonconsequence
Proofs come in a variety of di¬erent forms. When a mathematician proves
a theorem, or when a prosecutor proves a defendant™s guilt, they are show-
ing that a particular claim follows from certain accepted information, the
information they take as given. This kind of proof is what we call a proof of proofs of
consequence
consequence, a proof that a particular piece of information must be true if the
given information, the premises of the argument, are correct.
A very di¬erent, but equally important kind of proof is a proof of nonconse- proofs of
nonconsequence
quence. When a defense attorney shows that the crime might have been com-
mitted by someone other than the client, say by the butler, the attorney is
trying to prove that the client™s guilt does not follow from the evidence in the
case. When mathematicians show that the parallel postulate is not a conse-
quence of the other axioms of Euclidean geometry, they are doing the same
thing: they are showing that it would be possible for the claim in question (the
parallel postulate) to be false, even if the other information (the remaining
axioms) is true.
We have introduced a few methods for demonstrating the validity of an
argument, for showing that its conclusion is a consequence of its premises. We
will be returning to this topic repeatedly in the chapters that follow, adding
new tools for demonstrating consequence as we add new expressions to our

<<

. 12
( 107 .)



>>