. 11
( 107 .)


Methods of proof / 53


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
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:

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):


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):


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
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):


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

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,


. 11
( 107 .)