CHAPTER XV
Jumping out of the System
A More Powerful Formal System
ONE OF THE things which a thoughtful critic of Godel's proof might do
would be to examine its generality. Such a critic might, for example,
suspect that Godel has just cleverly taken advantage of a hidden defect in
one particular formal system, TNT. If this were the case, then perhaps a
formal system superior to TNT could be developed which would not be
subject to the Godelian trick, and Godel's Theorem would lose much of its
sting. In this Chapter we will carefully scrutinize the properties of TNT
which made it vulnerable to the arguments of last Chapter.
A natural thought is this: If the basic trouble with TNT is that it
contains a "hole"-in other words, a sentence which is undecidable, namely
G-then why not simply plug up the hole? Why not just tack G onto TNT
as a sixth axiom? Of course, by comparison to the other axioms, G is a
ridiculously huge giant, and the resulting system-TNT +G-would have a
rather comical aspect due to the disproportionateness of its axioms. Be that
as it may, adding G is a reasonable suggestion. Let us consider it done.
Now, it is to be hoped, the new system, TNT+G, is a superior formal
system-one which is not only supernatural-free, but also complete. It is
certain that TNT +G is superior to TNT in at least one respect: the string G
is no longer undecidable in this new system, since it is a theorem.
What was the vulnerability of TNT due to? The essence of its vulnera-
bility was that it was capable of expressing statements about itself-in
particular, the statement
"I Cannot Be Proven in Formal System TNT"
or, expanded a bit,
"There does not exist a natural number which forms a
TNT-proof-pair with the Godel number of this string."
Is there any reason to expect or hope that TNT +G would be invulner-
able to Godel's proof? Not really. Our new system is just as expressive as
TNT. Since Godel's proof relies primarily on the expressive power of a
formal system, we should not be surprised to see our new system succumb,
Jumping out of the System^465