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

o

Theorem arithmetic. This is the famous G¨del Incompleteness Theorem and is discussed

o

in the ¬nal section of this book.

Chapter 12

Axiomatizing shape / 341

Exercises

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

counterexample.

12.30 12.31

∃x (¬Cube(x) § ¬Dodec(x)) ∀x (Cube(x) ’ SameShape(x, c))

‚| ‚|

∃x ∀y SameShape(x, y)

Cube(c)

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

.

.

.

S(c)

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.

342

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

introduced.

Q(c)

∀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

discourse.

Universal Introduction (∀ Intro):

c

Where c does not occur out-

.

.

. side the subproof where it is

introduced.

P(c)

∀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.