0
$\begingroup$

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?

$\endgroup$
6
  • 1
    $\begingroup$ 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. $\endgroup$
    – Asaf Karagila
    Jun 5, 2018 at 14:17
  • $\begingroup$ @AsafKaragila You are taking us on a Highway to Hell there (I can already hear Hell's Bells) $\endgroup$ Jun 5, 2018 at 14:35
  • 1
    $\begingroup$ @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. $\endgroup$
    – Asaf Karagila
    Jun 5, 2018 at 14:38
  • 2
    $\begingroup$ 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. $\endgroup$ Jun 5, 2018 at 14:57
  • 2
    $\begingroup$ 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$. $\endgroup$ Jun 5, 2018 at 15:26

1 Answer 1

1
$\begingroup$
  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.
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .