Exercises

2.5 2.6

(Transitivity of Identity) Give an in- Give an informal proof that the follow-

formal proof of the following argument ing argument is valid. If you proved the

using only indiscernibility of identicals. transitivity of identity by doing Exer-

Make sure you say which name is be- cise 2.5, you may use this principle; oth-

ing substituted for which, and in what erwise, use only the indiscernibility of

sentence. identicals.

b=c SameRow(a, a)

a=b a=b

b=c

a=c

SameRow(c, a)

2.7 Consider the following sentences.

1. Max and Claire are not related.

2. Nancy is Max™s mother.

3. Nancy is not Claire™s mother.

Does (3) follow from (1) and (2)? Does (2) follow from (1) and (3)? Does (1) follow from (2) and

(3)? In each case, if your answer is no, describe a possible circumstance in which the premises

are true and the conclusion false.

Given the meanings of the atomic predicates in the blocks language, assess the following arguments for

validity. (You may again assume any general facts about the worlds that can be built in Tarski™s World.)

If the argument is valid, give an informal proof of its validity and turn it in on paper to your instructor.

If the conclusion is not a consequence of the premises, submit a world in which the premises are true

and the conclusion false.

2.8 2.9 2.10

Large(a) LeftOf(a, b) SameSize(b, c)

‚| ‚| ‚|

Larger(a, c) b=c SameShape(b, c)

Small(c) RightOf(c, a) b=c

2.11 2.12 2.13

LeftOf(a, b) BackOf(a, b) SameSize(a, b)

‚| ‚| ‚|

RightOf(c, a) FrontOf(a, c) Larger(a, c)

Smaller(d, c)

LeftOf(b, c) FrontOf(b, c)

Smaller(d, b)

Section 2.2

54 / The Logic of Atomic Sentences

2.14 Between(b, a, c)

‚| LeftOf(a, c)

LeftOf(a, b)

Section 2.3

Formal proofs

In this section we will begin introducing our system for presenting formal

proofs, what is known as a “deductive system.” There are many di¬erent

deductive systems

styles of deductive systems. The system we present in the ¬rst three parts of

the book, which we will call F, is a “Fitch-style” system, so called because

the system F

Frederic Fitch ¬rst introduced this format for giving proofs. We will look at

a very di¬erent deductive system in Part IV, one known as the resolution

method, which is of considerable importance in computer science.

In the system F, a proof of a conclusion S from premises P, Q, and R, looks

very much like an argument presented in Fitch format. The main di¬erence is

that the proof displays, in addition to the conclusion S, all of the intermediate

conclusions S1 , . . . , Sn that we derive in getting from the premises to the

conclusion S:

P

Q

R

S1 Justi¬cation 1

. .

. .

. .

Sn Justi¬cation n

S Justi¬cation n+1

There are two graphical devices to notice here, the vertical and horizontal

lines. The vertical line that runs on the left of the steps draws our attention

to the fact that we have a single purported proof consisting of a sequence

of several steps. The horizontal Fitch bar indicates the division between the

claims that are assumed and those that allegedly follow from them. Thus the

fact that P, Q, and R are above the bar shows that these are the premises of

our proof, while the fact that S1 , . . . , Sn , and S are below the bar shows that

these sentences are supposed to follow logically from the premises.

Chapter 2

Formal proofs / 55

Notice that on the right of every step below the Fitch bar, we give a

justi¬cation of the step. In our deductive system, a justi¬cation indicates justi¬cation

which rule allows us to make the step, and which earlier steps (if any) the rule

is applied to. In giving an actual formal proof, we will number the steps, so

we can refer to them in justifying later steps.

We already gave one example of a formal proof in the system F, back on

page 48. For another example, here is a formalization of our informal proof of

the symmetry of identity.

1. a = b

2. a = a = Intro

3. b = a = Elim: 2, 1

In the right hand margin of this proof you ¬nd a justi¬cation for each step

below the Fitch bar. These are applications of rules we are about to introduce.

The numbers at the right of step 3 show that this step follows from steps 2

and 1 by means of the rule cited.

The ¬rst rule we use in the above proof is Identity Introduction. This = Intro

rule allows you to introduce, for any name (or complex term) n in use in

the proof, the assertion n = n. You are allowed to do this at any step in the

proof, and need not cite any earlier step as justi¬cation. We will abbreviate

our statement of this rule in the following way:

Identity Introduction (= Intro):

n=n

We have used an additional graphical device in stating this rule. This is

the symbol . We will use it in stating rules to indicate which step is being

licensed by the rule. In this example there is only one step mentioned in the

rule, but in other examples there will be several steps.

The second rule of F is Identity Elimination. It tells us that if we have = Elim

proven a sentence containing n (which we indicate by writing P(n)) and a

sentence of the form n = m, then we are justi¬ed in asserting any sentence

which results from P(n) by replacing some or all of the occurrences of n by m.

Section 2.3

56 / The Logic of Atomic Sentences

Identity Elimination (= Elim):

P(n)

.

.

.

n=m

.

.

.

P(m)

When we apply this rule, it does not matter which of P(n) and n = m occurs

¬rst in the proof, as long as they both appear before P(m), the inferred step.

In justifying the step, we cite the name of the rule, followed by the steps in

which P(n) and n = m occur, in that order.

We could also introduce rules justi¬ed by the meanings of other predicates

besides = into the system F . For example, we could introduce a formal rule

of the following sort:

Bidirectionality of Between:

Between(a, b, c)

.

.

.

Between(a, c, b)

We don™t do this because there are just too many such rules. We could state

them for a few predicates, but certainly not all of the predicates you will

encounter in ¬rst-order languages.

There is one rule that is not technically necessary, but which will make

Reiteration

some proofs look more natural. This rule is called Reiteration, and simply

allows you to repeat an earlier step, if you so desire.

Reiteration (Reit):

P

.

.

.

P

To use the Reiteration rule, just repeat the sentence in question and, on the

right, write “Reit: x,” where x is the number of the earlier occurrence of the

sentence.

Chapter 2

Formal proofs / 57

Reiteration is obviously a valid rule of inference, since any sentence is a

logical consequence of itself. The reason for having the rule will become clear

as proofs in the system F become more complicated. For now, let™s just say

that it is like remarking, in the course of giving an informal proof, “we have

already shown that P.” This is often a helpful reminder to the person reading

the proof.

Now that we have the ¬rst three rules of F, let™s try our hand construct-

ing a formal proof. Suppose we were asked to prove SameRow(b, a) from the

premises SameRow(a, a) and b = a. We might begin by writing down the

premises and the conclusion, leaving space in between to ¬ll in the inter-

mediate steps in our proof.

1. SameRow(a, a)

2. b = a

.

.

.

?. SameRow(b, a)

It might at ¬rst seem that this proof should be a one step application of

= Elim. But notice that the way we have stated this rule requires that we

replace the ¬rst name in the identity sentence, b, for the second, a, but we

want to substitute the other way around. So we need to derive a = b as an

intermediate conclusion before we can apply = Elim.

1. SameRow(a, a)

2. b = a

.

.

.

?. a = b

?. SameRow(b, a) = Elim: 1, ?

Since we have already seen how to prove the symmetry of identity, we can

now ¬ll in all the steps of the proof. The ¬nished proof looks like this. Make

sure you understand why all the steps are there and how we arrived at them.

1. SameRow(a, a)

2. b = a

3. b = b = Intro

4. a = b = Elim: 3, 2

5. SameRow(b, a) = Elim: 1, 4

Section 2.3

58 / The Logic of Atomic Sentences

Section 2.4

Constructing proofs in Fitch

Writing out a long formal proof in complete detail, let alone reading or check-

ing it, can be a pretty tedious business. The system F makes this less painful

than many formal systems, but it™s still not easy. This book comes with a sec-

ond program, Fitch, that makes constructing formal proofs much less painful.

the program Fitch

Fitch can also check your proof, telling you whether it is correct, and if it isn™t,