47 ms·
What Gödel Discovered
- ProfHewitt 6y agoAlthough [Gödel 1931] failed to proved inferential undecidability of Russell's Principia Mathematica, there is a fairly simple undecidable proposition namely, the proposition *Undecidable*≡Halt<ExpressionFromString<Natural>>[RunOne.[]] where RunOne.[]≡Eval.[SelectOne.[0]] such that SelectOne.[i:Natural]≡ExpressionFromString<Natural>.[i] *finishesFirst* SelectOne.[i+1] Eval.[anExpression] evaluates anExpression and where the expression (expression1 *finishesFirst* expression2) returns the value of whichever of the expressions expression1 and expression2 evaluation finishes first. The procedure SelectOne selects one of the expressions created from strings. For details see: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- ProfHewitt 6y agoThere is a small typo in the above: Undecidable ≡ Halt<ExpressionFromString<Natural>>[⦅RunOne.[]⦆] is inferentially undecidable in the theory Actors, that is, ⊬Undecidable and ⊬¬Undecidable where RunOne.[]≡Eval.[SelectOne.[0]] and ⦅RunOne.[]⦆ is the expression for the procedure application RunOne.[]
- lqet 6y agoThis is a very nice and surprisingly readable write up. I think it is the best explanation of the incompleteness theorem I've ever read. Thank you for this! > Now, say he wanted to write when. He could just write 17. Shouldn't it be 19?
- stopachka 6y agoThanks for the kind words and the catch! Updated :) -- may take a few mins to show up
- deleted 6y ago[deleted]
- rntksi 6y agoSuch a quality write-up, I understood the topic easily ! Thank you :-)
- stopachka 6y agoCheers and thank you!
- marwan-nwh 6y ago[Commenting before reading] I was just reading about hilbert's problems, and his disappointment after Godel's and alan turing's papers. I am not sure if this blog is about that, but it is a very interesting topic. Let's read it now :)
- eyeundersand 6y agoThis is remarkably well done. I'm reading Hofstadter's Godel, Escher, Bach and found this at the perfect time. Thanks for the write up!
- stopachka 6y agoThank you :)
- marwan-nwh 6y agoMan, I just searched about that book, and it is like there is a world I don't know anything about. Would you mind sharing the names of your favorite books?
- hypertexthero 6y agoSee also I Am A Strange Loop by Douglas Hofstadter, and The First and Last Freedom by Jiddu Krishnamurti.
- madia_leva 6y agoEGB is one of my favourite books ever, but I think it doesn't explain Gödel's theorem as simple as it could. Of course, there are just so many wonderful things in EGB that this is not a fatal flaw by any means. There is a fantastic book called "The Universal Computer: The Road from Leibniz to Turing" by Martin D. Davis that makes a very good job of explaining the context of Gödel's theorem, the theorem itself and the relation with computing in an accesible way. I'd recommend it to anyone interested either in computers or in Gödel's theorem.
- eyeundersand 6y agoYup. Also recommend to those interested in existential philosophy and artificial intelligence as well. It really is a terrific book!
- layer8 6y agoGödel’s Proof by Nagel and Newman is quite good. ISBN 0814758371
- xyzzyz 6y agoI’m a mathematician who spent many hours thinking about Goedel theorem and adjacent topics. The author in a self-deprecating way says that he’s not a mathematician, but just a programmer. Bear no mind to that: this is one of the best popular expositions of Goedel theorem I’ve seen. Everything is very accurately explained, there are no silly mistakes and untruths one often sees mentioned in context of Goedel theorem, and even the original proof is sketched in a very approachable manner, striking a very good balance between getting across all crucial ideas, and skipping most of the distracting technical aspects (which are important and interesting, but I think only to mathematicians, haha). Great job all around.
- phaemon 6y agoWhat an excellent recommendation to the article. Thank you!
- stopachka 6y agoThis brought a big smile to read, thank you :)
- sillysaurusx 6y agoThere is an extraordinarily minor typo: “PM-LIsp” I point it out only because your work here is so good that it feels wrong not to smooth out any small splinters. Thank you for making this!
- irrational 6y ago> This proof showed that “1 + 1”, does indeed equal “2”. It took 2 volumes to get here. I know this seems logical to mathematicians, but it feels to me like having to take 2 volumes to prove something than any child knows intuitively is... I don't know what word I am looking for... obsessive?
- Twisol 6y agoYou can imagine "1 + 1 = 2" not as an important question in this context, but rather a proof of concept for the system they devised. It's a bit like the story about a "black triangle" [0]: a rather useless model passed through a rendering pipeline to produce a result any OpenGL novice can scramble in a couple dozen lines, but showing that the whole pipeline does, indeed, actually work as intended. [0] https://rampantgames.com/blog/?p=7745 https://rampantgames.com/blog/?p=7745
- FrozenVoid 6y agoThe idea is that 1+1 proof is made without the mathematical apparatus(High-level language) available after 1+1, i.e. its like a huge Assembler bootloader made from verified primitives(logical primitives) to load an operating system with High-level API(Mathemathics).
- leetcrew 6y agowe mostly live our lives as if P!=NP, but that does not detract from the importance of proving it.
- jandrese 6y agoThe point was to prove that math wasn't an arbitrary human construct, that it was rooted in the fundamental nature of reality.
- dddbbb 6y agoThey didn't set out to explicitly prove 1+1=2, they just got around to it after 2 volumes, it didn't require 2 volumes of background. A direct proof of 1+1=2 is pretty short in most logical systems.
- NoodleIncident 6y ago
- schoen 6y agoCf. Douglas Hofstadter's Metamagical Themas: > In March of 1977, I met the great AI pioneer Marvin Minsky for the first time. It was an unforgettable experience. One of the most memorable remarks he made to me was this one: "Gödel should just have thought up Lisp; it would have made the proof of his theorem much easier." I knew exactly what Minsky meant by that, I could see a grain of truth in it, and moreover I knew it had been made with tongue semi in cheek. Still, something about this remark drove me crazy. It made me itch to say a million things at once, and thus left me practically speechless. Finally today, after my seven-year itch, I will say some of the things I would have loved to say then. > [4 pages of detailed discussion of relationship between Gödel's methods and Lisp elided] > It was for all these reasons that Minsky's pseudo-joke struck my intellectual funnybone. One answer I wanted to make was: "I disagree: Gödel shouldn't have and couldn't have invented Lisp, because his work was a necessary precursor to the invention of Lisp, and anyway, he was out to destroy PM, not Lisp." Another answer was: "Your innuendo is wrong, because any type of reference has to be grounded in a code, and Gödel's way of doing it involved no more coding machinery grounding its referential capacity than any other efficient way would have." The final answer I badly wanted to blurt out was: "No, no, no—Gödel did invent Lisp!" You see why I was tongue-tied?
- deleted 6y ago[deleted]
- musicale 6y agoThat book helped me reach the conclusion that Hofstadter's self-references were annoying to the point that I wished to avoid them (and his writing in general) in the future.
- PartiallyTyped 6y agoI can't decide whether Gödel's method and Lisp are yet another Strange Loop [1]. Fortunately, I am still in the beginning. [1] https://www.goodreads.com/book/show/123471.I_Am_a_Strange_Loop https://www.goodreads.com/book/show/123471.I_Am_a_Strange_Lo...
- totemandtoken 6y agoDamn fine write up. Favorited this one, good job!
- stopachka 6y agoGlad you liked it, thank you :)
- andy-x 6y agoThanks for great write-up, fun to read! I only notices one tiny typo: "when apples are a fruit, then bananas or applies implies bananas or fruits" - "applies" should be "apples" I guess.
- gweinberg 6y agoAnd "pairs" should be "pears"!
- stopachka 6y agoWill address both, thanks team!
- wumms 6y agoTwo more typos: > These symbols map closely to the logical statements we are used too in programming. too => to > Hofstadter’s “I’m a Stange Loop” Stange => Strange
- stopachka 6y agoGreat catches! Updating now -- may take a few mins to show up
- vannevar 6y agoSomething I've always been curious about: does Gödel's theorem imply an infinity of inconsistent statements, or is the "this statement cannot be proven..." statement the only one? If it's the latter, then of what practical significance is the singularity? If a system is incomplete only in that regard, couldn't one redefine incompleteness to exclude it, and render the system complete for all practical purposes?
- lqet 6y agoFrom Wikipedia [0]: > The proof constructs a particular Gödel sentence for the system F, but there are infinitely many statements in the language of the system that share the same properties, such as the conjunction of the Gödel sentence and any logically valid sentence. [0] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#First_incompleteness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
- vannevar 6y agoYes, but the "such as..." example incorporates the original "this statement is not provable" statement, so it seems a bit of a cheat. If you could exclude that statement, it would also by definition exclude any compound versions of it. It seems to me that the issue boils down to, can "this statement is not provable" be leveraged to get to something like 1 + 1 = 3?
- Corazoor 6y agohttps://en.m.wikipedia.org/wiki/List_of_statements_independent_of_ZFC https://en.m.wikipedia.org/wiki/List_of_statements_independe... What Gödel did prove was that the above list of statements (and infinitely more) must exist. The special thing about his proof is indeed that it is recursive, i.e. adding another axiom can't fix the problem. But that was only necessary to prove that no formal system can be perfect, ever. Most undecidable problems can indeed be "fixed" by adding another axiom, but if you go beyond the ones of ZFC it becomes less clear which of the two alternatives is the "right" one...
- 6y ago
- jan_Inkepa 6y ago> For example, a gentleman called Frege discovered that he could craft a theory of sets, which could represent just about everything. For numbers, for example, he could do something like this: [ 0 is {}, 1 is {{}}, 2 is { {{}} {} }, etc. ] I don’t know Frege too well, but believe this is due to von Neumann, not Frege: https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_definition_of_ordinals https://en.wikipedia.org/wiki/Ordinal_number#Von_Neumann_def...
- libraryofbabel 6y agoCorrect. Frege (and then following him Bertrand Russell in Principia Mathematica) used a definition when a natural number n was the set of all sets with n elements. More info and contrast with the (later chronologically) Von Neumann definition: https://en.m.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers https://en.m.wikipedia.org/wiki/Set-theoretic_definition_of_...
- lqet 6y agoYou might be correct, Frege defined it (roughly) in a similar way, you can read his original publication here: https://ia800207.us.archive.org/22/items/diegrundlagende00freggoog/diegrundlagende00freggoog.pdf https://ia800207.us.archive.org/22/items/diegrundlagende00fr... It starts on book page 87, or PDF page 125. Basically, what he seems to be doing is to define 0 as the number of "everything that is not equal to itself" ("die Anzahl, welche dem Begriffe 'sich selbst ungleich' zukommt"), and 1 to be the number of "everything that is equal to 0" ("die Anzahl, welche dem Begriffe 'gleich 0' zukommt"), etc.
- jan_Inkepa 6y agoAh, yep, interesting! Thanks for the direct link. Ok, I wrote a long reply trying to figure out what exactly 2 is for him in terms of modern set theory notation, but I got really muddled. German’s not my mother-tongue/the pdf isn’t searchable, and when he says “Anzahl”/“Zahl” I’m never sure if he’s talking about size or abstract property, and would have to read a lot more of the book to figure out! [but naively: in §76 “n folgt in der natürlichen Zahlenreihe unmittelbar auf m.” is defined as “es giebt einen Begriff F und einen unter ihn fallenden Gegenstand x der Art, dass die Anzahl, welche dem Begriffe F zukommt, n ist, und dass die Anzahl, welche dem Begriffe ““unter F fallend aber nicht gleich x” zukommt, m ist””. “ is ‘n follows directly after m’ is defined as: there’s a preposition F and an object satisfying F such that the number of objects satisfying F is n and the number of objects satisfying “satisfying F but not x” is m. This really looks von Neumann like!] He also talks about numbers in §56 (but Zahlen, not Anzahlen)...with the problem of deciding in Julius Caesar is an (ordinal?) number or not, or whether anything has Julius Caesar as a number. [there’s also an english translation here http://www.naturalthinker.net/trl/texts/Frege,Gottlob/Frege,%20Gottlob%20-%20The%20Foundations%20of%20Arithmetic%20(1953)%202Ed_%207.0-2.5%20LotB.pdf http://www.naturalthinker.net/trl/texts/Frege,Gottlob/Frege,... but honestly it’s not much easier there :P ] ALL of this is confusing with what wikipedia says on the matter of defining natural number “Gottlob Frege and Bertrand Russell each proposed defining a natural number n as the collection of all sets with n elements.” - which may also be the case, but lacks a citation alas. https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers#Frege_and_Russell https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na... I don’t know if I have it in me to straighten this all out (that is, to RTFM).
- montebicyclelo 6y agoThis is really excellent. Amazing how much clearer the author’s Lisp code makes things (even to a non mathematician and non lisper). It’s rare to find explanations of difficult topics that are this well communicated, but I hope it becomes a trend.
- stopachka 6y agoThank you for the kind words! :)
- skrebbel 6y agoI agree and I want to add that I particularly appreciated how you consistently, in programming terms, communicated the type of things. Eg: (proves a b) So far saying “the sequence with the Gödel Number a proves the formula with Gödel Number b” In my experience, most mathematicians would have instead written "So far saying 'a proves b'". Repeating the type of the parameters consistently made it significantly easier for me to follow along. I hope this becomes more common.
- piyh 6y agoI read stuff like this on HN and feel like I'm an child watching dad work on a car. Except papa Godel was younger than me when he wrote his paper.
- baxtr 6y agoWho cares how old he was? Life is not a competition about age ;)
- odonnellryan 6y agoI am certain there are things you are better at then he was, and I'm certain there are things that could be found that you can do that he wish he could have done.
- ko27 6y agoJust to be clear. This implies that it's possible to write some specific statement (using PM axioms) that contradicts itself? Is there a readable example of this statement without using Gödel numbers but instead just with the axiom statements?
- thisiszilff 6y agoI don't think PM itself had any contradictions inside of it, rather there are statements composed of the PM langauge that aren't reached from the axioms selected by PM -- that is one of the sentences Godel demonstrates in his proof where he gets one that basically says "this statement has no proof in this system" (so if it does have a proof it is a contradiction, but if it doesn't have a proof then PM is an incomplete system). Someone else in the thread mentioned the continuum hypothesis as something that couldn't be proved from the standard ZFC axioms, so that would be an example of a statement without proof (incompleteness) albeit not in PM. I don't know of any contradictory statements.
- tildedave 6y agoThe continuum hypothesis is more like Euclid's parallel postulate than a Gödel sentence - assuming ZFC consistent there are models with CH true and CH false (the cardinality of the continuum doesn't have to be the first uncountable cardinal). Everything gets qualified with "assuming ZFC consistent" or "assuming Peano consistent" because any inconsistent theory proves any statement. More of a proof technicality than anything too profound. There is a construction of a model of Peano arithmetic, so it is consistent, as long as you accept the system used in the proof: https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof Not sure if this sheds light on the parent commentator's question ... the terminology can be quite tricky.
- ProfHewitt 6y agoYes, PM would be made inconsistent by including the [Gödel 1931] proposition I'mUnprovable for reasons explained elsewhere in this discussion. Fortunately, the rules on orders of propositions make it impossible to construct proposition I'mUnprovable in PM.
- vnjxk 6y agoI've been trying to understand it for so long and finally it's clear
- stopachka 6y agoGlad you enjoyed it! :)
- TheGrassyKnoll 6y agoHe used a word I don't see very often (if ever) https://en.wikipedia.org/wiki/Epiphenomenon https://en.wikipedia.org/wiki/Epiphenomenon
- 6gvONxR4sf7o 6y agoIf you format it that way (the spaces in front for a code block), we can't click the link.
- dang 6y agoI've fixed the formatting now.
- stopachka 6y agoIt's quite a fun effect! Hofstadter's claim that "I" (our conciousness) is an epiphenomena was very eye opening for me.
- dwohnitmok 6y agoThere are two things I will argue with on this otherwise great explanation. First, I've said this before and I'll bang this drum across every Godel post I see. Please don't introduce the notion of truth into an introductory post on Godel's Incompleteness Theorems (the Power of Numbers section). Introductory posts on Godel's Incompleteness Theorems like to say things like "there are true things you cannot prove" or in the case of this post "there are some truths that you can never write down as an algorithm." This is very nuanced and depends very heavily on what logical system you're in. To demonstrate how subtle this point is, there is also Godel's Completeness Theorem, which can informally be summarized as "all true statement are provable," and holds for most logical systems that mathematicians use, including those to which Godel's Incompleteness Theorems apply. The subtle point of course here is that "true" means something different in both contexts. This leads to the classic overly strong philosophical statements such as "For example, it may mean that we can’t write an algorithm that can think like a dog." That may be true, but it's not a direct consequence of Godel's Incompleteness Theorems. That's why in an introduction I strongly strongly recommend just sticking to incompleteness, i.e. the fact that you cannot have an exhaustive list of axioms. There will always be new axioms you can add. The second drum that I will keep banging on is that articles talking about how Godel's Incompleteness Theorems show that a system S cannot prove its own consistency and stop there miss the significance of this statement. Usually, like in this article, they go in the "opposite" direction by saying S can't prove itself, so maybe you could try using a more powerful S' to prove S, but then you couldn't prove S', and so you need an S'' to prove the consistency of S', and so on and so forth in an infinite regress. But we actually care about the opposite direction: using S to prove the consistency of S' and then using S' to prove the consistency of S'' and so on. That is we don't actually care about using S to prove its own consistency because if we were ever doubtful of S's consistency, we wouldn't trust any proof it produced, let alone a proof of its own consistency. Rather what is important is that we cannot prove the consistency of the stronger S' in the weaker S, since if we were able to prove the consistency of S', then we could definitely prove the consistency of the weaker S. This is the fatal blow to Hilbert's program. Hilbert was perfectly fine with having to assume the consistency of some logical system. His hope was something akin to a "trusted computing base" that if you assumed was consistent could then prove the consistency of all other more complex systems. Ideally this "trusted computing base" could be quite small, but it wouldn't necessarily have to be, as long as there was some definite size after which we could stop having to take consistency on faith. Godel's consistency result implies that this trusted computing base cannot exist! There is no minimal base whose consistency, when taken on faith, is enough to prove the consistency of other systems we care about. That is we care about the opposite direction: S can't prove the consistency of S, so it can't prove the consistency of the larger S', so it can't prove the consistency of the still larger S'', and so on. Now again there's some nuance here. We know that Con(S) is independent of S and in turn Con(S + Con(S)) is independent of S + Con(S) etc. but we also somehow know how to "collapse" this whole hierarchy if we know that S is consistent (the formalization of this intuition requires a deeper dive into model theory), so something is a little bit off here. Moreover stuff like Gentzen's proof of the consistency Peano Arithmetic demonstrate there is some more wiggle room in exactly what it means for a system to be logically stronger than another system. But the most straightforward, naive way of trying to use a single trusted computing base to prove the consistency of everything else will fail.
- madia_leva 6y agoShouldn't you use 2 for a '(' instead of 1?
- madia_leva 6y agoNevermind, my mistake
- Konohamaru 6y agoHere's how I interpret Gödel's landmark result: > semantic properties, except for the most trivial systems, can't be inferred from syntactic properties. E.g. you can't type a program by seeing everything is using the correct literals and syntactic objects: you need to, sooner or later, know what the program /actually does/. But the problem is that mathematicians do, in fact, reason about semantics. So saying that "it's uncomputable" ignores the elephant in the room, which is that mathematicians compute theorems for a living. What do mathematicians have that enables them to compute the uncomputable: well-aligned chakras, magic, coffee grounds, the zodiac, etc...?
- dwohnitmok 6y agoArgh... this is the nuance I was talking about in another post. Godel's Completeness Theorem (which applies to many systems that Godel's Incompleteness Theorem also applies to) shows that in a sense semantic properties coincide with syntactic properties and so in fact can exactly be inferred from syntactic properties. What instead Godel's Incompleteness Theorems show is that you cannot exhaustively list all the semantic properties of what you care about, but combined with Godel's Completeness Theorems, only the ones "relevant" to your syntactic axioms.
- Konohamaru 6y agoThis interpretation can't be correct, because Rice's Theorem says that no semantic property of any computer program is computable.
- dwohnitmok 6y agoMore nuance is needed; Rice's Theorem says that there is no formula for deciding any semantic property of an arbitrary computer program. Restricted classes of computer programs are totally fine, and in some sense that is exactly what a logical system is: a description of a restricted class of programs. But this is also getting a bit confusing because there are many different interpretations of how to tie computability to a logical system. For example the proof system of first-order logic can be interpreted as a single Turing machine program, not a family of ones, for which it is very possible to make all sorts of judgments about its semantic consequences.
- Bud 6y agoThis is an exceptionally good explanation of Gödel's incompleteness theorem for the general reader.
- stopachka 6y agoThank you, glad you liked it :)
- drran 6y agoWell, I disliked it. I see proof that every valid formula can be converted into a Godel number. However, every invalid formula can also be converted into a Godel number. So, if we are able to construct a number, then it proves what?
- arc0 6y agoThe conversion of formulae to Gödel numbers is basically an implementation detail, the fact it can be done allows us to define theorems on the natural numbers that describe properties of the logical system. Encoding an invalid formula is of course possible, but I don't see why that would be a problem, it doesn't inherently 'prove' anything.
- drran 6y agoFor me, it looks like use a program in C to generate a C code, and then prove that a C program can generate an invalid C code, so the C compiler must be invalid. Compilation step is missed. Compiler will refuse to compile the invalid code. IMHO, the same situation is for Godel numbers. We can use math to generate numbers, which are equivalent to formulas, BUT why these formulas must be accepted? Initial set of axioms was carefully chosen by human, so it not an open set, where anybody can add anything.
- arc0 6y agoGödel's proof does not apply to any single axiomatic system, it applies to any computable set of axioms that can talk about numbers, quantifiers, addition and multiplication. This isn't arbitrary, it's a set of properties required for just about any interesting mathematics to take place. The formulae are accepted because Gödel gives us a mapping, he proves that we can convert any formula into a number without losing information.
- 1970-01-01 6y agoVery off-topic, but long ago when Albert Einstein went for a car ride with Mr. Gödel to become U.S. citizens, Einstein was trying very hard to think of ways to shut him up about a Constitution loophole he discovered. Things didn't go exactly as planned, and in front of the naturalization examiner, Mr. Gödel started blabbing about how he had found a way the U.S could be transformed into a fascist regime... Sources: https://robert.accettura.com/wp-content/uploads/2010/10/Morgenstern_onGoedelcitizenship.pdf https://robert.accettura.com/wp-content/uploads/2010/10/Morg... https://en.wikipedia.org/wiki/Kurt_Gödel#cite_note-23 https://en.wikipedia.org/wiki/Kurt_Gödel#cite_note-23
- anonymousDan 6y agoIn light of current circumstances this story has actually been on my mind! Has there ever been any more detail revealed about Godel's scheme?
- schoen 6y agoThere is some more information at https://jeffreykegler.github.io/personal/morgenstern.html https://jeffreykegler.github.io/personal/morgenstern.html There's also an article about this question at https://papers.ssrn.com/sol3/papers.cfm?abstract_id=2010183 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=2010183
- kfarr 6y agoThanks the second one finally answered the question: In summary, Gödel’s loophole is that the amendment procedures set forth in Article V self-apply to the constitutional statements in Article V themselves, including the entrenchment clauses in Article V. Furthermore, not only may Article V itself be amended, but it may also be amended in a downward direction (i.e., through an “anti-entrenchment” amendment making it easier to amend the Constitution). Lastly, the Gödelian problem of self-amendment or anti-entrenchment is unsolvable. In addition, the author identifies some “non-Gödelian” flaws or “design defects” in the Constitution and explains why most of these miscellaneous design defects are non-Gödelian or non-logical flaws.
- dwohnitmok 6y agoI thought I replied to this post, but I guess not and my reply ended up being a top-level reply, which is just as well. I will just mention my main two quibbles to this otherwise excellent post and others like it so that other people who embark on introductory posts to Godel's results don't fall into the same trap. 1. Please don't bring the notion of truth into an introductory explanation (such as in the section "Power of Numbers" or in the short intro to "Hilbert's Program"). It makes it very confusing, especially in light of Godel's other landmark result, i.e Godel's Completeness Theorem which simultaneously applies to many of the same logical systems and can be very very vaguely described as "all true things are provable." Just stick to incompleteness and consistency at a syntactic level instead of appealing to truth, that is respectively the ability to always add new axioms and the lack of syntactic contradictions. 2. The lack of a system S's ability to prove its own consistency is not interesting by itself since we would not trust a proof from a potentially inconsistent system. Hence it is not, in a sense, terribly interesting that we require an infinite tower of increasingly stronger systems to prove the consistency of S and themselves. Rather the interesting direction goes the other way. S cannot prove the consistency of stronger systems, which means we cannot have a "minimal" system we use to explore the consistency of all other systems (again subject to some nuance).
- xyzzyz 6y ago> It makes it very confusing, especially in light of Godel's other landmark result, i.e Godel's Completeness Theorem which simultaneously applies to many of the same logical systems and can be very very vaguely described as "all true things are provable." If people want to understand how to reconcile this very vague statement with Goedel incompleteness theorem that appears to say that some "true" statements are in fact not provable, here's the rough idea: we distinguish between "theories", which live in syntactic world, and "models", which are meant to represent semantics. Theories are like specification of an interface of a programing module, and models are actual implementation of said modules. If one can implement an interface to satisfy all requirements of the specification (that is, all the axioms and theorem that the axioms entail), existence of such implementation shows that the specification is self-consistent: in math, we say that theories that have a model are consistent. What Goedel's completeness theorem says is the converse: consistent theories always have a model; in programming talk, non-contradictory specification can always be implemented. Here's why it means that "all true things are provable": if something is supposed to be true fact about the theory, it has be a property of every model of said theory, that's the lowest bar for any notion of "truth" to make sense. But, one can easily show, using Goedel's completeness theorem, that if something is true in every model of the theory, it has to be provable: indeed, suppose that statement f is true in every model of theory T, but is actually not provable from T. We can then extend theory T by statement "not f", and the resulting theory T' = {T, "not f"} is still consistent, because for it to be inconsistent means exactly that T could prove both "not f" and "not (not f)", and the latter is equivalent f, which we assumed T cannot prove. Then, Goedel's completeness theorem says that this extended theory, since it's consistent, must have a model, M'. But, a model of this extend theory T' is also a model of basic theory T; if you implement larger specification, your implementation also implements any subset of it. But f was supposed to be true in every model of T, and so f is true in M', but also "not f" is true in M', which is a contradiction. Hence, f must be provable from T. Why it doesn't conflict with Goedel's in-completeness theorem? After all, the Goedel's sentence constructed in the proof of Goedel's incompleteness theorem is supposed to express something true but not provable. Well, the idea is that it is not true of the theory of natural numbers, but it's true of the particular model of natural numbers that we have in mind when we think of what natural numbers are, the so called standard model of natural numbers, where all of the numbers are of the form 0 and, using OPs notation (next (next (next ... (next 0) ... )). As it turns out, there exist other models of natural numbers, which have extra, "non-standard" natural numbers which are not of that form, numbers you cannot reach by just applying successor operation finite number of times starting from 0. These models are really weird, but they still must abide all provable rules of the behavior of natural numbers. One can still add them, there must be some "prime" non-standard numbers that aren't products of any smaller numbers, the non-standard numbers must also split into unique product of prime numbers (some of which must necessarily also be non-standard), and so on. This is all crazy, and can make your mind twist, so only think about it at your own peril. To sum up, the notion of "truth" with respect to theories coincides with provability, but not so when you start talking about things true in particular models. This means that we cannot describe all true things about specific models, and in particular about standard natural numbers, using standard logic, but if something does follow from the theory and is true in every of its models, it is in fact provable.
- LifeIsBio 6y agoLoving this so far! One tiny typo that threw me for a loop for a second was: > when apples are a fruit, then bananas or applies implies bananas or fruits which should be: > when apples are a fruit, then bananas or apples implies bananas or fruits
- scanr 6y agoI really like the conversion to a representation that's more familiar but I suspect it's also confusing me. Here are the questions that I have to start: Does 'there-is' evaluate to a boolean (is boolean a thing? is evaluation a thing?) I was surprised that the axioms don't use there-is but I sense I shouldn't be? what does '(when 0 (or 0 1))' mean, it's described as 'when 0, then there is either 0 or 1' but I'm not sure what that means? is '(when 0 0)' true and '(when 1 0)' false? Why not use '(when A B)' as equals? Not a question but in the axioms I assume pairs should be pears and applies should be apples. How goes 'implies' get introduced by '(when (when q r) (when (or p q) (or p r))'? Also, this introduces a category in the example i.e. fruits but not sure how that happened. Why do we need to have second '(not (factor? x 3^22 ...))', isn't it sufficient to say that (factor? x 3^21 ...) to establish that the 2nd term is 'there-is'?
- ghayes 6y agoI took these to mean the existential operator and the implication operator, but I agree they were insufficiently defined for me, esp. as we're building from first principles. The post could have made the early proofs more obvious in how they were constructed (e.g. how the language is really used to prove statements).
- ReaLNero 6y agoFor existential quantification, we use the `there-is` function. Meanwhile, for universal quantification, we... just mention the variable. This intuitively makes sense: `there-is` is a restriction on a variable (the restriction is that there is at least one value for that variable). Meanwhile, the absence of restrictions implies universal quantification. Specifying universal quantification like this is quite common in math proofs, and it's not too bad to get used to.
- iHegazy 6y agoSuper awesome read, a great book about computability is "the annotated turing".
- stopachka 6y agoGlad you enjoyed it! :)
- junon 6y agoMinor formatting gripe: the first inline citation (superscript 1) looks like an exponent given that it's right after a numeric constant in an equation. It made me re-parse the sentence a few times before realizing it.
- cmonnow 6y agoI never understood the fascination people have with self-referential 'paradoxes' like : "This statement is False". Pronouns do not have an independent existence. Until the pronoun 'This' resolves to an actual statement which has a valid true/false property, it is a recurrence without termination i.e. a infinite loop, that has no meaning. Suppose I say: 1. Sky is blue. 2. Previous statement is True. 3. Previous statement is True. And ask you 'Is Statement 3 is True or False?'. You would say 'First I need to know what 'previous' refers to', so you would do pronoun substitution for the word 'Previous' in Statement 3: 3. 'Previous statement is True' is True. Since this statement has an unresolved pronoun, you would do pronoun substitution for the word 'Previous' in Statement 2: 3. ''Sky is blue' statement is True' is True. Since there are no more unresolved pronouns, you would evaluate the statement 'Sky is blue', and then the next Statement 2, and finally Statement 3, and say 'Yes, Statement 3 is True'. So far, so good ? Now, suppose I say: 1. This statement is False. And ask you 'Is Statement 1 True or False?'. You would say 'First I need to know what 'This' refers to', so you would do pronoun substitution for the word 'This' in Statement 1: 1. 'This statement is False' statement is False. Since this statement has an unresolved pronoun ('This'), you would do pronoun substitution again. - ''This statement is False' statement is False' statement is False. Since this statement has an unresolved pronoun ('This'), you would do pronoun substitution once more. - '''This statement is False' statement is False' statement is False' statement is False' And you will keep doing pronoun substitutions forever since statements with unresolved pronouns cannot have a True/False property. I find this teenage-girl-at-a-rock-concert-feigned-fascination with self-referential 'paradoxes' silly.
- musicale 6y agoWell, the liar paradox dates to antiquity, the halting problem has been well known for 70+ years, etc., and yet.... it turns out we can still use logic and software to solve lots of practical problems anyway, simply by avoiding self-referential contradictions and infinite loops. Arithmetic seems to have a number (so to speak) of practical applications as well. Perhaps it's a bit like theory vs. practice, or maybe mathematics vs. engineering.
- redvenom 6y agoPeople have a fascination with "This sentence is false" because it highlights the need to be precise distinguishing between the language of a logical system and a metalanguage to talk about the language. That discovery or 'invention' if you will is something that was not put into rigorous foundation until the 20th century.
- sudoaza 6y agoWas this successor? function ever implemented? I'm quite skeptic. Wouldn't there be infinite possible successors? Are all of them mechanistically derivable?
- amboo7 6y agoLispers learned marketing, bravo! The only issue is the missing credit to the Quanta article https://www.quantamagazine.org/how-godels-incompleteness-theorems-work-20200714 https://www.quantamagazine.org/how-godels-incompleteness-the....
- stopachka 6y agoThat's pretty rude of you. I didn't read that essay, but I did reference about 4 essays / books that I did read :). Went through the quanta article -- it seems reasonably different (doesn't go deep on how proof, subst, work, etc) -- I suspect the similarities stem from both of us reading Nagel and Newman's book.
- ProfHewitt 6y agoHi Amboo7! The article "What Gödel Discovered" improves on the Quanta article linked above by using Lisp expressions instead of Gödel numbers. The proof in "What Gödel Discovered" is still incorrect because the Lisp expressions it uses leave out the crucial orders on propositions in Russell's Principia Mathematica.
- turndown 6y agoI thought this was an amazing article; thank you for writing it.
- stopachka 6y agoThank you for the kind words :)
- ajnin 6y agoVery interesting. I'm wondering if this has implications in physics ? Since "the book of nature is written in mathematical language", does this mean that attempts to find a unified theory of everything are doomed ? I'm thinking not necessarily, since we wouldn't need to prove all possible physical phenomena, only those that actually happen, but how do we know if they are among the one that can be proven ?
- toyg 6y agoThe implications are really on the concept of language. It proves that there is no language that can be complete; as such, we cannot express a complete system, even if it existed. So a unified theory of everything might well exist, but you wouldn’t be able to describe it. Which is a nice philosophical riddle.
- yonixw 6y agoI think that if you allow some axioms, you can describe it. But I'm not sure if it will be called complete. I think because "(next axiom)" is not defined, it will make your language not mappable to integer numbers and you avoid Godel proof.
- ProfHewitt 6y agoA very comprehensive theory of physics including the physics of computation can be developed. However, such a foundational theory will be inferentially undecidable.
- lokedhs 6y agoNice article, I do like the way it's explained in a way that a programmer like myself can understand it. I did note a few typos that I will take the opportunity to report here, in order to make an already great article a little better: Under "PM-Lisp Axioms": Looking at the code "(when (or p q) (or (q p))". I don't think the (q p) should have parens around it. Under "(proves a b)": There is no ending quote at the end of the last sentence. Under "(subst a b c)": I find the text "PM-LIsp". I guess the I should be lower case.
- stopachka 6y agoThank you for taking the time! Updated -- should take a few mins to show up :)
- thwoasy9024 6y agoCool! I've always loved the sort of nihilism of the incompleteness theorems
- thrwoasy8473 6y agoThanks for the post. It is great seeing it written out (kind of like structure and interpretation of classical mechanics).
- stopachka 6y agoThank you for the kind message : )
- kazinator 6y agoThis article spectacularly misses a big chunk of the point of Lisp, by applying Gödel-numbering to the printed representation of the syntax, rather than to the object that it denotes.
- dexterlagan 6y agoThis is exactly what came to my mind as I was reading this article. Would it make a difference if it was applied to syntax objects?
- ProfHewitt 6y agoContrary to popular opinion, [Gödel 1931] did not actually prove inferential undecidability (sometimes called "inferential incompleteness") of Russell's Principia Mathematica for the reasons explained here: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 The article linked above gives a correct proof of inferential incompleteness.
- pythiccoder5 6y agoIn college and high school I spent years trying to understand these theorems I wish I had had this explanation then. This is the paper I wrote on the subject https://mdsoar.org/handle/11603/2249?show=full https://mdsoar.org/handle/11603/2249?show=full.
- deleted 6y ago[deleted]
- mensetmanusman 6y agoThis is amazing. Two thoughts: 1) It seems that the black/white formalism of ‘ a statement can be only true or false ‘ causes issues. Have people tried introducing additional options for verifiability, e.g. ‘true / false / maybe?’ or something that points to uncertainty à la Heisenberg? 2) It would be really interesting for the author to continue the line of reasoning to help add insight to Gödel’s ontological proof. ( https://en.m.wikipedia.org/wiki/Gödel%27s_ontological_proof https://en.m.wikipedia.org/wiki/Gödel%27s_ontological_proof )
- ianandrich 6y agoApparently someone had the following thought. "Everyone when faced with the dilemma of having either an unsound or incomplete formal system chooses incompleteness. What happens when we allow for unsoundness and treat this notion as first class?" There has been a slow burn on paraconsistent logics going back to the 80s or so now. https://en.wikipedia.org/wiki/Paraconsistent_logic https://en.wikipedia.org/wiki/Paraconsistent_logic I seem to recall at least one where one of the states was something analogous to a maybe/don't know.
- vcdimension 6y agoTYPO!!: In the section "Suspicious use of subst" it says that b is being replaced, but in the second formula box a has been replaced, not b. Furthermore the number that replaced a is not the same as the number used in the previous subst statement.
- stopachka 6y agoGreat catch! Updated : ) -- should take a few mins to show up
- Liron 6y agoPeople act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it to behave differently based on its own conclusion about its behavior. What if I ask you to predict whether you’re going to go left or right, but I also tell you that I’m going to force you to go the opposite direction as what you predict? Then the set of things you can accurately predict is Incomplete. But that’s not a profound limitation of human consciousness, it’s just the familiar paradox of any fortune teller or time travel scenarios.
- daralthus 6y agoBecause of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".
- skoll43 6y agoat the end: maybe not even wrong
- Liron 6y ago> Because of the halting issue you cannot summarise reality into a set of axioms and rules Conway's Game of Life is a kind of reality summarized into axioms and rules, and most likely our universe/multiverse is on track to being similarly summarized. The halting issue doesn't get in the way of that achievement... Once you have the intuition for why the Halting Problem (i.e. fortune teller paradox) is obvious, then Godel's proof is just an XSS attack on axiom systems whose designers think they're only "about numbers", like how CSS is designed to be about styling but it's also Turing-complete and vulnerable to XSS. Russel and Whitehead were trying to simultaneously (1) invent a system capable of proving highly insightful claims about the infinite space of numbers, like "there doesn't exist a number between 1 and infinity with property P" but (2) not a system that can encode a Turing-equivalent agent that creates paradoxes if it tries to predict its own future. Godel was just the first to point out that condition (2) was already met just by supporting Peano Arithmetic, the same way a modern computer science undergrad can point out that CSS is Turing-complete or your regex-based HTML validator is vulnerable to XSS attacks.
- barrenko 6y agoOh, author is friends with Sebastian Marshall, that explains a thing or two :).
- stopachka 6y agoIndeed, we worked together in China, and have been friends since :)
- ozankabak 6y agoSo if we have a theory expressive enough to make statements about ordinary (Peano) arithmetic, we can always form a self-referential statement within the framework of this theory which we can not prove or disprove. So far, so good. Here is my question: What happens if we restrict/weaken the theory to preclude self-referential statements? Obviously, we will lose our ability to express certain arithmetic statements which correspond to self-referential statements in the original theory. But what else? Is that the only class of statements we lose? Also, are there any other kinds of statements that still make the theory incomplete?
- Sharlin 6y agoWe lose the ability to reason about sets of unbounded size. As long as we only restrict ourselves to some bounded subset of integers, Gödel can't do the trick with his numerals. Equivalently, on the CS side, we must restrict ourselves to total functions, that is, all valid programs must provably halt after some bounded number of steps.
- Gehinnn 6y agoIt is very hard to detect self-referential statements and restricting yourself to "non-self-referential statements" might be quite severe. Given a set of "domino" tiles - each having a top and a bottom. Each top and bottom has some word on it - these words can only use the letters "a" and "b". You can duplicate domino tiles and also align tiles so that all tops and all bottoms are aligned. Now, given a finite set of such tiles, can you say whether there is an alignment so that all tops concatenated, read from right to left, equal all bottoms concatenated? In fact, given such a set of tiles S, you can easily create a formula P(S) that is true iff such a valid alignment does not exist. Obviously this formula is true for some sets of tiles and false for others. Now the funny thing: Given a (correct) fixed theory T in which you can state P(S) for every S and in which proofs can be computationally checked, there must be infinitely many S so that P(S) is true, but cannot be proved in T. Thus such theory T is incomplete. Where is the self-reference? This problem is also known as the Post correspondence problem (PCP). The halting problem can be reduced to it, which is not decidable. If T was complete, you could enumerating all proofs and see whether they correctly proof P(S) or its negation. Due to its completeness you would eventually find a proof for either of them and thus you could decide the halting problem.
- posed 6y agoJust imagine the number of times the author has used the word "imagine", lol.
- hvis 6y agoI've read Godel, Escher, Bach, and I've read this. It's a very nice explanation. But everywhere I see, Godel's theorem is touted as some kind of deep philosophical insight, whereas from what I understand, informally it could be rephrased as "if you have a usable language for mathematical proofs, some phrases in that language must be neither true nor false (i.e. nonsensical)". Nonsensical phrases in our human languages in nothing new, so the conclusion becomes that much less exciting. Though I'm sure it's valuable for fundamental math theory.
- nmg 6y agoTo me reading this article it was striking to consider the relationship between language and (mathematicsl/logical) truth this way. In my mind it correlates with the quantum phenomenon that observing something fundamentally alters its state.
- nmadden 6y agoIt’s not so much that they’re neither true nor false (they’re not paradoxes), but that they can be true in some interpretations and false in others. I wrote up some notes about this here: https://neilmadden.blog/2020/11/17/some-incomplete-thoughts-about-godel/ https://neilmadden.blog/2020/11/17/some-incomplete-thoughts-...
- hvis 6y agoWasn't that proof using a paradox, though? Then that basically really proves the existence of paradoxes. It doesn't disprove the existence of all other kinds of statements, of course. A statement 'x == 1' might be contextual (with a free variable x), but I think the theory is talking more about statements like for all x (x + 1)^ 2 == x^2 + 2*x + 1 which is true and does not depend on x. Contrast that with for all x x == 1 which is obviously false. But the proof outlined in the article constructed a statement with a free variable, where a substitution with a certain value leads to a statement which is neither true, nor false. That means that the general statement in the proof's example is neither true nor false either. Sorry about the awkward terminology, BTW, my engineering degree was a decade ago and in a language other than English.
- JesseMeyer 6y ago"This meant that no formal system, could prove by itself, that it could only produce true statements. " I see this generalization often, that Godel showed that all formal systems share this restriction, but doesn't the formal system have to be at least be able to express the properties of integers? Is the ability to formally express integers relatively a particularly demanding constraint on choice of axioms?
- deleted 6y ago[deleted]
- deanCommie 6y agoSomething that is never clear to me - what defines what is an axiom and what is derived from the axiom? In Russel's PM, `(when (or p p) p)` is considered an axiom, but `=` isn't, and is derived from the other axioms. But...why not the reverse? The axiom "when either apples or apples, then apples" just seems like another way to state "apples = apples". Why is that not the axiom that other things follow from, then?
- ir123 6y agoSome things that were not clear to me, can some one help me out with them? 1) While representing 1+1 = 2 i.e (= (+ (next 0) (next 0)) (next (next 0))) which comes at the start of this article, is this considered to be just a statement? Or a true statement that follows from the axioms? 2) On formulas, this example is shown (there-is a (= (next 0) a)). It is not clear whether this is a necessarily true statement or some symbols relating a and 0. 3) He says that proofs are a sequence of formulas but colloquially they are sequence of "implications". That "implication" is introduced later on and it is shown that this "implication" symbol also needs to be proved (successor). Didn't he use the fact that one thing implies another multiple times previously? I need the distinction amongst "statement", "formula" and "axioms". Apologies if the above looks like a vegetable soup but I'd love some explanation for this.
- ir123 6y agoWhats the difference amongst formula, statement, proof and successor?
- ProfHewitt 6y agoThe author of "What Gödel Discovered" has a good point that Gödel numbers are not a convenient representation of a proposition of Russell's Principia Mathematica (PM). (Nor are Gödel numbers adequate because they omit the order of a proposition.) Lisp expressions are an improvement. However, a Lisp expression, as used in the article, is also not adequate because it also omits the order of the proposition. See the following for a high-level representation of propositions of PM that includes the crucial orders on proportions: https://papers.ssrn.com/abstract=3459566 https://papers.ssrn.com/abstract=3459566