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?
I'm assuming a finite alphabet and a finitely axiomatizable proof system per convention. I can't think of an uncountable set of propositions in which each can be written as a finite string of symbols, so that's what I was missing. Thank you for clearing this up for me.
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.
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/
GEB is a great book, and I've probably read it at least 3.33333333... times over the years. As a late teen it blew my mind. But I'm not sure I'd recommend it as a route into Gödel's proofs [1]. The book covers a lot of other ground too, and is notoriously digressive and quirky (looking at you, dialogues).
Instead I'd recommend Gödel's Proof by Nagel and Newman for a conceptual intro.
[1] I'm not a mathematician, so my understanding is necessarily informal.
Most proof of the Gödel theorem use the primes encoding that is makes all the operations very unintuitive. But GEB uses just ascii and a lot of the side task get obvious. (It uses base 20 instead of 256, but it's the same idea.)
> is¨notoriously digressive and quirky
It is super mega ultra notoriously digressive and quirky.
I’ll never understand how GEB was using math, art, and music to explain consciousness (and Hofstadter himself still thinks no one understood it), but Nagel and Newman did a great job explaining why logic as a mechanical thing has only a tenuous relationship to concepts we understand, and that helped me crack at least a little bit of the mystery I was after when giving up on GEB.
I have not read GEB but I thought his second book, I am a Strange Loop, did a pretty good job of connecting the idea of self referential loops (like in godels proof) to consciousness and art and such.
Thanks for the suggestions. Just checked out some of Le Ton Beau de Marot, will most likely read the rest.
Actually, I was recently wondering whether poems can be interpreted as "efficient" computer programs. Words in a sentence/essay just connect different objects in space and time (syntactically and semantically) to form some concept, kind of like a program. A poem just uses higher order abstractions (imagery) to express the same concepts in fewer words.
> I’ll never understand how GEB was using math, art, and music to explain consciousness
As Flannery O'Connor wrote, "The result of the proper study of a novel should be contemplation of the mystery embodied in it, but this is a contemplation of the mystery in the whole work and not or some proposition or paraphrase. It is not the tracking down of an expressible moral or a statement about life." We don't read literature with the hopes of a book laying out a precise thesis and incontrovertibly demonstrating it.
If you come into GEB expecting a scientific explanation of consciousness (like I did, when I first read it) you walk away confused and maybe disappointed. Hofstadter observed something transcendentally beautiful about self-reference and had a spiritual or religious revelation that, for him, related it to consciousness, and he attempted to convey that beauty and spiritual revelation in - appropriately self-referentially - a book that embodied it. You're meant to appreciate it in your heart and soul, not (just) in your mind. It's literature, not science.
It’s actually an interesting fact that every person who was programming in the 80s owns a copy of GEB, which they flipped through a bit and then put on the bookshelf and never actually read.
while it is a groovy into to recursion and other cool ideas, GEB annoys me in that I feel like the three figures in the title are ill matched. Godel proves a super important result in math, sure... Escher was a skilled draughtsman who had a feel for tesselation. An OK artist IMO but no special insights. Bach on the other hand was an expressive genius who in the volume, power and beauty of his productions just seemed to drop out the sky like a meteor. Escher does not belong in the same breath frankly. if Bach made a crab canon or did other marginally math-y things that is just not the point - the work lives or dies in entirely different terms...
> 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.
It’s clearly true in The Natural Numbers. It’s not provable because in some model it’s false. Being clearly true in one model does not make it provable.
You can also obtain incompleteness from the unsolvability of the halting problem, by noting that if every statement in (say) Peano arithmetic were provable, one could solve the halting problem. Encode a halting execution of a TM as an integer using Gödel numbers and write a statement that the execution halts. Either that statement or its negation would be provable, so search for proofs for each at the same time.
An additional related theorem is Rogers' recursion theorem, which is how we get programs that, when run, print their own source code (by the theorem this can be done in any Turing complete programming language.)
also,
"Gödel's incompleteness theorems: The proof that broke mathematics" | Joel David Hamkins
https://www.youtube.com/watch?v=Sza69An_H8o
spam-bait title but excellent mid-level talk.
I think Godel's theorem is the single most important result in mathematics. At the same time, when the subject comes up, I like to link people to this essay to dispel a lot of the woo surrounding it regarding human exceptionalism, religion, etc:
I am wondering if I'm just not smart enough to understand, but I've managed to slog through GEB and in the end the proof seems contrived, it stands on self reference.
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.
Nagel & Newman is much better if you find GEB a slog (which was also my experience). However, Gödel’s theorem is fundamentally due to self reference. But so is the fact that the power set of countable infinity is uncountable, in a similar way.
This is my favourite proof in all of maths (that I've been exposed to). Truly unreal feeling proving a statement is unprovable using godel numbering in an exam
Kind of annoying that literally every article or link shared about this always goes on with some massive introduction of the past instead of just getting to the point.
2+2=4 without 7 paragraphs about humanity wanting numerical representations of quantities and the various number systems devised throughout history before they actually gloss over the actual facts and details.
I thought it was sorting an infinite set of infinite strings as the first step in the "algorithm" that seemed sketchy. [0]
It's definitely not a constructive proof, even though it pretends to be; none of the mathematical objects can be constructed, nor can any of the algorithmic steps be executed.
That said, it's far less well-known that the workaround (if you find it to be true) is trivially easy (from Alfred Tarski), making it kind of a useless theorem in practice.
[0] You might think, well, I'll just write out the strings in order by using a generator! No sorting needed... But you have to write the strings down to perform the algorithm, and it takes infinite time to write down the first string, so you'll never even get to the others which is when you do the diagonalization trick. Like I said: it's not constructive, none of it can actually be done.
If "yes" - how might such as proposition be proven true with a finite string of symbols?
(If your proof symbols are from an infinite character set, that has its own issues.)
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.
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.
https://archive.org/download/douglas-r.-hofstadter-collected... (PDF)
Instead I'd recommend Gödel's Proof by Nagel and Newman for a conceptual intro.
[1] I'm not a mathematician, so my understanding is necessarily informal.
Most proof of the Gödel theorem use the primes encoding that is makes all the operations very unintuitive. But GEB uses just ascii and a lot of the side task get obvious. (It uses base 20 instead of 256, but it's the same idea.)
> is¨notoriously digressive and quirky
It is super mega ultra notoriously digressive and quirky.
Unrusprisingly, since many years went by. But I still love the quirkiness of GEB
(Also, he has other books between the two, I deeply enjoyed Le Ton Beau de Marot, about translations)
Actually, I was recently wondering whether poems can be interpreted as "efficient" computer programs. Words in a sentence/essay just connect different objects in space and time (syntactically and semantically) to form some concept, kind of like a program. A poem just uses higher order abstractions (imagery) to express the same concepts in fewer words.
So this book should be great!
As Flannery O'Connor wrote, "The result of the proper study of a novel should be contemplation of the mystery embodied in it, but this is a contemplation of the mystery in the whole work and not or some proposition or paraphrase. It is not the tracking down of an expressible moral or a statement about life." We don't read literature with the hopes of a book laying out a precise thesis and incontrovertibly demonstrating it.
If you come into GEB expecting a scientific explanation of consciousness (like I did, when I first read it) you walk away confused and maybe disappointed. Hofstadter observed something transcendentally beautiful about self-reference and had a spiritual or religious revelation that, for him, related it to consciousness, and he attempted to convey that beauty and spiritual revelation in - appropriately self-referentially - a book that embodied it. You're meant to appreciate it in your heart and soul, not (just) in your mind. It's literature, not science.
https://nyupress.org/9780814758014/godels-proof/
Much like the many unread copies of Knuth's TAOCP.
(It's the title of his follow up work after GEB.)
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.
An additional related theorem is Rogers' recursion theorem, which is how we get programs that, when run, print their own source code (by the theorem this can be done in any Turing complete programming language.)
Joel David Hamkins - Oxford lectures on the philosophy of mathematics "The Gödel incompleteness phenomenon" https://www.youtube.com/watch?v=Y5trjR5aw0k
also, "Gödel's incompleteness theorems: The proof that broke mathematics" | Joel David Hamkins https://www.youtube.com/watch?v=Sza69An_H8o spam-bait title but excellent mid-level talk.
edit: speling
Godels Incompleteness Theorem (Little Mathematics Library)
by V. A. Uspensky
https://archive.org/details/GodelsIncompletenessTheorem
"Opposite statements, G and ~G, can’t both be true in a consistent axiomatic system."
https://shs.cairn.info/revue-internationale-de-philosophie-2...
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.
2+2=4 without 7 paragraphs about humanity wanting numerical representations of quantities and the various number systems devised throughout history before they actually gloss over the actual facts and details.
The same as me asking you to give me the last digit of pi.
I am a bit annoyed by pop science always twisting it to sound so convoluted.
It's definitely not a constructive proof, even though it pretends to be; none of the mathematical objects can be constructed, nor can any of the algorithmic steps be executed.
That said, it's far less well-known that the workaround (if you find it to be true) is trivially easy (from Alfred Tarski), making it kind of a useless theorem in practice.
[0] You might think, well, I'll just write out the strings in order by using a generator! No sorting needed... But you have to write the strings down to perform the algorithm, and it takes infinite time to write down the first string, so you'll never even get to the others which is when you do the diagonalization trick. Like I said: it's not constructive, none of it can actually be done.
Some previous discussions:
2023 https://news.ycombinator.com/item?id=38391787
2020 https://news.ycombinator.com/item?id=23832087