assert that n is a theorem-number is to assert that some value of m exists
which forms a proof-pair with n. (Incidentally, these comments apply
equally well to TNT and to the MIU-system; it may perhaps help to keep
both in mind, the MIU-system serving as a prototype.) To check whether n
is a theorem-number, you must embark on a search through all its potential
proof-pair "partners" m-and here you may be getting into an endless
chase. No one can say how far you will have to look to find a number which
forms a proof-pair with n as its second element. That is the whole problem
of having lengthening and shortening rules in the same system: they lead to
a certain degree of unpredictability.
The example of the Goldbach Variation may prove helpful at this
point. It is trivial to test whether a pair of numbers (m,n) form a Tortoise-
pair: that is to say, both m and n + m should be prime. The test is easy
because the property of primeness is primitive recursive: it admits of a
predictably terminating test. But if we want to know whether n possesses
the Tortoise property, then we are asking, "Does any number m form a
Tortoise-pair with n as its second element?"-and this, once again, leads us
out into the wild, MU-loopy unknown.
... And Is Therefore Represented in TNT
The key concept at this juncture, then, is Fundamental Fact 1 given above,
for from it we can concludeFUNDAMENTAL FACT 2: The property of forming a proof-pair is
testable in BlooP, and consequently, it is represented in TNT by
some formula having two free variables.Once again, we are being casual about specifying which system these
proof-pairs are relative to; it really doesn't matter, for both Fundamental
Facts hold for any formal system. That is the nature of formal systems: it is
always possible to tell, in a predictably terminating way, whether a given
sequence of lines forms a proof, or not-and this carries over to the
corresponding arithmetical notions.
The Power of Proof-PairsSuppose we assume we are dealing with the MIU-system, for the sake of
concreteness. You probably recall the string we called "MUMON", whose
interpretation on one level was the statement "MU is a theorem of the
MIU-system". We can show how MUMON would be expressed in TNT, in
terms of the formula which represents the notion of MIU-proof-pairs. Let
us abbreviate that formula, whose existence we are assured of by Funda-
mental Fact 2, this way:
MlU-PROOF-PAlR{a,a'}On Formally Undecidable Propositions^441