There is no effectively computable procedure for telling theorems of TNT (and other sufficiently powerful Formal systems) from nontheorems.

See GEB for proof on page 580

It all hinges on what G says: "G is not a theorem of TNT". Assume that G were a theorem. Then, since theoremhood is supposedly represented, the TNT-formula which asserts "G is a theorem" would be a theorem of TNT. But this formula is -G, the negation of G, so that TNT is inconsistent. On the other hand, assume G were not a theorem. Then once again by the supposed representability of theoremhood, the formula which asserts "G is not a theorem" would be a theorem of TNT. But this formula is G, and once again we get into paradox. Unlike the situation be fore, there is no resolution of the paradox. The problem is created by the assumption that theorernhood is represented by some formula of TNT, and therefore we must back track and erase that assumption. This forces us also to conclude that no FlooP program can tell the Gödel numbers of theorems from those of nontheorems. Finally, if we accept th e Al Version of the CT-Thesis, then we must backtrack further, and conclude that no method whatsoever could exist by which humans could reliably tell theorems from nont heorems-and this includes determinations based on beauty. Those who subscribe only to the Public-Processes Version might still think the Crab's performance is possible; but of all the versions, that one is perhaps the hardest one to find any justification for.