[HN Gopher] How Godel's proof works (2020)
___________________________________________________________________
How Godel's proof works (2020)
Author : ljosifov
Score : 96 points
Date : 2023-11-23 11:52 UTC (11 hours ago)
(HTM) web link (www.quantamagazine.org)
(TXT) w3m dump (www.quantamagazine.org)
| pfarrell wrote:
| Veritasium has an excellent video explaining the proof and the
| historical context.
|
| https://youtu.be/HeQX2HjkcNo
| grondilu wrote:
| You beat me to it. It is indeed a fantastic Veritasium video.
| One of his best, in my opinion.
| cubefox wrote:
| I remember this video containing some major inaccuracies in his
| presentation of Hilbert's program (which is understandable, he
| is not an expert), so you might want to take the rest of the
| video with a grain of salt as well.
| pfarrell wrote:
| I look at videos like these as gateways to get someone
| excited about a subject, not as scholarly works. What you say
| is good to keep in mind on any video. You can't get the full
| depth of anything complicated in 30 minutes, but it can make
| you want to learn more.
| Kranar wrote:
| What is the major inaccuracy? Usually when I hear claims like
| these and ask for an elaboration it turns out it's not a
| major inaccuracy at all, just a pedantic disagreement over
| what mostly amounts to style.
|
| At any rate I'd definitely be interested in to know what is
| such a major inaccuracy presented that the entire video can
| be dismissed on that basis.
| bmitc wrote:
| Not speaking to any inaccuracies as I haven't watched the
| video, but my main hesitancy is that he's not a
| mathematican, his videos aren't reviewed prior to
| publication, and Godel's work is very subtle and often
| misunderstood.
| ThrowawayTestr wrote:
| You should watch the video before commenting on it
| bmitc wrote:
| I didn't comment on the video. My point is that there
| isn't much draw to it over more accepted and reviewed
| sources.
| passion__desire wrote:
| I liked this explanation of Godel's theorem from programming's
| perspective.
|
| https://www.youtube.com/watch?v=PpSxqde0af4
| hprotagonist wrote:
| John Conway's lectures are quite good.
|
| https://www.youtube.com/watch?v=bSx63Uy-gn0
| scrim wrote:
| For a true dive into this subject I highly recommend the book
| Godel, Escher, Bach.
| demondemidi wrote:
| I have never finished that book. I've started it a dozen times
| since 1990. I die about 60% of the way through it. Does it ever
| get to the theorem?
|
| Edit: thanks for the recommendations, but I have several books
| that discuss the proof. I was just asking if GEB gets to it.
| drivebyadvice wrote:
| There's better resources if you just want to know about
| Godel's Incompleteness Theorem tbh. GEB is neat because of
| all the other ideas he ties into it.
| markisus wrote:
| I think so. But there are much shorter and more rigorous
| proofs in textbooks.
| tshaddox wrote:
| If you're not entertained throughout I don't think there's
| any reason to stick with it. It's not like there's some huge
| payoff at the end where "it all clicks." It's a fairly
| meandering journey across several disciplines with a lot of
| experimental literary techniques, and while it's certainly
| intellectually challenging and rewarding, if you're not
| enjoying the process there's no reason to stick with it!
| scubbo wrote:
| I don't have an answer for you (I last read it so long ago
| that I can't actually recall the specific content - though
| I'd be surprised if it didn't, given the title!), but just
| echoing that, although I _adore_ GEB (actually, I'm over-due
| for a re-read!), I've tried-and-failed multiple times to get
| through "Le Ton Beau De Marot", by the same author. Certain
| books just don't click with some people, and that's OK!
| demondemidi wrote:
| I lost track of the equations and theorems, but if when I
| put it down and come back to it, I've lost momentum! lol.
| Like "Gravity's Rainbow"... someday I'll make it through
| that without getting utterly lost.
| krukah wrote:
| It "gets to the theorem" without offering a formal proof, but
| having read both, I find that Hofstadter's short stories and
| intuitions have done more for my understanding of Godelian
| logic than any formal proofs have.
| bananaflag wrote:
| Yup the theorem gets proven in the book. It's very very
| verbose but the content is clearly there.
|
| "I am a Strange Loop" elaborates a bit on the parts which may
| have been confusingly explained, notably both in the proof of
| the theorem and in the author's AI philosophy.
| passion__desire wrote:
| Not related but I have been recommending Douglas's new popular
| book "Surfaces and Essences: Analogy as the Fuel and Fire of
| Thinking". He has few lectures on youtube on this topic in case
| you want to explore the content of the book before jumping in.
|
| > Analogy is the core of all thinking. This is the simple but
| unorthodox premise that Pulitzer Prize-winning author Douglas
| Hofstadter and French psychologist Emmanuel Sander defend in
| their new work. Hofstadter has been grappling with the
| mysteries of human thought for over thirty years. Now, with his
| trademark wit and special talent for making complex ideas
| vivid, he has partnered with Sander to put forth a highly novel
| perspective on cognition. We are constantly faced with a
| swirling and intermingling multitude of ill-defined situations.
| Our brain's job is to try to make sense of this unpredictable,
| swarming chaos of stimuli. How does it do so? The ceaseless
| hail of input triggers analogies galore, helping us to pinpoint
| the essence of what is going on. Often this means the
| spontaneous evocation of words, sometimes idioms, sometimes the
| triggering of nameless, long-buried memories. Why did two-year-
| old Camille proudly exclaim, "I undressed the banana!"? Why do
| people who hear a story often blurt out, "Exactly the same
| thing happened to me!" when it was a completely different
| event? How do we recognize an aggressive driver from a split-
| second glance in our rearview mirror? What in a friend's remark
| triggers the offhand reply, "That's just sour grapes"? What did
| Albert Einstein see that made him suspect that light consists
| of particles when a century of research had driven the final
| nail in the coffin of that long-dead idea? The answer to all
| these questions, of course, is analogy-making--the meat and
| potatoes, the heart and soul, the fuel and fire, the gist and
| the crux, the lifeblood and the wellsprings of thought.
| Analogy-making, far from happening at rare intervals, occurs at
| all moments, defining thinking from top to toe, from the
| tiniest and most fleeting thoughts to the most creative
| scientific insights. Like Godel, Escher, Bach before it,
| Surfaces and Essences will profoundly enrich our understanding
| of our own minds. By plunging the reader into an extraordinary
| variety of colorful situations involving language, thought, and
| memory, by revealing bit by bit the constantly churning
| cognitive mechanisms normally completely hidden from view, and
| by discovering in them one central, invariant core--the
| incessant, unconscious quest for strong analogical links to
| past experiences--this book puts forth a radical and deeply
| surprising new vision of the act of thinking.
| demondemidi wrote:
| Hash mapping without a computer since 1921.
| acchow wrote:
| Except the Godel encoding is 1:1
| demondemidi wrote:
| A perfect hash table.
| cubefox wrote:
| I find the section about substitution too quick and consequently
| confusing. For example, the author didn't clearly explain the
| meaning of sub(x,y,z).
| rssoconnor wrote:
| Maybe my link at https://news.ycombinator.com/item?id=38395058
| will help? Though even I kinda gloss over how to define sub. It
| is, in my experience, the most technically challenging part of
| the proof to actually formally define. I'm happy to try to go
| over details with you. There is also Section 5.3.1 of my thesis
| at https://r6.ca/thesis.pdf which probably goes into more
| detail than you would like.
| rssoconnor wrote:
| I have a blog post that does a somewhat deeper dive into how to
| build a self-referential sentence @
| https://r6.ca/blog/20190223T161625Z.html where I attempt to
| answer the question:
|
| > I never understood the step about how a system that can do
| basic arithmetic can express the "I am not provable in F"
| sentence. Does anyone have an ELI30 version of that?
| thereticent wrote:
| Nagel & Newman's _Godel 's Proof_ is an excellent book on how the
| proof works. It doesn't have all the tie-ins and fun asides that
| GEB has, but it's stronger for it.
| st-34-lth wrote:
| https://youtu.be/5LWQPGjAs3M?si=WBu6C6mWCZ88pH-K
|
| Any takes on this ? Spreads doubts over godels proofs
| jamiek88 wrote:
| What a lazy comment.
|
| What doubt does it spread?
|
| What's the key take away?
|
| Is it just a crank video?
|
| A famous proof published in 1931 that has had much discussion
| and testing is debunked and disproved on YouTube!
|
| No way of telling except to click through and watch a 15 minute
| video that isn't even vouched for or elaborated on by the
| commenter posting it.
| Kranar wrote:
| I watched the video and the video does not in any way attempt
| to debunk Godel's proof.
|
| I think moreso it just shows that Godel's proof is not as
| significant or as relevant as many people make it out to be,
| and on the whole I'd say I agree with that.
| rssoconnor wrote:
| I didn't watch the video, but FWIW I have personally formally
| verified the First Incompleteness Theorem (Goedel-Rosser
| variant) within the Coq proof assistant.
| abrenuntio wrote:
| Hey I know your proof, the 2005 paper is on my desk :-) If
| you were to code this in Coq again today, would you do things
| different in some way?
| smokel wrote:
| This does not cast doubt on Godel's proofs.
|
| The strengthened liar paradox discussed in the video is "This
| statement is not true", whereas Godel constructed a
| mathematical statement that says something along the lines of
| "This statement is not provable". Proving something is a
| different process than stating something.
| kkylin wrote:
| I thought this writeup was quite good. Anyway, anyone interested
| in this is also likely interested in Rosser's theorem:
| https://scottaaronson.blog/?p=710
| bmitc wrote:
| Does anyone know of any material linking Godel, Turing, and John
| McCarthy's work, beyond their individual publications?
|
| It's also my understanding that Godel did not like publishing.
| Has his unpublished work ever been combed through and published
| in some form? Did he primarily write in English or German? Who
| has his personal papers?
| cwzwarich wrote:
| Godel's collected works (including much unpublished work and
| correspondence) have been published by Clarendon Press, with
| more work (including translations from German) put into them
| than pretty much any other mathematician's collected works.
| bmitc wrote:
| I didn't realize that. Thank you! Volume III seems exactly
| what I'm looking for.
| gregfjohnson wrote:
| Everyone has their own way of stumbling through to a
| breakthrough, where suddenly things that had been confusing and
| complex suddenly seem clear, beautiful, and intuitive.
|
| Here are a couple of thoughts on Godel's incompleteness theorem
| that helped me get there.
|
| First, a description of the idea; consider the following two
| statements:
|
| "There exists a formula with Godel number M that has the property
| that neither the formula nor its negation has a proof."
|
| "Oh, by the way. The Godel number of the above formula is M."
|
| "M" in the above is an actual number. In the first statement, one
| has an arithmetic expression (i.e., "3 + 4*5 + 12^100000 + ...")
| that is short but that evaluates to a really large number.
|
| After developing the idea of mapping formulas and proofs of
| first-order logic to integers, Godel needed to use his new tool
| to come up with some way to express self reference. (The formula
| above has to have an embedded arithmetic expression "M" that
| unwraps and and evaluates to the Godel number of the entire
| formula.)
|
| Godel devised what we would today recognize as exactly the Y
| combinator, expressed in first order arithmetic.
|
| This was a shocking realization when it dawned on me, and it
| enabled me to gain an insight to the magnificent subtlety of
| Godel's mind.
|
| I am personally comfortable with lisp, functions as first-class
| objects, lambda calculus, etc., as is certainly the case for many
| Hacker News readers.
|
| So, at least for me, the above connection helped an awful lot to
| really understand the heart of Godel's insight.
| pyinstallwoes wrote:
| Take this with the most non-serious mode: In the methods used
| by Gematria and various arts, there is a similar mechanism at
| play is there not? Transforming words into quasi-hash
| coordinate space that is computable and thus able to see what
| is related or equal?
| calimoro78 wrote:
| From a newbie here, Aside from the one (and sufficient) self
| referential formula, have we come up with other examples of non
| decidable propositions that are meaningful?
| Sharlin wrote:
| Well, famously the halting problem is undecidable.
|
| As a consequence (via Rice's theorem [1]), _all_ nontrivial
| semantic properties of computer programs are undecidable. That
| is, there 's no algorithm that can answer "does program x have
| property y?" for all programs, although obviously it's possible
| to prove propositions about many _individual_ programs.
|
| Because Turing completeness is a fairly low bar to clear, there
| are infamously a lot of systems that were not designed (or
| indeed designed not) to be Turing-complete but nevertheless
| turned out to be so [2]. As such, things like the Java type
| system is undecidable - in principle there exist Java programs
| that the compiler can neither reject nor accept.
|
| [1] https://en.wikipedia.org/wiki/Rice%27s_theorem
|
| [2]
| https://beza1e1.tuxen.de/articles/accidentally_turing_comple...
| kkylin wrote:
| A well known example (mentioned in the article) is the
| Continuum Hypothesis (CH;
| https://en.wikipedia.org/wiki/Continuum_hypothesis). Godel
| proved CH is consistent with Zermelo-Fraenkel (ZF) set theory;
| Paul Cohen proved that CH is independent of ZF, and hence CH
| cannot be decided on the basis of the ZF axioms.
|
| By now there are numerous others; this is one of the earliest &
| best known examples in mathematics.
| krukah wrote:
| I'm always fascinated by how Godel's incompleteness theorems,
| Cantor's diagonalization proof, Turing's halting problem, and
| Russel's paradox all seem to graze the boundaries of logic.
| There's something almost terrifying about how everything we know
| seems to "bottom out" and what we're left with is an
| embarrassingly small infinite set of truths to grapple with.
|
| It really feels to me as if the distinctions between countable vs
| uncountable; rational vs irrational; discrete vs continuous; all
| represent the boundary between physics and mathematics - an idea
| I wish I could elaborate more precisely, but for me stands only
| on a shred of intuition.
|
| I've been interested lately in Stephen Wolfram's and Scott
| Aaronson's writings on related ideas.
|
| Aaronson on Godel, Turing, and Friends:
| https://www.scottaaronson.com/democritus/lec3.html
|
| Wolfram on computational irreducibility and equivalence:
| https://www.wolframscience.com/nks/chap-12--the-principle-of...
| acchow wrote:
| Physics only seems to be continuous when you "zoom out".
|
| I do agree that Godel's incompleteness is effectively a
| statement about integers. As is our model of computation
| (lambda calculus and church-Turing thesis)
| pyinstallwoes wrote:
| All boundaries are anthropomorphic in bias and nature. Humans
| excel at edge detection, all labels are artificial.
| andrewgleave wrote:
| You may find Constructor Theory interesting. An attempt to
| express physical laws solely in terms of possible and
| impossible transformations.
|
| "These include providing a theory of information underlying
| classical and quantum information; generalising the theory of
| computation to include all physical transformations; unifying
| formal statements of conservation laws with the stronger
| operational ones (such as the ruling-out of perpetual motion
| machines); expressing the principles of testability and of the
| computability of nature (currently deemed methodological and
| metaphysical respectively) as laws of physics; allowing exact
| statements of emergent laws (such as the second law of
| thermodynamics); and expressing certain apparently
| anthropocentric attributes such as knowledge in physical
| terms."
|
| https://arxiv.org/abs/1210.7439
| racl101 wrote:
| I've only had one math prof be able to articulate Godel's
| Incompleteness Theorem for me in a way that I could really
| understand (on a superficial level of course).
|
| She was such a great math prof. Weird how one person can make you
| love a subject even after years of not so great teachers.
| gcanyon wrote:
| Has anyone done work on finding undecidable math beyond self-
| referential statements? Meaning: beyond variations of "who shaves
| the barber," do we have a sense that the undecidable statements
| are all pathologically long, or are there (we think) undecidable
| statements a human can comprehend that are undecidable that don't
| rely on self-reference?
___________________________________________________________________
(page generated 2023-11-23 23:01 UTC)