How Gödel's Proof Works (2020)

I think you certainly grasp the gist of things if you understand that the point is self-reference. What makes the proof shocking and beautiful (at least, IMO), is how sparse a toolbox Gödel is working with (and, perhaps, how clever the construction is). Contradictory self-reference in, say, plain English or naïve set theory, is not particularly surprising (at least to our modern eyes), because those are rich languages where you can express an extremely wide range of statements, but Gödel manages to smuggle it in using just whole-number arithmetic and first-order logical statements, which provides a recipe for doing so in essentially any formalized system of interest to "normal" mathematicians.

Some comments elsewhere in this topic mention that you can use the halting problem to arrive at the same essential conclusion in a more understandable way (and certainly one less fraught with small technicalities to work through), but (again, IMO) there's a certain mischievous magic to the way the Gödel sentence gets constructed that makes it very fun to work through for the first time.

[dead]

Wish I had the full text on me, but I recall there's a version of it with an introduction by Douglas Hofstadter that disagrees with the interpretation of the proof by Nagel and Newman, and it's something key to their culminating assessment of what Gödel's proof truly means, which is a remarkable disagreement to put into a forward to a text. Unfortunately the Kindle version I got from Amazon doesn't contain his forward and I'm struggling to find that version.

Edit: found the quote, and frankly I agree wholeheartedly with Hofstadter who seems to have a much more sophisticated understanding of the capabilities of computers, perhaps owing to his encountering them in a later era.

"My book, despite owing a large debt to Nagel and Newman, does not agree with all of their philosophical conclusions, and here I would like to point out one key difference. In their “Concluding Reflections,” Nagel and Newman argue that from Godel’s discoveries it follows that computers—“calculating machines,” as they call them—are in principle incapable of reasoning as flexibly as we humans reason, a result that supposedly ensues from the fact that computers follow “a fixed set of directives” (i.e., a program).

To Nagel and Newman, this notion corresponds to a fixed set of axioms and rules of inference—and the computer’s behavior, as it executes its program, amounts to that of a machine systematically churning out proofs of theorems in a formal system. This mapping of computer onto formal system takes the term “calculating machine” very literally—that is, a machine built to deal.with numbers and arithmetical facts alone. The idea that such machines by their very nature should churn out sets of true statements about mathematics is seductive and certainly has a grain of truth to it, but it is far from the full vision of the power and versatility of computers.

Although computers, as their name implies, are built of rigidly arithmetic-respecting hardware, nothing in their design links them inseparably to mathematical truth. It is no harder to get a computer to print out scads of false calculations (“2 + 2 = 5; 0/0 = 43,” etc.) than to print out theorems in a formal system. A subtler challenge would be to devise “a fixed set of directives” by which a computer might explore the world of mathematical ideas (not just strings of mathematical symbols), guided by visual imagery, the associative patterns linking concepts, and the intuitive processes of guesswork, analogy, and esthetic choice that every mathematician uses.

When Nagel and Newman were composing Godel’s Proof, the goal of getting computers to think like people—in other words, artificial intelligence—was very new and its potential was unclear. The main thrust in those early days used computers as mechanical instantiations of axiomatic systems, and as such, they did nothing but churn out proofs of theorems. Now admittedly, if this approach represented the full scope of how computers might ever in principle be used to model cognition, then, indeed, Nagel and Newman would be wholly justified in arguing, based on Godel’s discoveries, that computers, no matter how rapid their calculations or how capacious their memories, are necessarily less flexible and insightful than the human mind.

But theorem-proving is among the least subtle of ways of trying to get computers to think[...]"

He goes on like this for a bit more, and fleshes out a deeper argument, but this is already long as quoted passages on hn go. But I think Hofstadter is exactly right and shows a much more sophisticated understanding of computers than Nagel and Newman in their celebrated introduction to Gödel. I would go so far as to say their philosophical conclusion is almost exactly wrong, and is as baffling as if Darwin's Origin of Species included a section of "conclusions" denying the possibility of ever developing effective vaccines in the future. Wrong to the point of being contrary to the spirit of the subject that was so exceptionally articulated up to that point. And it's in my opinion terribly damaging for a conclusion so backwards to be embedded in a text that's celebrated as the best explanation of the proof.

[flagged]

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?