5 ms·

I still can not wrap my head around his incompletness theorem. I have read Hofstadter book about it, but still feel that I'm missing something. Does anyone kno

I still can not wrap my head around his incompletness theorem. I have read Hofstadter book about it, but still feel that I'm missing something. Does anyone knows or has a good write up about it?

papercrane 5y ago
I'd recommend "Gödel's Proof" by Ernest Nagel and James Roy Newman. The edition I read was revised by Hofstadter and I thought it did a good job of explaining the theorem.
slibhb 5y ago
There was this thread a while back: https://news.ycombinator.com/item?id=25115746 https://news.ycombinator.com/item?id=25115746 (direct link: https://stopa.io/post/269 https://stopa.io/post/269) As someone with limited math knowledge, I found it quite readable and understandable though I can't vouch for its accuracy. I would say, though, when talking about Godel, there is significant disagreement over what his work implies about the world or about the status of truth statements (if anything). You can see people arguing over that in the comments. edit - this one looks good too, maybe better as it avoids the controversial philosophical discussion: https://dvt.name/2018/03/12/godels-first-incompleteness-theorem-programmers https://dvt.name/2018/03/12/godels-first-incompleteness-theo...
pegasus 5y ago
Check out this HN discussion for some recommendations: https://news.ycombinator.com/item?id=24081858 https://news.ycombinator.com/item?id=24081858
jjcc 5y ago
I always try to to find some ELI5 but haven't found one yet. ELI5 won't be accurate but it's better than nothing. Here's my version. I know it's terrible but I wish it could trigger better versions from smarter HNers. Hopefully the ELI5 can evolve. ....Long time ago, in the Game Kingdom, people play games by rules called game law deduced by a basic meta law called Game Constitution. Most of time players play by game law. However not all judgment can be easily made following this principle. Some time 2 players would arguing like this: Group A: What you are doing is wrong so it is violating game law. Group B: Your blame is wrong. So your act of blaming violates game law. It ended up with conflicts. Too groups were firing rockets and air raiding with each other. To solve the contradictory, the Game Kingdom invited a group of alien higher order players to form a United Game Nation to make judgment about which claim is true or false. However as the high order players joined the new expanded Game Kingdom, there are conflicts again as before with the exact same reason. Now a new higher order United Game Nation needs to set up. But it will create new conflicts again and on and on ....
- ProfHewitt 5y ago
  Incompleteness in foundations is not exactly analogous to your game. The proposition MyTheoremsAreEnumerable is true but unprovable. Adding MyTheoremsAreEnumerable to a foundational theory makes the theory inconsistent.
  - jjcc 5y ago
    >is not exactly analogous Yes, I know as I already mentioned. That's why I wish somebody smarter than me can do it more accurately by putting the concepts such as "MytheoreumsAreEnumerable" into a better ELI5 way.
ziroshima 5y ago
I feel the same way. My take away was that every system of logic will have some sort of "This sentence is a lie." type of paradox. But it feels more like a technical quirk to me than anything of real significance. The fact that many people smarter than I am feel otherwise indicates to me that I'm missing something.
- rsj_hn 5y ago
  It is not about paradoxes like this, but missing proofs. Paradoxes are features of inconsistent systems, and we do not care about inconsistent systems. The types of paradoxes discovered in the early 20th century led people to refine set theory so that the paradoxes were removed and the systems were believed to be paradox free and thus useful for proving theorems. Once you've gotten rid of the paradoxes, you have a consistent system. This is the system of interest. Here, Godel is saying that consistent systems are incomplete. E.g. any consistent system will have some theorems that cannot be proved within that system. Note that I am not saying there are theorems for which we don't know the proof. E.g. the proof is too difficult or unknown, waiting for a more brilliant mind to discover it. I mean that the theorem cannot possibly have a proof of its truth or falsehood. The most famous example is the Continuum Hypothesis, which cannot be proved or disproved using standard set theory. The question of whether the continuum hypothesis is true is unanswerable. Thus the formal system is incomplete. https://en.wikipedia.org/wiki/Continuum_hypothesis https://en.wikipedia.org/wiki/Continuum_hypothesis The reductio ad absurdum, i.e. assume the system is complete and prove that it is inconsistent is not used to seriously consider inconsistent systems but rather to demonstrate that the systems we care about -- e.g. the consistent systems -- are incomplete.
  - ProfHewitt 5y ago
    It is only for 1st-order logic that it has been shown that the Continuum Hypothesis can neither be proved non disproved. The issue of the Continuum Hypothesis is still open for more powerful theories. See the following: https://papers.ssrn.com/abstract=3457802 https://papers.ssrn.com/abstract=3457802
  - ProfHewitt 5y ago
clairity 5y ago
i’ve never tried to walk through the proof myself (i’ve heard it makes some significant leaps, ironically), but understanding the gist of it seems reasonably straightforward. a simple summary (forget from where this came) is that no self-consistent set of statements is provable true (reflective of reality), and the converse, no provably true set of statements can be provably self-consistent (no unprovable premises allowed). the proof surely has lots of nuance and caveats, but the (apparently debatable) philosophical implication is that logical systems can’t stand on their own and explain the world, which actually seems succinctly consistent with our general lived experience.
- ProfHewitt 5y ago
  The proofs in [Gödel 1931] are incorrect for foundational theories because the proposition I'mUnprovable does not exist. It is very fortunate that I'mUnprovable does not exist because otherwise foundational theories would be inconsistent. See the following for an explanation: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
mcprwklzpq 5y ago
I can ELIP (Explain Like I am a Programmer) statements and consequences of both incompleteness theorems and two related problems. So the pemise is that you have to write 4 programs, but you can not, they all would fail for some inputs. 1. The first Gödel's incompleteness theorem. A program has to take a set of axioms and a set of true statements about natural numbers. It has to return proofs for all the statements. How it will fail? It would either for some statements return a proof that contradicts itself (so the set of axioms is inconsistent) or return no proof at all (so the set of axioms is incomplete). 2. The second Gödel's incompleteness theorem. A program has to take a set of axioms. I has to return true if program 1 given theese axioms would never retrun a proof that contradicts itself. How it will fail? It would return true for some set of axioms that are inconsistent. 3. Entscheidungsproblem. A program has to take a set of axioms and a statement. It has to return true if the statement is true. How it will fail? It would return true for some false statement. 4. Halting problem. A program has to take a program (in a Turing complete language). It has to return true if the program will ever finish. How will it fail? It would return true for program that would never finish. Or probably would itself never finish. This is also possible for all other programs.
- ProfHewitt 5y ago
  Your statement 1 of Gödel's first result is not quite correct. Suppose that Halt[e] means that expression e halts. The predicate Halt is algorithmically undecidable. That is, there is no algorithm that decides Halt. But this does not directly say that Halt is inferentially undecidable. That is, Halt[e] can always be proved or disproved.
- ProfHewitt 5y ago
  Your statement 2 of Gödel's second result is false because Gödel's second result is false for foundational theories. Foundational theories can in fact prove their own consistency. However, the self-proof of consistency is not very convincing because the proof is valid even if the theory is inconsistent. Fortunately, there is another way to prove consistency by showing that a theory has a mathematical model. See the following for an overview: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
bmitc 5y ago
Gödel Without (Too Many) Tears by Peter Smith https://www.amazon.com/G%C3%B6del-Without-Too-Many-Tears/dp/B08L5MQLRQ/ https://www.amazon.com/G%C3%B6del-Without-Too-Many-Tears/dp/...
ProfHewitt 5y ago
Inferential undecidablity is that not every proposition can be proved or disproved in the most powerful foundational theories. For example, the proposition Halt[e] means that evaluation of the expression e halts. It is not the case for every expression e that the following holds: *Halt*[e} is provable or not *Halt*[e] is provable. Inferential incompleteness is that there are true propositions in a foundational theories can cannot be proved. For example, the following proposition is true but unprovable: Theorems can be enumerated. See the following for more information: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
ProfHewitt 5y ago
You are correct to be confused. Godel's results depend on the existence of the proposition I'mUnprovable, which does not exist in foundations because the fixed point used in its construction violates orders on propositions. The most up-to-date article is here: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021

I still can not wrap my head around his incompletness theorem. I have read Hofstadter book about it, but still feel that I'm missing something. Does anyone knows or has a good write up about it?

papercrane 5y ago

I'd recommend "Gödel's Proof" by Ernest Nagel and James Roy Newman. The edition I read was revised by Hofstadter and I thought it did a good job of explaining the theorem.

slibhb 5y ago

There was this thread a while back: https://news.ycombinator.com/item?id=25115746 https://news.ycombinator.com/item?id=25115746 (direct link: https://stopa.io/post/269 https://stopa.io/post/269) As someone with limited math knowledge, I found it quite readable and understandable though I can't vouch for its accuracy. I would say, though, when talking about Godel, there is significant disagreement over what his work implies about the world or about the status of truth statements (if anything). You can see people arguing over that in the comments. edit - this one looks good too, maybe better as it avoids the controversial philosophical discussion: https://dvt.name/2018/03/12/godels-first-incompleteness-theorem-programmers https://dvt.name/2018/03/12/godels-first-incompleteness-theo...

pegasus 5y ago

Check out this HN discussion for some recommendations: https://news.ycombinator.com/item?id=24081858 https://news.ycombinator.com/item?id=24081858

jjcc 5y ago

I always try to to find some ELI5 but haven't found one yet. ELI5 won't be accurate but it's better than nothing. Here's my version. I know it's terrible but I wish it could trigger better versions from smarter HNers. Hopefully the ELI5 can evolve. ....Long time ago, in the Game Kingdom, people play games by rules called game law deduced by a basic meta law called Game Constitution. Most of time players play by game law. However not all judgment can be easily made following this principle. Some time 2 players would arguing like this: Group A: What you are doing is wrong so it is violating game law. Group B: Your blame is wrong. So your act of blaming violates game law. It ended up with conflicts. Too groups were firing rockets and air raiding with each other. To solve the contradictory, the Game Kingdom invited a group of alien higher order players to form a United Game Nation to make judgment about which claim is true or false. However as the high order players joined the new expanded Game Kingdom, there are conflicts again as before with the exact same reason. Now a new higher order United Game Nation needs to set up. But it will create new conflicts again and on and on ....

ProfHewitt 5y ago
Incompleteness in foundations is not exactly analogous to your game. The proposition MyTheoremsAreEnumerable is true but unprovable. Adding MyTheoremsAreEnumerable to a foundational theory makes the theory inconsistent.
- jjcc 5y ago
  >is not exactly analogous Yes, I know as I already mentioned. That's why I wish somebody smarter than me can do it more accurately by putting the concepts such as "MytheoreumsAreEnumerable" into a better ELI5 way.

ziroshima 5y ago

I feel the same way. My take away was that every system of logic will have some sort of "This sentence is a lie." type of paradox. But it feels more like a technical quirk to me than anything of real significance. The fact that many people smarter than I am feel otherwise indicates to me that I'm missing something.

rsj_hn 5y ago
It is not about paradoxes like this, but missing proofs. Paradoxes are features of inconsistent systems, and we do not care about inconsistent systems. The types of paradoxes discovered in the early 20th century led people to refine set theory so that the paradoxes were removed and the systems were believed to be paradox free and thus useful for proving theorems. Once you've gotten rid of the paradoxes, you have a consistent system. This is the system of interest. Here, Godel is saying that consistent systems are incomplete. E.g. any consistent system will have some theorems that cannot be proved within that system. Note that I am not saying there are theorems for which we don't know the proof. E.g. the proof is too difficult or unknown, waiting for a more brilliant mind to discover it. I mean that the theorem cannot possibly have a proof of its truth or falsehood. The most famous example is the Continuum Hypothesis, which cannot be proved or disproved using standard set theory. The question of whether the continuum hypothesis is true is unanswerable. Thus the formal system is incomplete. https://en.wikipedia.org/wiki/Continuum_hypothesis https://en.wikipedia.org/wiki/Continuum_hypothesis The reductio ad absurdum, i.e. assume the system is complete and prove that it is inconsistent is not used to seriously consider inconsistent systems but rather to demonstrate that the systems we care about -- e.g. the consistent systems -- are incomplete.
- ProfHewitt 5y ago
  It is only for 1st-order logic that it has been shown that the Continuum Hypothesis can neither be proved non disproved. The issue of the Continuum Hypothesis is still open for more powerful theories. See the following: https://papers.ssrn.com/abstract=3457802 https://papers.ssrn.com/abstract=3457802
- ProfHewitt 5y ago

clairity 5y ago

i’ve never tried to walk through the proof myself (i’ve heard it makes some significant leaps, ironically), but understanding the gist of it seems reasonably straightforward. a simple summary (forget from where this came) is that no self-consistent set of statements is provable true (reflective of reality), and the converse, no provably true set of statements can be provably self-consistent (no unprovable premises allowed). the proof surely has lots of nuance and caveats, but the (apparently debatable) philosophical implication is that logical systems can’t stand on their own and explain the world, which actually seems succinctly consistent with our general lived experience.

ProfHewitt 5y ago
The proofs in [Gödel 1931] are incorrect for foundational theories because the proposition I'mUnprovable does not exist. It is very fortunate that I'mUnprovable does not exist because otherwise foundational theories would be inconsistent. See the following for an explanation: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021

mcprwklzpq 5y ago

I can ELIP (Explain Like I am a Programmer) statements and consequences of both incompleteness theorems and two related problems. So the pemise is that you have to write 4 programs, but you can not, they all would fail for some inputs. 1. The first Gödel's incompleteness theorem. A program has to take a set of axioms and a set of true statements about natural numbers. It has to return proofs for all the statements. How it will fail? It would either for some statements return a proof that contradicts itself (so the set of axioms is inconsistent) or return no proof at all (so the set of axioms is incomplete). 2. The second Gödel's incompleteness theorem. A program has to take a set of axioms. I has to return true if program 1 given theese axioms would never retrun a proof that contradicts itself. How it will fail? It would return true for some set of axioms that are inconsistent. 3. Entscheidungsproblem. A program has to take a set of axioms and a statement. It has to return true if the statement is true. How it will fail? It would return true for some false statement. 4. Halting problem. A program has to take a program (in a Turing complete language). It has to return true if the program will ever finish. How will it fail? It would return true for program that would never finish. Or probably would itself never finish. This is also possible for all other programs.

ProfHewitt 5y ago
Your statement 1 of Gödel's first result is not quite correct. Suppose that Halt[e] means that expression e halts. The predicate Halt is algorithmically undecidable. That is, there is no algorithm that decides Halt. But this does not directly say that Halt is inferentially undecidable. That is, Halt[e] can always be proved or disproved.
ProfHewitt 5y ago
Your statement 2 of Gödel's second result is false because Gödel's second result is false for foundational theories. Foundational theories can in fact prove their own consistency. However, the self-proof of consistency is not very convincing because the proof is valid even if the theory is inconsistent. Fortunately, there is another way to prove consistency by showing that a theory has a mathematical model. See the following for an overview: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021

bmitc 5y ago

Gödel Without (Too Many) Tears by Peter Smith https://www.amazon.com/G%C3%B6del-Without-Too-Many-Tears/dp/B08L5MQLRQ/ https://www.amazon.com/G%C3%B6del-Without-Too-Many-Tears/dp/...

ProfHewitt 5y ago

Inferential undecidablity is that not every proposition can be proved or disproved in the most powerful foundational theories. For example, the proposition Halt[e] means that evaluation of the expression e halts. It is not the case for every expression e that the following holds: *Halt*[e} is provable or not *Halt*[e] is provable. Inferential incompleteness is that there are true propositions in a foundational theories can cannot be proved. For example, the following proposition is true but unprovable: Theorems can be enumerated. See the following for more information: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021

ProfHewitt 5y ago

You are correct to be confused. Godel's results depend on the existence of the proposition I'mUnprovable, which does not exist in foundations because the fixed point used in its construction violates orders on propositions. The most up-to-date article is here: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021