the day: how to prove a system consistent. Godel found a simple way to
express the statement "TNT is consistent" in a TNT formula; and then he
showed that this formula (and all others which express the same idea) are
only theorems of TNT under one condition: that TNT is inconsistent. This
perverse result was a severe blow to optimists who expected that one could
find a rigorous proof that mathematics is contradiction-free.
How do you express the statement "TNT is consistent" inside TNT? It
hinges on this simple fact: that inconsistency means that two formulas, x
and - x, one the negation of the other, are both theorems. But if both x
and - x are theorems, then according to the Propositional Calculus, all
well-formed formulas are theorems. Thus, to show TNT's consistency, it
would suffice to exhibit one single sentence of TNT which can be proven to
be a nontheorem. Therefore, one way to express "TNT is consistent" is to
say "The formula -0=0 is not a theorem of TNT". This was already
proposed as an exercise a few pages back. The translation is:
-3a:TNT-PROOF-PAIR{a,SSSSS ..... SSSSSO/a'}
------------223,666,111,666 S's
It can be shown, by lengthy but fairly straightforward reasoning, that-as
long as TNT is consistent-this oath-of-consistency by TNT is not a theo-
rem of TNT. So TNT's powers of introspection are great when it comes to
expressing things, but fairly weak when it comes to proving them. This is
quite a provocative result, if one applies it metaphorically to the human
problem of self-knowledge.TNT Is w-IncompleteNow what variety of incompleteness does TNT "enjoy"? We shall see that
TNT's incompleteness is of the "omega" variety-defined in Chapter VIII.
This means that there is some infinite pyramidal family of strings all of
which are theorems, but whose associated "summarizing string" is a non-
theorem. It is easy to exhibit the summarizing string which is a nontheo-
rem:
uS's
~
Va:-3a':<TNT-PROOF-PAlR{a,a' }AARITHMOQUlNE{SSS ... SSSO/a",a'}>To understand why this string is a nontheorem, notice that it is extremely
similar to G itself-in fact, G can be made from it in one step (viz.,
according to TNT's Rule of Interchange). Therefore, if it were a theorem,
so would G be. But since G isn't a theorem, neither can this be.
Now we want to show that all of the strings in the related pyramidal
family are theorems. We can write them down easily enough:
450 On Formally Undecidable Propositions