tzury · 108 points · 48 comments · 16 jam yang lalu · Open original
Comments
5 preview comments · loading full thread
Log in to use comments
Log in to h4cker, then connect Hacker News to publish comments.
MAMathMonkeyMan10 jam yang lalu
"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.
GRgregfjohnson13 jam yang lalu
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/
GAgavinsyancey15 jam yang lalu
If you find this interesting, I highly recommend reading "Gödel, Escher, Bach: an Eternal Golden Braid"
GRgradschool2 jam yang lalu
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?
MAmatherial14 jam yang lalu
> 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.
Comments
5 preview comments · loading full threadLog in to h4cker, then connect Hacker News to publish comments.
"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.
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"
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?
> 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.