How do the solutions differ from the example done above, and from each
other? Here are a few more translation exercises.(4) jOSHO is a theorem of TNT. (Call the TNT-string which
expresses this "META-JOSHO".)
(5) META-jOSHO is a theorem of TNT. (Call the TNT-string
which expresses this "META-META-jOSHO".)
(6) META-META-jOSHO is a theorem of TNT.
(7) META-META-META-jOSHO is a theorem of TNT.
(etc., etc.)Example 5 shows that statements of meta-met a-TNT can be translated into
TNT-notation; example 6 does the same for meta-meta-meta-TNT, etc.
It is important to keep in mind the difference between expressing a
property, and representing it, at this point. The property of being a TNT-
theorem-number, for instance, is expressed by the formula3a:TNT-PROOF-PAIR{a,a'}Translation: "a' is a TNT-theorem-number". However, we have no
guarantee that this formula represents the notion, for we have no guarantee
that this property is primitive recursive-in fact, we have more than a
sneaking suspicion that it isn't. (This suspicion is well warranted. The
property of being a TNT -theorem-number is not primitive recursive, and
no TNT-formula can represent the property!) By contrast, the property of
being a proof-pair, by virtue of its primitive recursivity, is both expressible
and representable, by the formula already introduced.Substitution Leads to the Second Idea
The preceding discussion got us to the point where we saw how TNT can
"introspect" on the notion of TNT -theoremhood. This is the essence of the
first part of the proof. We now wish to press on to the second major idea of
the proof, by developing a notion which allows the concentration of this
introspection into a single formula. To do this, we need to look at what
happens to the Godel number of a formula when you modify the formula
structurally in a simple way. In fact, we shall consider this specific modifica-
tion:replacement of all free variables by a specific numeral.Below are shown a couple of examples of this operation in the left-hand
column, and in the right-hand column are exhibited the parallel changes in
Godel numbers.On Formally Undecidable Propositions 443