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

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?

• Just as a heads up, the song T.N.T. by AC/DC is actually written as a self-encoding Gödel sentence for Hofstadter's TNT approach. Also their name is actually a reference to Axiom of Choice/Dependent Choice. Jun 5, 2018 at 14:17
• @AsafKaragila You are taking us on a Highway to Hell there (I can already hear Hell's Bells) Jun 5, 2018 at 14:35
• @Hagen: Well, formally speaking, Hell is Gehenom in Hebrew, which is derived from the Valley of Hinnom or Gehenna. This is a place just outside of Jerusalem. So in reality, what AC/DC were singing about was just being on Route 1 from Tel Aviv to Jerusalem. Jun 5, 2018 at 14:38
• The "construction" on which Gödel's Incompleteness Theorem is based needs a decidable relation $\text{Prf}(x,y)$ - meaning that $y$ is the G-number of a derivation (in the formal system) of the formula whose G-number is $x$ - in order to build $\text{Prov}(x) := \exists y \text{Prf}(x,y)$ - meaning that there is a derivation (in the formal system) of the formula whose G-number is $x$. In order that the last one is semi-decidable (r.e.), we need decidability of the first one. Jun 5, 2018 at 14:57
• In a nutshell, representability of a relation $R(n_1,\ldots, n_k)$ means that (for some $\varphi_R$) : if $R(n_1,\ldots, n_k)$ holds, then $\vdash_F \varphi_R(n_1,\ldots, n_k)$, and if not-$R(n_1,\ldots, n_k)$ holds, then $\vdash_F \lnot \varphi_R(n_1,\ldots, n_k)$. This fact matches the "completeness" property for the formal system $F$ : for every sentence $\varphi$ : either $\vdash_F \varphi$ or $\vdash_F \lnot \varphi$. Jun 5, 2018 at 15:26

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.