8 ms·
Gödel's Completeness Theorem
- kkylin 7y agoAnyone interested in this topic should be sure to follow the various links on the page. One of my personal favorites is the Compactness Theorem: https://en.wikipedia.org/wiki/Compactness_theorem https://en.wikipedia.org/wiki/Compactness_theorem .
- phab 7y agoDouglas Hofstadter's book, "Gödel, Escher, Bach" is very highly recommended reading for anyone who finds this (and the theory of computability more generally) interesting. I've lost entire days of my life to that book! https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach
- danielneri 7y agoOne more related recommendation would be James Gleick's Chaos book: https://en.wikipedia.org/wiki/Chaos:_Making_a_New_Science https://en.wikipedia.org/wiki/Chaos:_Making_a_New_Science It is a good introduction to Chaos Theory and complexity science and a nice read alongside GEB.
- theWheez 7y agoI'm 100 or so pages in to this now. What a book! I'm sure this will be a long time classic for me.
- wellpast 7y agoHere's a good adjacent read that I thought was a much clearer and relatively accessible tour through the Proof - https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081... - it's more of a pamphlet than a book, really.
- jerf 7y agoGEB is fun, but it's definitely a bad introduction to the idea itself. It's a lot more fun if you already understand the subject matter and can enjoy the tone of the book.
- aerovistae 7y agoGodel's work has always been incomprehensible to me. no matter how I attempt to understand his theorems, I find them impenetrable. Apparently they are of great consequence, so I'm very interested, but to no avail.
- headshock1111 7y agoI was the same until I watched this: https://www.youtube.com/watch?v=V9ohtKameio https://www.youtube.com/watch?v=V9ohtKameio
- rwill128 7y agoI can relate. My understanding of it thus far leads me to think I can summarize it fairly well though, and I would welcome other people's input or critique on this. It seems like it's so consequential because he demonstrated that no matter what kind of mathematical system you're using -- and no matter how much mathematics generally speaking develops -- there will be objectively true mathematical statements within that system that can't be proven. If that part of my understanding is correct, the part that's really interesting to me is whether we can know these true statements to be true, despite them not having proofs. This is where I could be misunderstanding things I suppose, but it suggests there's a disconnect between what's knowable and what's provable, and furthermore, that we can know more than we can prove. To actual seasoned mathematicians: is this a really naive interpretation of what I've read, or not?
- SomeOldThrow 7y ago> If that part of my understanding is correct, the part that's really interesting to me is whether we can know these true statements to be true, despite them not having proofs. There may be proofs, just using different fundamental axioms. The finding is that there is no initial set of axioms that by themselves allow proving all provable truths.
- xamuel 7y agoYou need to be a bit more specific: no matter what kind of true, computable axiom-set you're using (this has nothing to do with 'how much mathematics generally speaking develops'), there will be objectively true mathematical statements that can't be proven by that axiom-set. >a disconnect between what's knowable and what's provable "what's provable [from a given axiom-set]" is a concrete, technical, unambiguously defined set of things. "what's knowable" is a vague philosophical set of things. Goedel's Incompleteness Theorem is a technical result about the former, and it's a common mistake to assume it says anything about the latter, except very tangentially. For those who are interested in the misty area where the two things do overlap, I will shamelessly plug this 2-page paper of mine, "Mathematical shortcomings in a simulated universe": https://philpapers.org/archive/ALEMSI.pdf https://philpapers.org/archive/ALEMSI.pdf
- adamnemecek 7y agoThe theorem reminds me of William Lawvere's "Adjointness in foundations". Formulas/programs are in an adjoint relationship with their executions. The fact that they are adjoints is a big deal.
- theWheez 7y agoIs that related to the Curry-Howard isomorphism?
- 120bits 7y agoOh my! this reminds me of a class I took in my masters. Had to learn "Halting Problem". Godel's work in just astonishing and way beyond my caliber. I managed to pass the class but memories are still with me.
- jandrese 7y agoI still think most CS courses teach the Halting Problem in just about the worst way possible. They always give you that one highly contrived counterexample where you're feeding the algorithm with the output from itself which doesn't even begin to touch on what the Halting Problem actually is or why it is so important. And if the student asks "well, what if we redefine it so it only works on OTHER algorithms to avoid this one weird edge case" the answer is basically "that's not covered." But really, the Halting Problem is asking the question if we can solve all of mathematics, and indeed all of philosophy with a fancy enough computer program. Can we build a machine God? And the standard textbook answer is roughly "If we built a machine God it could create a burrito so big that even it could not eat it, therefore machine God can not exist." IMHO, it would make more sense to get students down the right path to ask them what the halting computer would do when fed a program that calculates all of the digits of Pi. Or one that halts when it computes the answer to life, the universe, and everything. The halting problem may have been mathematically disproven by finding one highly convoluted counter example, but it's more significant failing is that it is infinite and thus can not be implemented on a machine with finite limits.
- cyphar 7y ago> The halting problem may have been mathematically disproven by finding one highly convoluted counter example, but it's more significant failing is that it is infinite and thus can not be implemented on a machine with finite limits. I agree that would be a better way to teach it, but Turing machines have infinitely-long tapes -- the really unexpected result is that you couldn't solve the Halting Problem even if you had (countably) infinite tape and infinite time to do it. The same probably holds for uncountably-infinite tapes too (the "burrito" counterexample still breaks it), though you can't really address a tape that long for obvious reasons.
- 7y ago
- theWheez 7y agoThis theorem actually changed my life. Once it clicked for me it shifted my understanding of reality significantly.
- vga805 7y agoCan you expand on this, I am quite curious.
- theWheez 7y agoThis, alongside the second incompleteness theorem, showed me that any formal system cannot prove itself, and any system deemed "consistent" can only be considered as such from outside that system. A great way that I visualize it (thanks to Hofstadter) is like Escher's never ending staircase painting. If you look at each step, it looks just fine. In fact, you can say that each step on its own is "consistent". But it is only when you take a step back, outside the system of each isolated step, that you see the paradox. Similarly, the theorem applies this to mathematics, and by extent, any formal system. Just as we can see each "step" going from one to the next, in mathematics we must hold an axiom as truth without proof, so that subsequent theorems may use it as the next "step". It is, in a sense, a paradox which we agree to use. In practical terms, I may extrapolate that further and more philosophically than was intended (or that I have commonly seen), but the subsequent Halting Problem combined with the Curry-Howard isomorphism shows me that Godel's Theorem has major real world effects. The idea that there can be something that is true but not provable rings true to me in many regards. I, like many, spend nearly every moment of the day unconsciously putting faith into the "truth" that I am not alone in the universe, thereby fending off solipsism. I cannot prove "I" exist. But it is true. What are the other truths that cannot be proven? That question guides my thinking.
- psychometry 7y agoThe FIT is a statement about finitary number theory. Even Godel, who was an ardent platonist, wouldn't try to extrapolate it to philosophy.
- bulatb 7y agoThis theorem seems to be like monads: Someone posts about it on the internet, someone doesn't understand and asks for help, someone comes along and writes a simple explanation that seems to make sense, then someone says that explanation is completely wrong (but here's this totally inscrutable "correct" one... which someone comes along and says is even worse.) And everyone is left confused.
- anaphor 7y agoJust read this book, IMO https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081... It's only 160 pages and gives what seems to be a good explanation of the basics.
- novalis78 7y agoCurrently reading Morris Kline’s “Loss of certainty” - a beautiful very readable work that elucidates the relationship of Mathematics with concepts of ‘truth’ and ‘reality’ throughout mathematical history. https://www.amazon.com/dp/0195030850/ref=cm_sw_r_cp_api_i_aJ.BDb2XFHVCA https://www.amazon.com/dp/0195030850/ref=cm_sw_r_cp_api_i_aJ...
- theWheez 7y agoLike monads, I think the issue comes from "frames" of thinking. You cannot understand monads in terms of functions as is understood in most languages. You also can't understand it in terms of its common uses like I/O. Yes, it can be applied in those domains, but it is like explaining the internet with electricity.
- adamnemecek 7y agoFunny that you mention this, you can construct monads with this in some sense. GCT talks about adjointness (it's analogous to William Levwere's work "adjointness in foundations"). One can build monads from adjoint functors. http://www.stephendiehl.com/posts/adjunctions.html http://www.stephendiehl.com/posts/adjunctions.html
- bulatb 7y ago
- tabtab 7y agoWhat are practical consequences and examples of such in typical debates about politics, programming paradigms, etc?
- psychometry 7y agoThere aren't any. These theorems apply to specific systems in finitary number theory with certain axioms. They're important, but they're important in mathematical logic, not rhetoric or anything like that.
- lacker 7y agoOne practical consequence is that the halting problem is undecidable, so if your boss asks you to build a program to check if another program will ever do X, you can tell them "hey that's an impossible task!"
- jmcqk6 7y agoIn practical matters, this is not quite true. If you ask 'will this program launch a toaster to orbit mars', you can usually answer that question with high confidence. The halting problem describes the situations where you can't decide one way or another, but it does not say you can't decide anything. This is a very important distinction. We write code to analyze other code all the type. It's a core part of developer tools. If it was impossible, life would really suck.
- triska 7y agoRegarding programming paradigms, at least one very important consequence of the completeness theorem is that first-order logic can be used as a formal basis for computation. This is because you can model what a Turing machine does via predicates in first-order logic, describing a relation between states of the machine. The completeness theorem tells us that every semantic consequence of a first-order theory (with a well-orderable language) can be derived syntactically. This means that to derive results of the computation, we only have to systematically search for proofs. Due to the completeness theorem, we know that we won't miss anything (i.e., a result of the computation) that is actually the case. An immediate application is an important programming paradigm called logic programming. See for example Prolog, Mercury, and other languages that are based on this idea.
- wrp 7y agoGodel's theorems are a popular subject among technophiles, but the popular conception of their implications is seriously off base. Torkel Franzen's book[1] is a quick read and will guide you away from the most common errors. [1] https://www.amazon.com/G%C3%B6dels-Theorem-Torkel-Franz%C3%A9n/dp/1568812388/ https://www.amazon.com/G%C3%B6dels-Theorem-Torkel-Franz%C3%A...
- adamnemecek 7y agoMost people talk about incompleteness theorem, not completeness. The book does briefly mention completeness theorem.
- gigabytes 7y agoGuys, this is the completeness theorem, not the incompleteness theorem.
- lacker 7y agoIMHO if you understand the history it makes sense why the theorem is both important and confusing. In 1921, Hilbert had this idea, that mathematicians could create an algorithm that would automatically prove every true statement and disprove every false statement. Wouldn't that be neat? It's important that this idea predates computers. When Hilbert was thinking about an algorithm, it wasn't an algorithm as we would think about it in computer science today, because the modern idea of a computer hadn't been formalized. In 1931, Godel proved that it was impossible for an algorithm to automatically prove or disprove true mathematical statements. Take that, Hilbert. The modern idea of a computer still hadn't been formalized. So a lot of stuff that nowadays we think of as simple, Godel did in a really weird and confusing way. For example, as part of his proof Godel needed a way to algorithmically encode a bunch of numbers into a single number. Nowadays, that's pretty intuitive - any software program can be saved into a file, any file can be interpreted as a sequence of binary bits, which can be interpreted as a number. Back then, Godel used a really crazy encoding - encoding (a, b, c, d, ...) as 2^a * 3^b * 5^c etc. So if you go back and try to understand Godel's proof, it is really just needlessly complicated. I loved the book Godel, Escher, Bach when I first read it, but once I understood the mathematics more deeply I started thinking that it really wasn't the best approach to actually understand the mathematics. In 1936, Turing defined a Turing machine and also proved that the halting problem was undecidable. This is an equivalent statement to Godel's incompleteness theorem, and the proof is about 100 times more intuitive, especially for modern computer programmers who tend understand computers and computer programs pretty well, far better than they understand prime factorization. So, personally I think if you are learning this stuff, you are better off starting by learning about the halting problem. Sometimes the historical sequence of discovery isn't the best way to learn math, just like we don't learn about the Greek method of exhaustion before we learn modern methods of calculus.
- deleted 7y ago[deleted]
- dwohnitmok 7y agoThis is not Godel's incompleteness theorem(s). This deals with a completely different notion of completeness. Godel's completeness theorem is the theoretical justification for why first-order logic occupies such an important position in mathematical logic. It basically establishes that two different methods of proving a logical statement happen to coincide for first-order logic. Let's say that I come up with a long list of axioms that define what it means for an object to be a "cow" and what it means to have a "spot." Then I state "all cows have spots." There are two ways of proving this. One way, the "semantic" way, is to take every example of cow and prove that it has a spot. This is hard; I not only have to examine every cow that exists, I have to examine every possible imaginary entity that satisfies the definition of "cow" and prove that it has a spot. The second way, the "syntactic" way, is to play the string manipulation game that people often associate with the notion of a "logical proof." I start out with the axioms of a "cow," and I'm given some rules for how I can manipulate these axioms. Example of this include the string "A and B" allows me to immediately substitute "A" instead. Given "A implies C" I can substitute all instances of "A" with "C" and so on and so forth. Hopefully I can work out a series of string manipulation steps that eventually end with the statement "All cows have spots." It is not obvious that these two methods should coincide in what they are able to prove. The rule set that I get to manipulate my strings by could be a really wacky set of rules. Maybe it says something like if you see "A implies B," you get to substitute any arbitrary string "C." It's also not apparent how you might choose to interpret the axioms that define a "cow." One of the axioms might say "a cow has four legs" and you might say, in my world, I've decided the string "four" corresponds to the natural number 5, and I'm going to look at all entities with 5 legs. Godel's completeness theorem states that for first-order logic these two proof techniques coincide: every statement you can prove or disprove the first way can also be proved or disproved the second way. More specifically, if you stipulate that rules of string manipulation are exactly the rules of deduction in first-order logic, and that you interpret your axioms when constructing semantic entities according to the standard semantics of first-order logic (e.g. you don't get to arbitrarily stipulate that the string "and" actually means logical disjunction, i.e. or, in your world), then any property that is true of every entity you can conjure up that satisfies your axioms has a "string manipulation" proof that proves that property. Conversely, every statement you can prove with your string manipulation game also holds true of every entity you can conjure up that satisfies your axioms (this isn't strictly speaking part of the completeness theorem, but is also true and usually stated hand-in-hand with it).