I am trying to understand the proof of Gödel's incompleteness theorems. I am using this document https://mat.iitm.ac.in/home/asingh/public_html/papers/goedel.pdf and finding it quite helpful, but I am a little confused about a particular part of it - on page 2, what is meant by "extend $g$ to proofs of formulas..."? What are $X_1$, $X_2$, etc.?

  • 5
    $\begingroup$ Someone had asked about that same paper before. My advice is that you do not read it and instead look for a different source. The paper has many mistakes and serious technical inaccuracies. I doubt it will end up being helpful, in spite of your current opinion. $\endgroup$ – Andrés E. Caicedo Sep 4 '17 at 14:52
  • 1
    $\begingroup$ See here. $\endgroup$ – Andrés E. Caicedo Sep 4 '17 at 14:53
  • $\begingroup$ To echo Andres' comments, I strongly recommend another source. For example, another paper by the same author contains this: $${}{}$$ "We look at the phrase “the ball game definitely ends in $k$ or fewer moves” as a property of the natural number k. Call this property as $P(k)$. Then “the ball game eventually ends” is translated as $\exists k P(k)$." $${}{}$$ This is, of course, absolutely bonkers: it's like claiming (in fact, it is claiming) "every natural number is finite, so there is a largest natural number." And from the rest of the paper this isn't a typo but rather a genuine error! $\endgroup$ – Noah Schweber Aug 4 '18 at 20:43
  • $\begingroup$ To clarify: that other paper is also about incompleteness, so I'm not randomly picking on an unrelated mistake. The paper is this one. (The specific focus of that paper, incidentally, is an interesting one: the author is trying to give an exposition of an argument of Smullyan's, which is itself a variant of Kirby/Paris' result on Goodstein sequences intended to be easier to approach.) $\endgroup$ – Noah Schweber Aug 4 '18 at 20:46

$X$ is a formula, i.e. a string of symbols.

The function $g$ has been defined for "basic" symbols: $g(\top)=1, g(\bot)=2, \ldots$

Then it is extended to formulas in this way; for $X= \sigma_1 \sigma_2 \ldots \sigma_m$:

$g(X)=g(σ_1 σ_2 \ldots σ_m) = 2^{g(σ_1)} \times 3^ {g(σ_2)} \times \ldots \times p_m ^{g(σ_m)}$.

A proof, i.e. a derivation in the calculus, is a sequence of formulas: $X_1, X_2, \ldots X_n$.

Thus, $g$ can be extended again to encode proofs by:

$g(X_1 X_2 \ldots X_n) = 2^{g(X_1)} \times 3^{g(X_2)} \times \ldots \times p_n ^{g(X_m)}$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.