can only make a record called "I Cannot Be Played on Record Player X"
provided that Record Player X is really a record player! The Tortoise's
method is quite insidious, as it plays on the strength, rather than on the
weakness, of the system. And therefore he requires "sufficiently hi-fi"
record players.
Ditto for formal versions of number theory. The reason that TNT is a
formalization of N'is that its symbols act the right way: that is, its theorems
are not silent like a refrigerator-they speak actual truths of N. Of course,
so do the theorems of the pq-system. Does it, too, count as "a formalization
of number theory", or is it more like a refrigerator? Well, it is a little better
than a refrigerator, but it is still pretty weak. The pq-system does not
include enough of the core truths of N to count as "a number theory".
What, then, are these "core truths" of N? They are the primitive recur-
sive truths; that means they involve only predictably terminating calculations.
These core truths serve for N as Euclid's first four postulates served for
geometry: they allow you to throw out certain candidates before the game
begins, on the grounds of "insufficient power". From here on out, the
representability of all primitive recursive truths will be the criterion for calling a
system "sufficiently powerful".Ganto's Ax in Metamathematics
The significance of the notion is shown by the following key fact: If you
have a sufficiently powerful formalization of number theory, then Godel's
method is applicable, and consequently your system is incomplete. If, on the
other hand, your system is not sufficiently powerful (i.e., not all primitive
recursive truths are theorems), then your system is, precisely by virtue of
that lack, incomplete. Here we have a reformulation of "Gant6's Ax" in
metamathematics: whatever the system does, Godel's Ax will chop its head
om Notice also how this completely parallels the high-fidelity-versus-low-
fidelity battle in the Contracrostipunctus.
Actually, it turns out that much weaker systems are still vulnerable to
the Godel method; the criterion that all primitive recursive truths need be
represented as theorems is far too stringent. It is a little like a thief who will
only rob "sufficiently rich" people, and whose criterion is that the potential
victim should be carrying at least a million dollars in cash. In the case of
TNT, luckily, we will be able to act in our capacity as thieves, for the million
in cash is there-which is to say, TNT does indeed contain all primitive
recursive truths as theorems.
Now before we plunge into a detailed discussion of primitive recursive
functions and predicates, I would like to tie the themes of this Chapter to
themes from earlier Chapters, so as to provide a bit better motivation.
Finding Order by Choosing the Right Filter
We saw at a very early stage that formal systems can be difficult and unruly
beasts because they have lengthening and shortening rules, which can
BlooP and FlooP and GlooP^407