10 ms·

Gödel's Incompleteness Theorems (2015)

161 points by mutor 10y ago

threepipeproblm 10y ago
I took a full semester course on Godel's Incompleteness Theorems in college and found it rewarding. It was one of those experiences that convinced me that hand-wavy familiarity with stuff sometimes pales by contrast to a deep dive. One of the professors also had a very old newspaper clipping taped up (it was brown then and that was quite a while ago), about several mathematicians committing suicide in the wake of those proofs. I've looked for corroboration of this and have never found it. A bit difficult to comprehend from a modern perspective, but more plausible with an appreciation of the 19th Century faith in rationalism / logical positivism that Godel helped overturn. Not many people are aware that Godel spent much of his life secretly working on a modern update of an ontological argument for God's existence, and didn't reveal this until late in life -- https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_proof https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_pro...
- MichaelOtte 10y ago
  Though not a proof of the existence of God as worked on by Godel, but Al Platinga is known for his work for the logical discussion of the rationality or religious belief Somewhat related excerpt: https://www.princeton.edu/~hhalvors/restricted/plantinga-ReasonandBelief.pdf https://www.princeton.edu/~hhalvors/restricted/plantinga-Rea...
  - cousin_it 10y ago
    Plantinga is known for his proof of God's existence, and in fact a proof of any sentence you like, using the modal logic operators of possibility and necessity: "possibly necessarily pigs fly, therefore pigs fly". (Where "possibly" is shorthand for "in some possible world", and "necessarily" is shorthand for "in all possible worlds".) It's a valid proof if you buy the assumption, but the assumption is dubious at best.
    - dvt 10y ago
      Of course it's valid! A world-renowned philosopher like Plantinga wouldn't publish a proof that's not valid. That's like saying Dijkstra's code compiles :) The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise. E.g.: the possibility of a maximally great being seems to definitionally imply its necessity. Why? Because such a being B must have some properties P = { ? ? ? ... }. We may not be sure what's inside P, but we know, with absolute certainty, that existence is in there. Kant would disagree. He thinks that existence is not a property. This is a rare case when I think he's right.
      - throwaway729 10y ago
        > The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise But that is also true of the informal rhetorical arguments that are more common in (christian) apologetics. The gift of formal proofs is that they make explicit and unavoidable this embedding of conclusion in premise, which is fundamental to all (epistemologically rational) apologetics
        dvt 10y ago
        > this embedding of conclusion in premise [...] is fundamental to all (epistemologically rational) apologetics It might be true of all ontological arguments, but certainly not all apologetic arguments.
      - naasking 10y ago
        > E.g.: the possibility of a maximally great being seems to definitionally imply its necessity. One of my favourite tongue-in-cheeek replies I read to these ontological arguments: Ah, but surely there is no greater being than one who could create the universe despite not existing!
    - nthcolumn 10y ago
      What is it he has proven the existence of? Can he describe it? Can anyone... please?
- pizza 10y ago
  Godel's god is already a github repo! https://github.com/FormalTheology/GoedelGod https://github.com/FormalTheology/GoedelGod Now we just wait for someone to code a proof of Erdos' Supreme Fascist..
- qwert-e 10y ago
  As far as I know it's not like the proofs caused a wave of suicides, but mathematicians studying this topic often became mentally unstable, including Godel (who starved himself in a sanatorium) and others like Georg Cantor. I'm curious where you studied; I also took a semester course on "logic and computability" where the main text we read was 'Godel, Escher, Bach'
  - dvt 10y ago
    I studied at UCLA and also took several logic and metalogic classes (it was my AOF). For one of the metalogic classes, this was our text: http://www.math.ucla.edu/~dam/135.07w/135notes.pdf http://www.math.ucla.edu/~dam/135.07w/135notes.pdf We briefly talked about Godel's proofs, but they are nontrivial. Henkin's proof of completeness is hard enough[1]. I don't mean to sound dismissive, but a class where Godel, Escher, Bach is the text does not seem very rigorous. Logic is very tricky stuff. And once you get into infinities, it's not even intuitive. [1] https://www.cs.nmsu.edu/historical-projects/Projects/completeness.pdf https://www.cs.nmsu.edu/historical-projects/Projects/complet...
  - threepipeproblm 10y ago
    This article referenced some guys jumping off buildings... maybe it was more of the journalist's interpretation, connecting the sort of thing you mentioned with the suicides in a less direct way than I recall. I have wondered if it was a real news clipping (it looked like one), or some kind of old joke. To answer your question, I went to one of the so-called "elite" American colleges that still has a primarily classical/analytic philosophy program (as opposed to what is known as a "Continental" program). Would rather not say which one, but I was able to take some great logic courses through the philo department. We used Godel's work directly, and if memory serves also some Goldfarb.
  - Solheim 10y ago
    I also took a Computability course. We used: https://www.amazon.com/Computability-Logic-George-S-Boolos/dp/0521389232 https://www.amazon.com/Computability-Logic-George-S-Boolos/d...
okket 10y ago
A non-mathematical interpretation of Gödels Theorems and their implications http://rationalwiki.org/wiki/G%C3%B6del's_incompleteness_theorems http://rationalwiki.org/wiki/G%C3%B6del's_incompleteness_the...
curuinor 10y ago
Carl Hewitt (of Actor model fame) has this thing where he claims that contradiction alone allows you to defeat Godel Incompleteness, so he shops it around places and everyone's like, "man, wtf, this isn't how that works". I saw him shop it to D. Hofstadter and Hofstadter basically smiled and took the little piece of paper and threw it away when Carl wasn't looking. This doesn't have anything to do with anything, just a thing that happened
- wfn 10y ago
  I know that the above was written in jest anyway :) but just for completeness (har), a contradiction would help you defeat many things (i.e., it's not specific to incompleteness theorems, so to speak), because given it, (at least in traditional logic) you can prove anything. This is trivial and known, but to spell it out, if we have a contradiction formalized by p and not p (given), we can prove that q: 1. p and not p (given). 2. p (from 1). 3. not p (from 1). 4. p or q (from 2 (disjunction introduction)). 5. q (from 3 and 4). So obviously this would upset quite a few things around :) that said, the interesting stuff is with Graham Priest's (et al.) paraconsistent logic systems wherein your system can tolerate a contradiction without exploding in whole. And (so the story goes) those systems may offer an actual insight into handling incompleteness (while still being usable). If anyone has looked into this more, would be interesting to hear about it!
  - jesuslop 10y ago
    That behaviour was desribed by the old masters as 'ex falso quodlibet': from falsity whatever (when else am i having the chance to be this pedantic). In the uni I was taught that hippie-era AI dealt with that with things called non-monotonic reasoning, abduction, truth maintenance systems.
    - dvt 10y ago
      Also known as the (much cooler-sounding) Principle of Explosion :)
  - brenderup 10y ago
matt_morgan 10y ago
If you're interested in this and you haven't read Logicomix, https://en.wikipedia.org/wiki/Logicomix https://en.wikipedia.org/wiki/Logicomix get it at your library now. http://www.worldcat.org/title/logicomix/oclc/708346776&referer=brief_results http://www.worldcat.org/title/logicomix/oclc/708346776&refer...
- osullivj 10y ago
  Great comic book treatment of the Frege - Russell - Godel story. Strongly recommended.
  - Y_Y 10y ago
    They do mention this in the book, but it does take artistic license with some of the history.
danharaj 10y ago
Goedel's results imply some surprising and counterintuitive things about our formal models of computability: https://johncarlosbaez.wordpress.com/2016/04/02/computing-the-uncomputable/ https://johncarlosbaez.wordpress.com/2016/04/02/computing-th...
- pizza 10y ago
  Enjoyed rereading this, thanks
maskedinvader 10y ago
I recently read 'Incompleteness: The Proof and Paradox of Kurt Gödel' by Rebecca Goldstein [1], I highly recommend it for those interested in learning more about his life and the proof itself. 1.https://smile.amazon.com/Incompleteness-Proof-Paradox-G%C3%B6del-Discoveries/dp/0393327604/ https://smile.amazon.com/Incompleteness-Proof-Paradox-G%C3%B...
rb1 10y ago
Just chipping in with my interesting reading about the implications of Godel's incompleteness theorems. This piece about what the theorem means for developing "deep AI" and the human mind, was a fascinating eye opener for me, about the far stretching implications of the theorem. "The Lucas-Penrose Argument about Gödel's Theorem" - http://www.iep.utm.edu/lp-argue/ http://www.iep.utm.edu/lp-argue/
- clairity 10y ago
  penrose wrote a whole book walking through his argument around deep AI (and providing a gentle explanation of gödel's incompleteness theorem in the process): https://en.wikipedia.org/wiki/The_Emperor%27s_New_Mind https://en.wikipedia.org/wiki/The_Emperor%27s_New_Mind
laxd 10y ago
"A common misunderstanding is to interpret Gödel's first theorem as showing that there are truths that cannot be proved." I've heard it stated that confusing way so many times in popular media. And then often follows quantum mechanics, and geniuses going mad, and the world is just your imagination... forever.
- saguiar 10y ago
  Agreed it has been abused. On the other hand, if you adhere to a computational theory of mind and see the mind as computation over a formal system, then it is saying something about the mind and the fact that some (true) sentences cannot be proven in that system, isn't it? It is a big if though. (though maybe in a completely irrelevant sense of truth).
  - deleted 10y ago
    [deleted]
  - laxd 10y ago
    Just poking fun at the way these things are presented in pop.sci. media. Anyway, talking over my head, I'm not shure formal systems are a good way of modelling the mind itself. Formal systems are (usually) considered consistent. The mind is not. Neither are neural nets. And it's interesting how neural nets, and other statistical models/algorithms that drop the requirement of always beeing right, seems more much more capable in certain practical matters.
  - eli_gottlieb 10y ago
    >see the mind as computation over a formal system Wow, is that what people actually think a "computational theory of mind" is? Look, just because every program can be trivially rewritten as some kind of formal proof system, doesn't mean that any given program meaningfully has the semantics of a formal proof system, let alone the mind.
dataphyte 10y ago
I recommend Torkel Franzén's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. It is readable without sacrificing rigor. It is especially good at ensuring the reader doesn't come away infected with the pseudo-profound BS that plagues many discussions of the Gödel's Theorems.
- theoh 10y ago
  That, and Nagel's book on the proof, have been recommended on HN before (very recently!). And Rebecca Goldstein's book has been dismissed as too hand-wavy. For important, wiki-friendly topics like this one, HN is frustratingly not great for building a readily checkable/cumulative knowledge base, rather than encouraging a forgetful herd discussion that goes around in circles. It is as I say frustrating for anyone who wants long-term knowledge rather than flimsy "news".
  - Jun8 10y ago
    Very apt obeservation! I was thinking on how to address that for some time. Any ideas? Would you like to collaborate on this?
crypto5 10y ago
I always was wondering: Godel proved his theorem regarding formal systems described in Principia Mathematics. In my understanding this is some higher level logic with recursive functions. But how this can be extended to the whole universe of all possible formal systems? Who guarantee that there will be no some new system with quantum-oracle-operator, which will not be affected by incompleteness theorem, and can self-proof self-consistency? Even well known m-recursive functions (which are essentially Turing machines) are wider class than primitive recursive functions used in the proof..
- martincmartin 10y ago
  It says "any system which includes the Peano axioms is either inconsistent or incomplete." So having a wider class doesn't help, if it contains the Peano axioms.
  - crypto5 10y ago
    Proof was made within specific framework, with very specific quantors and type of inference, I still don't understand how it prevents existence of more powerful frameworks with different quantors and inference where incompleteness theorems wouldn't work.
    - eli_gottlieb 10y ago
      You can construct a new Incompleteness Theorem for any more powerful formal system. To really get syntactic completeness, you would need an infinite tower of Goedel Statements as axioms, where the truth of each one is a completely independent mathematical fact not reducible to any other axiom ever. Effectively, syntactic completeness in logic is equivalent to the Halting Problem in computing, via bijective proofs.
      - crypto5 10y ago
        Let me give you example. At first you have predicate calculus, and Godel completeness Theorem. Now you add new tool: existence predicate, and you got first order logic, which allows you to prove Godel's incompleteness Theorem. What is the guarantee exactly that more advanced systems can't exist? Say system with new 'quantum hack' operator. You can't prove formula from Godel's proof? 'Quantum hack' under some conditions covers missing gap in proof path by building continuum truth table and give you tool to check if formula from Godel's proof actually provable, or it is false.
quizotic 10y ago
When I rant about it, I claim his theorem says "any system that reference parts of itself is either incomplete or inconsistent," and that the universe is such a system, as we're a part of it, and refer to parts of it. So therefore, the universe is either full of magic (in a system with inconsistency, anything can happen), or mystery (there are true things that we can never prove). My belief is that the quest to find a unified physics that describes everything is provably impossible due to Godel's theorem. And on the rare occasions when I look for evidence of God, the fact that one of the things we can know for sure - is that we can't know everything - provides about as much comfort as I need.
- petegrif 10y ago
  This sort of application is wildly out of bounds of the true scope of the theory. The relationship between physics (unified or otherwise) can't be resolved with reference to Godel's theorems.
  - quizotic 10y ago
    Why? I honestly don't see how it's out of scope at all (majored in mathematics, minored in physics)
    - mrbrowning 10y ago
      Well, you're actually making metaphysical claims more than mathematical or physical ones. One of two assumptions, depending on how literally the sentiment that the universe is a formal system is intended, is being elided here: 1. That the universe _is_ a formal system, rather than being describable in the language of some formal system. It's not evident what the universe being a formal system even means, or how it squares with basic intuition regarding e.g. the fact that physical systems have state. 2. That, dropping the physical system <=> formal system equivalence and given some real system R consisting of some fundamental entities whose behaviors can be described in full in the language of some formal system S, (borrowing a useful construct from Lucas' anti-mechanism argument, even though I don't buy that argument) no machine can be constructed in R which computes theorems of some formal system S' in which all true statements of S are provable, meaning that no state of the system R can be said to contain a description of S', and that S' is therefore not describable by any arrangement of the entities in R (assuming some reasonable predicate over states of R that is true for a state when some arrangement of a subset of the entities in that state describes S'). Intuitively, this doesn't seem to hold up: by analogy, I can describe a universal Turing machine with a computer equipped with only finite memory. You could then attempt to go down the road of claiming that, even if a description of S' is possible in R, that a mind within R would not be capable of formulating that description, but then you're heaping on an even larger tangle of assumptions, unknowns, and things you have to define if you're going to argue the case rigorously. The point being that confidence about _any_ hypothesis about the nature of reality made on the basis of Gödel's incompleteness theorems is not epistemologically warranted.
cousin_it 10y ago
Here's a nice way to make peace with Godel's theorems. Let's say your beliefs about the integers can be summarized by some formal theory T. ("Every number has a successor", and so on, until your intuition runs out of things to say.) Now Godel jumps out of the bushes and says aha, your T doesn't include Con(T), so you aren't the math genius that you thought you were! But let's stop for a moment and consider what it would take for T to include Con(T). First of all, compared to other sentences about integers that you believe, Con(T) is an absolutely huge sentence. It must contain an arithmetization of all of T (encoding the axioms, inference rules, etc. into integer arithmetic). Second of all, if Con(T) is included in T while speaking about T, it might need to include an arithmetization of Con(T) itself! That uses a diagonal construction ("quine" in computer science terms), making the sentence even bigger. Now you're looking at some kind of hundred-kilobyte Diophantine equation, with no intuitive reason to believe it at all. And third of all, it's easy to see that an inconsistent theory T would easily prove Con(T) (because it proves any sentence), so having Con(T) inside T doesn't even give you any positive evidence for trusting T. In fact, we're lucky to live in a world where Godel's theorems are true, and having Con(T) inside T is negative evidence instead of none at all!
- vilhelm_s 10y ago
  I wonder if anyone has written out a Gödel sentence in full as a statement about numbers in English. It would be fun to see how big it gets. Also, the comment about size and diagonalization is interesting. The Gödel sentence from the first incompleteness theorem is made by diagonalizing, while the sentence from the second incompleteness theorem is just "Con(T)", so the sentence from the 2nd theorem is shorter and more natural if written out in full---making it even more disappointing that it's not provable. Indeed, if we put in more work we should be able to prove a more interesting theorem, but I never really thought about it before.
- Certhas 10y ago
  To some degree Chaitlin's equations [1] make the issue less abstract than that though. "We outline our construction of a single equation involving only addition, multiplication, and exponentiation of non-negative integer constants and variables with the following remarkable property. One of the variables is considered to be a parameter. Take the parameter to be 0, 1, 2, ... obtaining an infinite series of equations from the original one. Consider the question of whether each of the derived equations has finitely or infinitely many non-negative integer solutions. The original equation is constructed in such a manner that the answers to these questions about the derived equations are independent mathematical facts that cannot be compressed into any finite set of axioms." So there are finite (though several hundred pages long) equations for which the finiteness of the solution set is independent of every finite axiomatization of arithmetic. So suddenly, even though the formula is enormous, the type of sentence is perfectly normal. Does f(x) have finitely many solutions, where f(x) is built from addition, multiplication and exponentiation. Much more so than Gödel’s incompleteness this deeply violates my intuition about what type of statements should be decidable. [1] https://www.cs.auckland.ac.nz/~chaitin/berlin.pdf https://www.cs.auckland.ac.nz/~chaitin/berlin.pdf
psyc 10y ago
This isn't really about Gödel, but I always wish that people had a little bit less of a natural instinct towards bastardized Gödelian thinking. So that there would be fewer infuriating people arguing things like "Infringing on my right to infringe on the rights of others infringes on my rights." Or, "You can't be against criticism, because then you'd be criticizing criticism." I've been rolling my eyes at these arguments for decades, and I wish fewer people thought they were clever.
jchassoul 10y ago
Wittgenstein bitches!
cantagi 10y ago
I am halfway through reading Raymond Smullyan: A puzzle guide to Gödel, after finding out about his recent death here: https://news.ycombinator.com/item?id=13626221 https://news.ycombinator.com/item?id=13626221 . It explains Godel's incompleteness Theorems accurately to a layperson through a set of logical puzzles.

161 points by mutor 10y ago

I took a full semester course on Godel's Incompleteness Theorems in college and found it rewarding. It was one of those experiences that convinced me that hand-wavy familiarity with stuff sometimes pales by contrast to a deep dive. One of the professors also had a very old newspaper clipping taped up (it was brown then and that was quite a while ago), about several mathematicians committing suicide in the wake of those proofs. I've looked for corroboration of this and have never found it. A bit difficult to comprehend from a modern perspective, but more plausible with an appreciation of the 19th Century faith in rationalism / logical positivism that Godel helped overturn. Not many people are aware that Godel spent much of his life secretly working on a modern update of an ontological argument for God's existence, and didn't reveal this until late in life -- https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_proof https://en.wikipedia.org/wiki/G%C3%B6del%27s_ontological_pro...

MichaelOtte 10y ago
Though not a proof of the existence of God as worked on by Godel, but Al Platinga is known for his work for the logical discussion of the rationality or religious belief Somewhat related excerpt: https://www.princeton.edu/~hhalvors/restricted/plantinga-ReasonandBelief.pdf https://www.princeton.edu/~hhalvors/restricted/plantinga-Rea...
- cousin_it 10y ago
  Plantinga is known for his proof of God's existence, and in fact a proof of any sentence you like, using the modal logic operators of possibility and necessity: "possibly necessarily pigs fly, therefore pigs fly". (Where "possibly" is shorthand for "in some possible world", and "necessarily" is shorthand for "in all possible worlds".) It's a valid proof if you buy the assumption, but the assumption is dubious at best.
  - dvt 10y ago
    Of course it's valid! A world-renowned philosopher like Plantinga wouldn't publish a proof that's not valid. That's like saying Dijkstra's code compiles :) The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise. E.g.: the possibility of a maximally great being seems to definitionally imply its necessity. Why? Because such a being B must have some properties P = { ? ? ? ... }. We may not be sure what's inside P, but we know, with absolute certainty, that existence is in there. Kant would disagree. He thinks that existence is not a property. This is a rare case when I think he's right.
    - throwaway729 10y ago
      > The main problem with ontological arguments (and why, even as a Christian, I don't like them) is because they seem to embed the conclusion in their first premise But that is also true of the informal rhetorical arguments that are more common in (christian) apologetics. The gift of formal proofs is that they make explicit and unavoidable this embedding of conclusion in premise, which is fundamental to all (epistemologically rational) apologetics
      - dvt 10y ago
        > this embedding of conclusion in premise [...] is fundamental to all (epistemologically rational) apologetics It might be true of all ontological arguments, but certainly not all apologetic arguments.
    - naasking 10y ago
      > E.g.: the possibility of a maximally great being seems to definitionally imply its necessity. One of my favourite tongue-in-cheeek replies I read to these ontological arguments: Ah, but surely there is no greater being than one who could create the universe despite not existing!
  - nthcolumn 10y ago
    What is it he has proven the existence of? Can he describe it? Can anyone... please?
pizza 10y ago
Godel's god is already a github repo! https://github.com/FormalTheology/GoedelGod https://github.com/FormalTheology/GoedelGod Now we just wait for someone to code a proof of Erdos' Supreme Fascist..
qwert-e 10y ago
As far as I know it's not like the proofs caused a wave of suicides, but mathematicians studying this topic often became mentally unstable, including Godel (who starved himself in a sanatorium) and others like Georg Cantor. I'm curious where you studied; I also took a semester course on "logic and computability" where the main text we read was 'Godel, Escher, Bach'
- dvt 10y ago
  I studied at UCLA and also took several logic and metalogic classes (it was my AOF). For one of the metalogic classes, this was our text: http://www.math.ucla.edu/~dam/135.07w/135notes.pdf http://www.math.ucla.edu/~dam/135.07w/135notes.pdf We briefly talked about Godel's proofs, but they are nontrivial. Henkin's proof of completeness is hard enough[1]. I don't mean to sound dismissive, but a class where Godel, Escher, Bach is the text does not seem very rigorous. Logic is very tricky stuff. And once you get into infinities, it's not even intuitive. [1] https://www.cs.nmsu.edu/historical-projects/Projects/completeness.pdf https://www.cs.nmsu.edu/historical-projects/Projects/complet...
- threepipeproblm 10y ago
  This article referenced some guys jumping off buildings... maybe it was more of the journalist's interpretation, connecting the sort of thing you mentioned with the suicides in a less direct way than I recall. I have wondered if it was a real news clipping (it looked like one), or some kind of old joke. To answer your question, I went to one of the so-called "elite" American colleges that still has a primarily classical/analytic philosophy program (as opposed to what is known as a "Continental" program). Would rather not say which one, but I was able to take some great logic courses through the philo department. We used Godel's work directly, and if memory serves also some Goldfarb.
- Solheim 10y ago
  I also took a Computability course. We used: https://www.amazon.com/Computability-Logic-George-S-Boolos/dp/0521389232 https://www.amazon.com/Computability-Logic-George-S-Boolos/d...

okket 10y ago

A non-mathematical interpretation of Gödels Theorems and their implications http://rationalwiki.org/wiki/G%C3%B6del's_incompleteness_theorems http://rationalwiki.org/wiki/G%C3%B6del's_incompleteness_the...

curuinor 10y ago

Carl Hewitt (of Actor model fame) has this thing where he claims that contradiction alone allows you to defeat Godel Incompleteness, so he shops it around places and everyone's like, "man, wtf, this isn't how that works". I saw him shop it to D. Hofstadter and Hofstadter basically smiled and took the little piece of paper and threw it away when Carl wasn't looking. This doesn't have anything to do with anything, just a thing that happened

wfn 10y ago
I know that the above was written in jest anyway :) but just for completeness (har), a contradiction would help you defeat many things (i.e., it's not specific to incompleteness theorems, so to speak), because given it, (at least in traditional logic) you can prove anything. This is trivial and known, but to spell it out, if we have a contradiction formalized by p and not p (given), we can prove that q: 1. p and not p (given). 2. p (from 1). 3. not p (from 1). 4. p or q (from 2 (disjunction introduction)). 5. q (from 3 and 4). So obviously this would upset quite a few things around :) that said, the interesting stuff is with Graham Priest's (et al.) paraconsistent logic systems wherein your system can tolerate a contradiction without exploding in whole. And (so the story goes) those systems may offer an actual insight into handling incompleteness (while still being usable). If anyone has looked into this more, would be interesting to hear about it!
- jesuslop 10y ago
  That behaviour was desribed by the old masters as 'ex falso quodlibet': from falsity whatever (when else am i having the chance to be this pedantic). In the uni I was taught that hippie-era AI dealt with that with things called non-monotonic reasoning, abduction, truth maintenance systems.
  - dvt 10y ago
    Also known as the (much cooler-sounding) Principle of Explosion :)
- brenderup 10y ago

matt_morgan 10y ago

If you're interested in this and you haven't read Logicomix, https://en.wikipedia.org/wiki/Logicomix https://en.wikipedia.org/wiki/Logicomix get it at your library now. http://www.worldcat.org/title/logicomix/oclc/708346776&referer=brief_results http://www.worldcat.org/title/logicomix/oclc/708346776&refer...

osullivj 10y ago
Great comic book treatment of the Frege - Russell - Godel story. Strongly recommended.
- Y_Y 10y ago
  They do mention this in the book, but it does take artistic license with some of the history.

danharaj 10y ago

Goedel's results imply some surprising and counterintuitive things about our formal models of computability: https://johncarlosbaez.wordpress.com/2016/04/02/computing-the-uncomputable/ https://johncarlosbaez.wordpress.com/2016/04/02/computing-th...

pizza 10y ago
Enjoyed rereading this, thanks

maskedinvader 10y ago

I recently read 'Incompleteness: The Proof and Paradox of Kurt Gödel' by Rebecca Goldstein [1], I highly recommend it for those interested in learning more about his life and the proof itself. 1.https://smile.amazon.com/Incompleteness-Proof-Paradox-G%C3%B6del-Discoveries/dp/0393327604/ https://smile.amazon.com/Incompleteness-Proof-Paradox-G%C3%B...

rb1 10y ago

Just chipping in with my interesting reading about the implications of Godel's incompleteness theorems. This piece about what the theorem means for developing "deep AI" and the human mind, was a fascinating eye opener for me, about the far stretching implications of the theorem. "The Lucas-Penrose Argument about Gödel's Theorem" - http://www.iep.utm.edu/lp-argue/ http://www.iep.utm.edu/lp-argue/

clairity 10y ago
penrose wrote a whole book walking through his argument around deep AI (and providing a gentle explanation of gödel's incompleteness theorem in the process): https://en.wikipedia.org/wiki/The_Emperor%27s_New_Mind https://en.wikipedia.org/wiki/The_Emperor%27s_New_Mind

laxd 10y ago

"A common misunderstanding is to interpret Gödel's first theorem as showing that there are truths that cannot be proved." I've heard it stated that confusing way so many times in popular media. And then often follows quantum mechanics, and geniuses going mad, and the world is just your imagination... forever.

saguiar 10y ago
Agreed it has been abused. On the other hand, if you adhere to a computational theory of mind and see the mind as computation over a formal system, then it is saying something about the mind and the fact that some (true) sentences cannot be proven in that system, isn't it? It is a big if though. (though maybe in a completely irrelevant sense of truth).
- deleted 10y ago
  [deleted]
- laxd 10y ago
  Just poking fun at the way these things are presented in pop.sci. media. Anyway, talking over my head, I'm not shure formal systems are a good way of modelling the mind itself. Formal systems are (usually) considered consistent. The mind is not. Neither are neural nets. And it's interesting how neural nets, and other statistical models/algorithms that drop the requirement of always beeing right, seems more much more capable in certain practical matters.
- eli_gottlieb 10y ago
  >see the mind as computation over a formal system Wow, is that what people actually think a "computational theory of mind" is? Look, just because every program can be trivially rewritten as some kind of formal proof system, doesn't mean that any given program meaningfully has the semantics of a formal proof system, let alone the mind.

dataphyte 10y ago

I recommend Torkel Franzén's Gödel's Theorem: An Incomplete Guide to Its Use and Abuse. It is readable without sacrificing rigor. It is especially good at ensuring the reader doesn't come away infected with the pseudo-profound BS that plagues many discussions of the Gödel's Theorems.

theoh 10y ago
That, and Nagel's book on the proof, have been recommended on HN before (very recently!). And Rebecca Goldstein's book has been dismissed as too hand-wavy. For important, wiki-friendly topics like this one, HN is frustratingly not great for building a readily checkable/cumulative knowledge base, rather than encouraging a forgetful herd discussion that goes around in circles. It is as I say frustrating for anyone who wants long-term knowledge rather than flimsy "news".
- Jun8 10y ago
  Very apt obeservation! I was thinking on how to address that for some time. Any ideas? Would you like to collaborate on this?

crypto5 10y ago

I always was wondering: Godel proved his theorem regarding formal systems described in Principia Mathematics. In my understanding this is some higher level logic with recursive functions. But how this can be extended to the whole universe of all possible formal systems? Who guarantee that there will be no some new system with quantum-oracle-operator, which will not be affected by incompleteness theorem, and can self-proof self-consistency? Even well known m-recursive functions (which are essentially Turing machines) are wider class than primitive recursive functions used in the proof..

martincmartin 10y ago
It says "any system which includes the Peano axioms is either inconsistent or incomplete." So having a wider class doesn't help, if it contains the Peano axioms.
- crypto5 10y ago
  Proof was made within specific framework, with very specific quantors and type of inference, I still don't understand how it prevents existence of more powerful frameworks with different quantors and inference where incompleteness theorems wouldn't work.
  - eli_gottlieb 10y ago
    You can construct a new Incompleteness Theorem for any more powerful formal system. To really get syntactic completeness, you would need an infinite tower of Goedel Statements as axioms, where the truth of each one is a completely independent mathematical fact not reducible to any other axiom ever. Effectively, syntactic completeness in logic is equivalent to the Halting Problem in computing, via bijective proofs.
    - crypto5 10y ago
      Let me give you example. At first you have predicate calculus, and Godel completeness Theorem. Now you add new tool: existence predicate, and you got first order logic, which allows you to prove Godel's incompleteness Theorem. What is the guarantee exactly that more advanced systems can't exist? Say system with new 'quantum hack' operator. You can't prove formula from Godel's proof? 'Quantum hack' under some conditions covers missing gap in proof path by building continuum truth table and give you tool to check if formula from Godel's proof actually provable, or it is false.

quizotic 10y ago

When I rant about it, I claim his theorem says "any system that reference parts of itself is either incomplete or inconsistent," and that the universe is such a system, as we're a part of it, and refer to parts of it. So therefore, the universe is either full of magic (in a system with inconsistency, anything can happen), or mystery (there are true things that we can never prove). My belief is that the quest to find a unified physics that describes everything is provably impossible due to Godel's theorem. And on the rare occasions when I look for evidence of God, the fact that one of the things we can know for sure - is that we can't know everything - provides about as much comfort as I need.

petegrif 10y ago
This sort of application is wildly out of bounds of the true scope of the theory. The relationship between physics (unified or otherwise) can't be resolved with reference to Godel's theorems.
- quizotic 10y ago
  Why? I honestly don't see how it's out of scope at all (majored in mathematics, minored in physics)
  - mrbrowning 10y ago
    Well, you're actually making metaphysical claims more than mathematical or physical ones. One of two assumptions, depending on how literally the sentiment that the universe is a formal system is intended, is being elided here: 1. That the universe _is_ a formal system, rather than being describable in the language of some formal system. It's not evident what the universe being a formal system even means, or how it squares with basic intuition regarding e.g. the fact that physical systems have state. 2. That, dropping the physical system <=> formal system equivalence and given some real system R consisting of some fundamental entities whose behaviors can be described in full in the language of some formal system S, (borrowing a useful construct from Lucas' anti-mechanism argument, even though I don't buy that argument) no machine can be constructed in R which computes theorems of some formal system S' in which all true statements of S are provable, meaning that no state of the system R can be said to contain a description of S', and that S' is therefore not describable by any arrangement of the entities in R (assuming some reasonable predicate over states of R that is true for a state when some arrangement of a subset of the entities in that state describes S'). Intuitively, this doesn't seem to hold up: by analogy, I can describe a universal Turing machine with a computer equipped with only finite memory. You could then attempt to go down the road of claiming that, even if a description of S' is possible in R, that a mind within R would not be capable of formulating that description, but then you're heaping on an even larger tangle of assumptions, unknowns, and things you have to define if you're going to argue the case rigorously. The point being that confidence about _any_ hypothesis about the nature of reality made on the basis of Gödel's incompleteness theorems is not epistemologically warranted.

cousin_it 10y ago

Here's a nice way to make peace with Godel's theorems. Let's say your beliefs about the integers can be summarized by some formal theory T. ("Every number has a successor", and so on, until your intuition runs out of things to say.) Now Godel jumps out of the bushes and says aha, your T doesn't include Con(T), so you aren't the math genius that you thought you were! But let's stop for a moment and consider what it would take for T to include Con(T). First of all, compared to other sentences about integers that you believe, Con(T) is an absolutely huge sentence. It must contain an arithmetization of all of T (encoding the axioms, inference rules, etc. into integer arithmetic). Second of all, if Con(T) is included in T while speaking about T, it might need to include an arithmetization of Con(T) itself! That uses a diagonal construction ("quine" in computer science terms), making the sentence even bigger. Now you're looking at some kind of hundred-kilobyte Diophantine equation, with no intuitive reason to believe it at all. And third of all, it's easy to see that an inconsistent theory T would easily prove Con(T) (because it proves any sentence), so having Con(T) inside T doesn't even give you any positive evidence for trusting T. In fact, we're lucky to live in a world where Godel's theorems are true, and having Con(T) inside T is negative evidence instead of none at all!

vilhelm_s 10y ago
I wonder if anyone has written out a Gödel sentence in full as a statement about numbers in English. It would be fun to see how big it gets. Also, the comment about size and diagonalization is interesting. The Gödel sentence from the first incompleteness theorem is made by diagonalizing, while the sentence from the second incompleteness theorem is just "Con(T)", so the sentence from the 2nd theorem is shorter and more natural if written out in full---making it even more disappointing that it's not provable. Indeed, if we put in more work we should be able to prove a more interesting theorem, but I never really thought about it before.
Certhas 10y ago
To some degree Chaitlin's equations [1] make the issue less abstract than that though. "We outline our construction of a single equation involving only addition, multiplication, and exponentiation of non-negative integer constants and variables with the following remarkable property. One of the variables is considered to be a parameter. Take the parameter to be 0, 1, 2, ... obtaining an infinite series of equations from the original one. Consider the question of whether each of the derived equations has finitely or infinitely many non-negative integer solutions. The original equation is constructed in such a manner that the answers to these questions about the derived equations are independent mathematical facts that cannot be compressed into any finite set of axioms." So there are finite (though several hundred pages long) equations for which the finiteness of the solution set is independent of every finite axiomatization of arithmetic. So suddenly, even though the formula is enormous, the type of sentence is perfectly normal. Does f(x) have finitely many solutions, where f(x) is built from addition, multiplication and exponentiation. Much more so than Gödel’s incompleteness this deeply violates my intuition about what type of statements should be decidable. [1] https://www.cs.auckland.ac.nz/~chaitin/berlin.pdf https://www.cs.auckland.ac.nz/~chaitin/berlin.pdf

psyc 10y ago

This isn't really about Gödel, but I always wish that people had a little bit less of a natural instinct towards bastardized Gödelian thinking. So that there would be fewer infuriating people arguing things like "Infringing on my right to infringe on the rights of others infringes on my rights." Or, "You can't be against criticism, because then you'd be criticizing criticism." I've been rolling my eyes at these arguments for decades, and I wish fewer people thought they were clever.

jchassoul 10y ago

Wittgenstein bitches!

cantagi 10y ago

I am halfway through reading Raymond Smullyan: A puzzle guide to Gödel, after finding out about his recent death here: https://news.ycombinator.com/item?id=13626221 https://news.ycombinator.com/item?id=13626221 . It explains Godel's incompleteness Theorems accurately to a layperson through a set of logical puzzles.