How Gödel’s Proof Works

For a detailed perspective on how the proof works, I highly recommend Ernest Nagel and James Newman's book Gödel's Proof [0], mentioned in the article. Alternatively, Gödel Escher Bach by Douglas Hofstader is a classic which serves as a great (and more accessible) introduction to the proof [1].

[0] https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081...

[1] https://www.amazon.com/G%C3%B6del-Escher-Bach-Eternal-Golden...

Actually, the [Gödel 1931] proof does not work as advertised for Principia Mathematica because the Gödel number of a proposition does not include the order of the proposition.

Consequently, the rules on orders of propositions mean that the [Gödel 1931] proposition I'mUnprovable does not exist in Principia Mathematica where

            I'mUnprovable <=> ¬⊦I'mUnprovable

For details see the following: https://papers.ssrn.com/abstract=3603021

With today's knowledge, Gödel's theorem should be regarded as a corollary of the impossibility to solve the halting problem.

In my opinion, this is also how it should be taught in order to convey the explanation for its truth in the most straightforward way.

After that, one may of course also note that in the old days, without a good theory of computation, one had to resort to such hacks as Gödel numbers.

A good explanation including all the finer points can be found here: https://www.scottaaronson.com/blog/?p=710

Just finished a book club for Gödel, Escher, Bach, which gives a lay -- but pretty detailed and thorough -- explanation of the proof. Here's how I'd say lay out the key insights as they applied to the parts I didn't understand before.

You want to use pure math to say "this statement cannot be proven". To do that, you:

1) Express the concept of statements following from other strings by the axioms or other theorems.

2) Express the concept of "this is a valid chain of statements, each of which follows from the previous". (GEB calls it a proof-pair.)

3) Express the concept of "Statement A does not have such a valid chain" (there exists no such chain with A at the end).

That allows you to say "Statement A cannot be proven."

From that point, it's a matter of extending it to the statement (call it G): "There exists a statement S such that S has no proof and S statisfies criteria A/B/C."

...and then constructing the criteria A/B/C such that G is the one statement that can satisfy it. The details of how you construct the criteria so that you are specifying G are the Gödel numbering that the Quanta article describes.

Charles Petzold's "Annotated Turing" is a book about Turing's article, which provides another approach to this problem. Turing machine, described in the article, is arguably a more - convenient? generalized? - device for similar areas.

Yes, Godel's theorem is mentioned more than once.