. 62
( 107 .)


Section 18.4. Here we will simply illustrate it.
Consider the following argument:

∃x ∃y (Tet(x) § Dodec(y) § ∀z (z = x ∨ z = y))
¬∃x Cube(x)

This argument is clearly valid, in the sense that in any world in which the
premise is true, the conclusion will be true as well. But the conclusion is
certainly not a ¬rst-order consequence of the premise. (Why?) If we treat
the four basic shape axioms as additional premises, though, we can prove the
conclusion using just the ¬rst-order methods of proof available to us.

Proof: By the explicit premise, we know there are blocks e and f
such that e is a tetrahedron, f is a dodecahedron, and everything
is one of these two blocks. Toward a contradiction, suppose there
were a cube, say c. Then either c = e or c = f . If c = e then by
the indiscernibility of identicals, c is both a cube and a tetrahedron,
contradicting axiom 1. Similarly, if c = f then c is both a cube and
a dodecahedron, contradicting axiom 3. So we have a contradiction
in either case, showing that our assumption cannot be true.

While our four axioms are complete if we restrict attention to the three
shape predicates, they are clearly not complete when we consider sentences
involving SameShape. If we were to give inference rules for this predicate, it
would be natural to state them in the form of introduction and elimination
rules: the former specifying when we can conclude that two blocks are the
same shape; the latter specifying what we can infer from such a fact. This
suggests the following axioms:

SameShape Introduction Axioms:

5. ∀x ∀y ((Cube(x) § Cube(y)) ’ SameShape(x, y))

6. ∀x ∀y ((Dodec(x) § Dodec(y)) ’ SameShape(x, y))

7. ∀x ∀y ((Tet(x) § Tet(y)) ’ SameShape(x, y))

Section 12.5
340 / Methods of Proof for Quantifiers

SameShape Elimination Axioms:

8. ∀x ∀y ((SameShape(x, y) § Cube(x)) ’ Cube(y))

9. ∀x ∀y ((SameShape(x, y) § Dodec(x)) ’ Dodec(y))

10. ∀x ∀y ((SameShape(x, y) § Tet(x)) ’ Tet(y))

As it happens, these ten axioms give us a complete axiomatization of the
shape predicates in our blocks language. This means that any argument that
is valid and which uses only these predicates can be turned into one where the
conclusion is a ¬rst-order consequence of the premises plus these ten axioms.
It also means that any sentence that is true simply in virtue of the meanings
of the four shape predicates is a ¬rst-order consequence of these axioms. For
example, the sentence ∀x SameShape(x, x), which we considered as a possible
axiom in Chapter 10, follows from our ten axioms:

Proof: Let b be an arbitrary block. By axiom 4, we know that b
is a tetrahedron, a dodecahedron, or a cube. If b is a tetrahedron,
then axiom 7 guarantees that b is the same shape as b. If b is a
dodecahedron or a cube, this same conclusion follows from axioms 6
or 5, respectively. Consequently, we know that b is the same shape
as b. Since b was arbitrary, we can conclude that every block is the
same shape as itself.

During the course of this book, we have proven many claims about natural
numbers, and asked you to prove some as well. You may have noticed that
these proofs did not appeal to explicit premises. Rather, the proofs freely cited
any obvious facts about the natural numbers. However, we could (and will)
make the needed assumptions explicit by means of the axiomatic method.
In Section 16.4, we will discuss the standard Peano axioms that are used to
Peano axioms
axiomatize the obvious truths of arithmetic. While we will not do so, it would
be possible to take each of our proofs about natural numbers and turn it into
a proof that used only these Peano Axioms as premises.
We will later show, however, that the Peano Axioms are not complete, and
that it is in fact impossible to present ¬rst-order axioms that are complete for
G¨del™s Incompleteness
Theorem arithmetic. This is the famous G¨del Incompleteness Theorem and is discussed
in the ¬nal section of this book.

Chapter 12
Axiomatizing shape / 341


Give informal proofs of the following arguments, if they are valid, making use of any of the ten shape
axioms as needed, so that your proof uses only ¬rst-order methods of proof. Be very explicit about which
axioms you are using at various steps. If the argument is not valid, use Tarski™s World to provide a

12.30 12.31
∃x (¬Cube(x) § ¬Dodec(x)) ∀x (Cube(x) ’ SameShape(x, c))
‚| ‚|
∃x ∀y SameShape(x, y)
∀x Tet(x)

12.32 12.33
∀x Cube(x) ∨ ∀x Tet(x) ∨ ∀x Dodec(x) ∀x ∀y SameShape(x, y)
‚| ‚|
∀x ∀y SameShape(x, y) ∀x Cube(x) ∨ ∀x Tet(x) ∨ ∀x Dodec(x)

12.34 12.35
SameShape(b, c) SameShape(b, c)
‚| ‚| SameShape(c, d)
SameShape(c, b)
SameShape(b, d)

12.36 The last six shape axioms are quite intuitive and easy to remember, but we could have gotten
 by with fewer. In fact, there is a single sentence that completely captures the meaning of
SameShape, given the ¬rst four axioms. This is the sentence that says that two things are the
same shape if and only if they are both cubes, both tetrahedra, or both dodecahedra:
∀x ∀y (SameShape(x, y) ” ((Cube(x) § Cube(y))
∨(Tet(x) § Tet(y))
∨(Dodec(x) § Dodec(y)))

Use this axiom and and the basic shape axioms (1)-(4) to give informal proofs of axioms (5)
and (8).

12.37 Let us imagine adding as new atomic sentences involving a binary predicate MoreSides. We
 assume that MoreSides(b, c) holds if block b has more sides that block c. See if you can come
up with axioms that completely capture the meaning of this predicate. The natural way to do
this involves two or three introduction axioms and three or four elimination axioms. Turn in
your axioms to your instructor.

12.38 Find ¬rst-order axioms for the six size predicates of the blocks language. [Hint: use the axiom-
 atization of shape to guide you.]

Section 12.5
Chapter 13

Formal Proofs and Quanti¬ers

Now that we have learned the basic informal methods of proof for quanti¬ers,
we turn to the task of giving formal rules that correspond to them. Again, we
can to do this by having two rules for each quanti¬er, an introduction rule
and an elimination rule.
Before getting down to the rules, though, we should emphasize that formal
proofs in the system F contain only sentences, never w¬s with free variables.
This is because we want every line of a proof to make a de¬nite claim. W¬s
with free variables do not make claims, as we have noted. Some deductive
systems do allow proofs containing formulas with free variables, where such
variables are interpreted universally, but that is not how the system F works.

Section 13.1
Universal quanti¬er rules
The valid inference step of universal instantiation or elimination is easily for-
malized. Here is the schematic version of the rule:

Universal Elimination (∀ Elim):

∀x S(x)

Here x stands for any variable, c stands for any individual constant (whether
or not it has been used elsewhere in the proof), and S(c) stands for the result
of replacing free occurrences of x in S(x) with c.
Next, let us formalize the more interesting methods of general conditional
proof and universal generalization. This requires that we decide how to rep-
resent the fact that a constant symbol, say c, has been introduced to stand
for an arbitrary object satisfying some condition, say P(c). We indicate this
by means of a subproof with assumption P(c), insisting that the constant c in
question occur only within that subproof. This will guarantee, for example,
that the constant does not appear in the premises of the overall proof.

Universal quantifier rules / 343

To remind ourselves of this crucial restriction, we will introduce a new
graphical device, boxing the constant symbol in question and putting it in boxed constant
front of the assumption. We will think of the boxed constant as the formal
analog of the English phrase “Let c denote an arbitrary object satisfying P(c).”

General Conditional Proof (∀ Intro):

c P(c)

Where c does not occur out-
. side the subproof where it is
∀x (P(x) ’ Q(x))

When we give the justi¬cation for universal introduction, we will cite the
subproof, as we do in the case of conditional introduction. The requirement
that c not occur outside the subproof in which it is introduced does not pre-
clude it occurring within subproofs of that subproof. A sentence in a subproof
of a subproof still counts as a sentence of the larger subproof.
As a special case of ∀ Intro we allow a subproof where there is no sentential
assumption at all, just the boxed constant on its own. This corresponds to
the method of universal generalization discussed earlier, where one assumes
that the constant in question stands for an arbitrary object in the domain of

Universal Introduction (∀ Intro):


Where c does not occur out-
. side the subproof where it is
∀x P(x)

As we have indicated, we don™t really need both forms of ∀ Intro. Either
form could be eliminated in favor of the other. We use both because the ¬rst
is more natural while the second is more often used in logic textbooks (and
so something to be familiar with if you go on to study more logic).

Section 13.1
344 / Formal Proofs and Quantifiers

Let™s illustrate how to use these rules by giving a formal proof mirroring
the informal proof given on page 326. We prove that the following argument
is valid:

∀x (P(x) ’ Q(x))
∀z (Q(z) ’ R(z))
∀x (P(x) ’ R(x))

(This is a general form of the argument about all math majors being smart
given earlier.) Here is a completed proof:

1. ∀x (P(x) ’ Q(x))
2. ∀z (Q(z) ’ R(z))

3. d P(d)

4. P(d) ’ Q(d) ∀ Elim: 1
5. Q(d) ’ Elim: 3, 4
6. Q(d) ’ R(d) ∀ Elim: 2
7. R(d) ’ Elim: 5, 6
8. ∀x (P(x) ’ R(x)) ∀ Intro: 3-7

Notice that the constant symbol d does not appear outside the subproof. It is
newly introduced at the beginning of that subproof, and occurs nowhere else
outside it. That is what allows the introduction of the universal quanti¬er in
the ¬nal step.


. 62
( 107 .)