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