GEB Why is it necessary for TNT-PROOF-PAIR{a,a'} to be represented in TNT?

Question

In Hofstadter's Gödel, Escher, Bach there is the predicate TNT-PROOF-PAIR{a,a'} which is used in constructing the Gödel string.

He then explains that it is a fundamental fact that this is not only expressed in TNT but also represented in TNT, which means that this predicate is always decidable for 2 concrete numerals.

Now why is this fact important? Couldn't the Gödel string be constructed in the same way if the predicate was only expressible and not decidable?

Answer 1

1. Yes, the Gödel formula could be constructed if the predicate was not represented in TNT, but then TNT would be a weak system and already incomplete because TNT-PROOF-PAIR{a,a'} is undecidable, therefore the Gödel construction becomes superfluous.
2. The hope was that a strong system(where TNT-PROOF-PAIR{a,a'} is represented/decidable) would provide a decision procedure for any formula because either it is true and therefore a provable theorem, or it is false and therefore its negation a provable theorem. This is what completeness means.
3. The whole point of the Gödel construction was to prove that even strong systems are incomplete.