CHAPTER XIV
On Formally Undecidable
Propositions of TNT
and Related Systems
l
The Two Ideas of the "Oyster"
THIS CHAPTER'S TITLE is an adaptation of the title of Godel's famous
1931 paper-"TNT" having been substituted for "Principia Mathematica".
Godel's paper was a technical one, concentrating on making his proof
watertight and rigorous; this Chapter will be more intuitive, and in it I will
stress the two key ideas which are at the core of the proof. The first key idea
is the deep discovery that there are strings of TNT which can be interpret-
ed as speaking about other strings of TNT; in short, that TNT, as a
language, is capable of "introspection", or self-scrutiny. This is what comes
from Godel-numbering. The second key idea is that the property of self-
scrutiny can be entirely concentrated into a single string; thus that string's
sole focus of attention is itself. This "focusing trick" is traceable, in essence,
to the Cantor diagonal method.
In my opinion, if one is interested in understanding Godel's proof in a
deep way, then one must recognize that the proof, in its essence, consists of
a fusion of these two main ideas. Each of them alone is a master stroke; to
put them together took an act of genius. If I were to choose, however,
which of the two key ideas is deeper, I would unhesitatingly pick the first
one-the idea of Godel-numbering, for that idea is related to the whole
notion of what meaning and reference are, in symbol-manipulating sys-
tems. This is an idea which goes far beyond the confines of mathematical
logic, whereas the Cantor trick, rich though it is in mathematical conse-
quences, has little if any relation to issues in real life.The First Idea: Proof-PairsWithout further ado, then, let us proceed to the elaboration of the proof
itself. We have already given a fairly careful notion of what the Godel
isomorphism is about, in Chapter IX. We now shall describe a mathemati-
cal notion which allows us to translate a statement such as "The string 0=0
is a theorem of TNT" into a statement of number theory. This will involve
the notion of proof-pairs. A proof-pair is a pair of natural numbers related
in a particular way. Here is the idea:(^438) On Formally Undecidable Propositions