10 ms·
How Gödel's proof works (2020)
- pfarrell 3y agoVeritasium has an excellent video explaining the proof and the historical context. https://youtu.be/HeQX2HjkcNo https://youtu.be/HeQX2HjkcNo
- grondilu 3y agoYou beat me to it. It is indeed a fantastic Veritasium video. One of his best, in my opinion.
- cubefox 3y agoI 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 3y agoI 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 3y agoWhat 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 3y agoNot 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 3y agoYou should watch the video before commenting on it
- bmitc 3y agoI didn't comment on the video. My point is that there isn't much draw to it over more accepted and reviewed sources.
- cubefox 3y agoThe way he presents Hilbert's program in 13:34 would make it immediately incompatible with Gödel's theorems. But Hilbert's program was different from what is suggested in the video. It was concerned with proving the consistency of mathematics (or more specifically, arithmetic) using "finitary methods", and in a "conservative" manner using the notions of "real" and "ideal" mathematics. Whether Gödel's theorems show that this is impossible is not completely clear, as it is not established what should count as "finitary", and how to interpret Hilbert's conservativity requirement. See this section for an overview: https://plato.stanford.edu/entries/hilbert-program/#4 https://plato.stanford.edu/entries/hilbert-program/#4 Another inaccuracy: In 8:42 he says Russell pointed out a "problem in Cantor's set theory". But Cantor's theory wasn't even axiomatized, and Russell didn't talk about Cantor's theory, but about Frege's Basic Laws of Arithmetic, which contained an inconsistency. The thing I was pointing at (grain of salt) is basically the same as Gell-Mann amnesia[1]: Why should you trust someone in a subject you don't know anything about, when you don't overly trust him in topics where you do know something about? The trust level should arguably be the same in both subjects. 1: https://news.ycombinator.com/item?id=13155538 https://news.ycombinator.com/item?id=13155538
- Tainnor 3y agoI think you have to be really, really charitable not to see the Second Incompleteness Theorem as a complete repudiation of the Hilbert Program - at least it destroys the possibility of proving ZFC consistent in PA - to the point that I think it's a reasonable simplification to say that the Hilbert program failed, even if the paragraph you linked shows that some people have been trying to salvage Hilbert's program by relaxing it a little. I'm aware e.g. of Gentzen's proof of the consistency of PA, but I don't find it plausible to claim that it uses "finitary methods". At the very least, I don't think such arguments would have convinced the people that Hilbert was trying to convince, such as intuitionists. Your second point also seems like a very minor nitpick. Clearly, set theory is inconsistent if you don't impose any restrictions on what kinds of set can be formed (something that Cantor to my knowledge didn't do), which is what Russell's paradox showed. The fact that they used Frege's formalisation for setting up the paradox doesn't seem particularly relevant to me.
- passion__desire 3y agoI liked this explanation of Godel's theorem from programming's perspective. https://www.youtube.com/watch?v=PpSxqde0af4 https://www.youtube.com/watch?v=PpSxqde0af4
- hprotagonist 3y agoJohn Conway’s lectures are quite good. https://www.youtube.com/watch?v=bSx63Uy-gn0 https://www.youtube.com/watch?v=bSx63Uy-gn0
- scrim 3y agoFor a true dive into this subject I highly recommend the book Godel, Escher, Bach.
- demondemidi 3y agoI 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 3y agoThere's better resources if you just want to know about Gödel's Incompleteness Theorem tbh. GEB is neat because of all the other ideas he ties into it.
- markisus 3y agoI think so. But there are much shorter and more rigorous proofs in textbooks.
- tshaddox 3y agoIf 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 3y agoI 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 3y agoHash mapping without a computer since 1921.
- acchow 3y agoExcept the Godel encoding is 1:1
- demondemidi 3y agoA perfect hash table.
- cubefox 3y agoI 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 3y agoMaybe my link at https://news.ycombinator.com/item?id=38395058 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 https://r6.ca/thesis.pdf which probably goes into more detail than you would like.
- cubefox 3y agoThanks, in your case the informal definition is clear. I believe in the Quanta article the second and third argument of sub are switched relative to yours. Another question, do you use Cantor-style diagonalization for the fixed-point theorem? Apparently this is the case for the standard proof of incompleteness, as explained here, though this paper goes over my head: https://haimgaifman.files.wordpress.com/2016/07/22odel-to-kleene.pdf https://haimgaifman.files.wordpress.com/2016/07/22odel-to-kl... The reason why I'm asking is that Cantor used diagonalization in his famous "diagonal argument" for the real numbers being uncountable. Some people found this argument unconvincing, because it relied on perhaps questionable assumptions, like the decimal representation of real numbers and that different decimal representations must denote a different real number. But if the diagonal argument (or his earlier powerset argument) could be formalized and checked with Coq, doubts would presumably be removed.
- rssoconnor 3y ago> do you use Cantor-style diagonalization for the fixed-point theorem? If you think Kleene's recursion theorem and Cantor's diagonalization are the same sort of argument, then I'd say yes. I don't know if people historically had an issue with Cantor's argument or not. Certainly the modern presentation with decimals can be dicey if you are not careful because, as you note, some real numbers have two representations as decimals, one with repeating 9's and another with repeating 0's. But this issue can be avoided so long as you are careful. e.g convert all non-5's to 5's and convert 5's to 6's, thus staying far away from the dangerous 0/9 zone of digits. The constructed decimal sequence only has 5's and 6's and thus is a real number with a unique decimal representation. There is no problem with Cantor's argument, and it can easily be formalized. It would be a reasonable exercise to do at some point in an introductory course for proof assistants.
- justincredible 3y ago[dead]
- rssoconnor 3y agoI have a blog post that does a somewhat deeper dive into how to build a self-referential sentence @ https://r6.ca/blog/20190223T161625Z.html 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 3y agoNagel & Newman's Gödel'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 3y agohttps://youtu.be/5LWQPGjAs3M?si=WBu6C6mWCZ88pH-K https://youtu.be/5LWQPGjAs3M?si=WBu6C6mWCZ88pH-K Any takes on this ? Spreads doubts over godels proofs
- jamiek88 3y agoWhat 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 3y agoI 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 3y agoI 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 3y agoHey 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?
- rssoconnor 3y agoMy biggest mistake was following the traditional single variable definition of substitution. I now understand that modern CS definitions of substitution typically substitute all (free) variables simultaneously. For variables that you don't want to substitute, you are required to explicitly map them back to themselves. Chapter 7 of my thesis <https://r6.ca/thesis.pdf https://r6.ca/thesis.pdf> has some more comments. With a bit more care using Prop/Set maybe one could compute explicitly what these Goedel sentences are (similar to <https://web.archive.org/web/20160528092209/http://tachyos.org/godel/Godel_number.html https://web.archive.org/web/20160528092209/http://tachyos.or...>). Maybe using Robinson Q instead of Hodel's obscure NN system would have been better, or maybe with a bit more abstraction it would be easier to apply the proof to other axioms systems, such as ZF, which don't use the same language that PA does. And maybe making sure the Second Incompleteness could follow more easily would be good (which has since been formalized elsewhere).
- kkylin 3y agoI thought this writeup was quite good. Anyway, anyone interested in this is also likely interested in Rosser's theorem: https://scottaaronson.blog/?p=710 https://scottaaronson.blog/?p=710
- bmitc 3y agoDoes 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 3y agoGodel’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 3y agoI didn't realize that. Thank you! Volume III seems exactly what I'm looking for.
- gregfjohnson 3y agoEveryone 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 3y agoTake 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?
- gregfjohnson 3y agoFascinating observation, thanks. Relevant to your comment but diverging farther from the original post: Coincidentally, I am taking a beginner's Kabbalah course right now. I wonder if some of the writers of scripture actually used steganography or other word encodings such as the ones you allude to intentionally. One obvious example of word play at the meta level might be Psalm 119.
- calimoro78 3y agoFrom 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 3y agoWell, 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 https://en.wikipedia.org/wiki/Rice%27s_theorem [2] https://beza1e1.tuxen.de/articles/accidentally_turing_complete.html https://beza1e1.tuxen.de/articles/accidentally_turing_comple...
- kkylin 3y agoA well known example (mentioned in the article) is the Continuum Hypothesis (CH; https://en.wikipedia.org/wiki/Continuum_hypothesis 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 3y agoI'm always fascinated by how Gödel'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 Gödel, Turing, and Friends: https://www.scottaaronson.com/democritus/lec3.html https://www.scottaaronson.com/democritus/lec3.html Wolfram on computational irreducibility and equivalence: https://www.wolframscience.com/nks/chap-12--the-principle-of-computational-equivalence/ https://www.wolframscience.com/nks/chap-12--the-principle-of...
- acchow 3y agoPhysics 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 3y agoAll boundaries are anthropomorphic in bias and nature. Humans excel at edge detection, all labels are artificial.
- andrewgleave 3y agoYou 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 https://arxiv.org/abs/1210.7439
- racl101 3y agoI've only had one math prof be able to articulate Gödel'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 3y agoHas 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?
- wardedVibe 3y agoSo the most physically grounded example I know of is the undecidability of some spectral gaps[0] (is there a discrete jump between the ground state and the excited states), which as far as I can tell doesn't rely on self-reference. [0]: https://arxiv.org/pdf/1502.04573.pdf https://arxiv.org/pdf/1502.04573.pdf
- calf 3y agoApparently it does? Check this old comment from Scott Aaronson: > Rahul #97: No, because the other point is that whether a spectral gap goes to zero as the lattice size goes to infinity is the kind of thing that real condensed-matter physicists and quantum field theorists ask all the time. It’s something they accept every day as a good mathematical idealization for what they care about. So it’s worthwhile to know that their problem secretly contains the halting problem—that for large enough constant d, there can never be a clean algorithmic criterion to tell you which nearest-neighbor qudit Hamiltonians are gapped and which are gapless. https://scottaaronson.blog/?p=2586#comment-975416 https://scottaaronson.blog/?p=2586#comment-975416 If I read this he's clearly implying the spectral gaps problem is done by reduction to the halting problem. (Edit, in the blog entry he explains: "Cubitt et al.’s theorem now says the following: for some fixed, constant local dimension d, there is no algorithm that takes as input the local Hamiltonian h (say, as a d2×d2 matrix of algebraic numbers), and that decides whether the material is gapped or gapless. Indeed, you can reduce the halting problem to that problem, in such a way that the material will be gapped if your Turing machine halts, or gapless if it runs forever.")
- gsinclair 3y agoI believe the continuum hypothesis is an example of an undecidable statement. That is, we know that the integers have cardinality of “aleph null”, the smallest infinity. And we know how to construct the “next” level of infinity using something analogous to power sets. Call this “aleph one”. Now the hypothesis: the cardinality of the real numbers is equal to aleph one. It is known that we can never prove that hypothesis one way or the other. The US mathematician Paul Cohen established this in the 1960s. There are probably egregious errors in my telling of this, but it could be a prompt for further reading.
- farhanhubble 3y agoI have known about Godel's work and the incompleteness theorem but never understood it much until I read this article. Can anyone recommend a book relating to Godel's work written is a similarly accessible style?
- adrianh 3y ago"I Am A Strange Loop," by Douglas Hofstadter, is reasonably accessible and has an explanation of this in very readable prose.