How Gödel's Proof Works (2020)

"Gödel's Proof" by Ernest Nagel and James R. Newman helped me to get it at some point. On Amazon: <https://www.amazon.com/Godels-Proof-Ernest-Nagel-ebook/dp/B0...> I might even pick up an ebook version if I can find it somewhere else. Been a while.

I'm aware that very smart people have thought carefully about all this, but I still can't help thinking that this argument is unnecessarily complicated. It seems to me that a proof is something that can be written down as a finite string of symbols, so any proof system admits only countably many proofs. On the other hand, it's easy to make up an example of an uncountable set of propositions. That's too many for each of them to have a proof, so some of them must be unprovable. What am I missing?

Show HN: I recently gave a talk on the incompleteness theorem, specifically expressed in the language of software. It starts with a bit of historical background and a discussion of some of the philosophical context in which he carried out his work. The second half of the talk is my attempt to show the beautiful essential idea at the core of Godel's idea, pitched to a technically knowledgeable general audience. These are the slides from the talk, not translated into web pages; YMMV. Link: https://www.gregfjohnson.com/godel_incompleteness/

If you find this interesting, I highly recommend reading "Gödel, Escher, Bach: an Eternal Golden Braid"

> However, although G is undecidable, it’s clearly true. That's... not really true; it's surprising to see it in Quanta, of all places. Godel's (separate) completeness theorem says that in first-order logic, anything that's semantically true in all possible scenarios can be syntactically proved. So, if G is "clearly true", that ought to make it provable. The theorems don't contradict each other because in FOL, G is not guaranteed to be true. Its truth is independent of the machinery Godel put in place. It's not something you really need to get into an introductory text, but it actually makes the whole outcome easier to grasp, and leads to many more counterintuitive results, such as Skolem's paradox.