From the article:<p>> Here’s another example (known as the Berry paradox):<p>> Define {x} to be the smallest positive integer that cannot be defined in under {100} words.<p>> This might look like a valid mathematical definition. But again it’s nonsensical. And, importantly for the sanity of mathematics, no analogous statement can be made mathematically formal.<p>I thought it was worth mentioning that the Berry Paradox <i>does</i> show up in a mathematically formal way, and it was fascinating to me. It can be used to prove that a general algorithm to compute the Kolmogorov complexity of a string is uncomputable.<p><a href="https://en.wikipedia.org/wiki/Berry_paradox#Formal_analogues" rel="nofollow">https://en.wikipedia.org/wiki/Berry_paradox#Formal_analogues</a>
A layperson here, I always wanted to ask this question: Godel proves that not ALL statements that are true can be proven, because here is this one example. I get it, it's a valid mathematical proof. But does it really say anything about other statements, except this one? Does it says anything about statements that are not self-referential? Is it possible that the incompleteness theorem really applies only to self-referential statements and says nothing about non-self-referential statements?
What made the theorem hard is not the details, which are simple, it's the conceptual leap to thinking about mathematical statements as mathematical objects - something that is much easier for us than for mathematicians of Godel's time because we are familiar with programs and computers. Much of the text is taken up with proving things that were surprising to mathematicians of the era, but are now commonplace: e.g. that we can treat numbers as encoding mathematical propositions so that for every proposition P expressible in some formal logic L, there is a number #P which encodes P in some unambiguous way - as long as L is expressive enough to formalize some basic arithmetic. Then we can start making trouble by asking if we can construct a proposition Q so that Q(#P) is true iff the proposition #P encodes, P, is provable in our system. If so, we should be able to prove Q(#P) or NOT Q(#P) if L is complete, but things don't work out well because it's possible to encode paradoxical statements. In short.
Godel Incompleteness Theorem and Turing Halting Problem are two faces to the same coin, I intuited. It is deeper than I thought, especially that I forgot about the two godel's incompleteness theorems (not just one.)<p>Scott Aaranson "popularizes" Kleene's textbook proof of Godel's theorems using Turing machines in his blog:<p><a href="https://www.scottaaronson.com/blog/?p=710" rel="nofollow">https://www.scottaaronson.com/blog/?p=710</a>
While the Berry paradox isn't strictly speaking mathematically sensible, there are similar ideas that lead to new and less well-known impossibility results. <a href="https://arxiv.org/pdf/chao-dyn/9406002.pdf" rel="nofollow">https://arxiv.org/pdf/chao-dyn/9406002.pdf</a> has a transcript of an overview of the idea and main results by the researcher who came up with them, as well as a fairly extensive bibliography.<p>There's also a version of Russell's paradox lurking in the standard proof of Cantor's theorem (<a href="https://en.wikipedia.org/wiki/Cantor%27s_theorem" rel="nofollow">https://en.wikipedia.org/wiki/Cantor%27s_theorem</a>).
I couldn't make it through GEB, but I read a good concise explanation in a book called Godel's Proof: <a href="https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371" rel="nofollow">https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081...</a>
See the following for history and limitations of Godel's results:<p><a href="https://hal.archives-ouvertes.fr/hal-01566393" rel="nofollow">https://hal.archives-ouvertes.fr/hal-01566393</a>
I just read "I Am a Strange Loop" and he the author a pretty nice job of explaining this -- Unfortunately, I could never get through GEB so I do not know if the explanation in there.
For those interested, Hoffstadter's Godel Escher Bach gives a great introduction into formal systems and Godels incompleteness theorem. Highly recommended.