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

Scott Aaronson's post is very interesting. Unfortunately, Scott's proofs in the above blog post do not work for strongly-typed foundations of Computer Science.

For more information, see the following:

https://papers.ssrn.com/abstract=3418003

Yes, this is the way to correctly prove "incompleteness", i.e that there are preferentially undecidable propositions in powerful theories of computer science.

See the following for a proof: https://papers.ssrn.com/abstract=3603021

Of course, I meant to say "inferentially undecidable" instead of "preferentially undecidable".

Being inferentially undecidable means that it is not the case that for every proposition, there is either a proof of the proposition or its negation.

Inferential undecidablity implies "incompleteness" in the sense that it is not the case that every true proposition can be proved.

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.

Unfortunately, the above proof sketch does not work. Mathematics becomes inconsistent if a proposition G is allowed such that G<=>¬⊦G.

For a simple proof that allowing such a G makes mathematics inconsistent, please see the following:

https://papers.ssrn.com/abstract=3603021

The proposition G in the sketch above just says G can't be proven, not that it's false, just like the one in GEB.

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.

You might be interested in knowing that there are some nondeterministic computations that cannot be performed by a Turing Machine.

For a simple example, see the following:

https://papers.ssrn.com/abstract=3418003

https://papers.ssrn.com/abstract=3459566

I have this book. It's an amazing and recommended read.