on 17-Oct-2020 (Sat)

Rule of Specification: Suppose u is a variable which occurs inside the string x. If the string \(\forall u:x\) is a theorem, then so is x, and so are any strings made from x by replacing u, wherever it occurs, by one and the same term. (Restriction: The term which replaces u must not contain any variable that is quantified in x.)

Rule of Generalization: Suppose x is a theorem in which u, a variable, occurs free. Then \(\forall u:x\) is a theorem. (Restriction: No generalization is allowed in a fantasy on any variable which appeared free in the fantasy's premise.)

(1)	[	push
(2)	a=0	premise

(1) [

(2) a=0

(3) \(\forall a:a=0\)

(4) Sa=0

(5) ]

meaning is an automatic by-product of our recognition of any isomorphism

Central Proposition: If there is a typographical rule which tells how certain digits are to be shifted, changed, dropped, or inserted in any number represented decimally, then this rule can be rep resented equally well by an arithmetical counterpart which in volves arithmetical operations with powers of 10 as well as addi tions, subtractions, and so forth. More briefly: Typographical rules for manipulating numerals are actually arithmetical rules for operating on numbers

TNT Tries to Swallow Itself This unexpected double-entendre demonstrates that TNT contains strings which talk about other strings of TNT. In other words, the metalanguage in which we, on the outside, can speak about TNT, is at least partially imitated inside TNT itself. And this is not an accidental feature of TNT; it happens because the architecture of any formal system can be mirrored inside N (number theory).

We want to find a string of TNT—which we'll call 'G'—which is about itself, in the sense that one of its passive meanings is a sentence about G. In particular the passive meaning will turn out to be "G is not a theorem of TNT."

We will make our usual assumption: that TNT incorporates valid methods of reasoning, and therefore that TNT never has falsities for theorems. In other words, anything which is a theorem of TNT expresses a truth. So if G were a theorem, it would express a truth, namely: "G is not a theorem". The full force of its self-reference hits us. By being a theorem, G would have to be a falsity. Relying on our assumption that TNT never has falsities for theorems, we'd be forced to conclude that G is not a theorem. This is all right; it leaves us, however, with a lesser problem. Knowing that G is not a theorem, we'd have to concede that G expresses a truth. Here is a situation in which TNT doesn't live up to our expectations—we have found a string which expresses a true statement yet the string is not a theorem. And in our amazement, we shouldn't lose track of the fact that G has an arithmetical interpretation, too—which allows us to summarize our findings this way: A string of TNT has been found; it expresses, unambiguously, a statement about certain arithmetical properties of natural num bers; moreover, by reasoning outside the system we can determine not only that the statement is a true one, but also that the string fails to be a theorem of TNT. And thus, if we ask TNT whether the statement is true, TNT says neither yes nor no.