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.
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.
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
....
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.
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.
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.
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.
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.
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.
Thank you. I downloaded this paper a month ago to read it eventually. Your comment made me read it yesterday and i have a question.
By using the type system would we exlude potentially consistent theories? Is it similar to how limitimg ourselves to a decidable language instead of a turing complete one would prevent us from writing potentially never halting programms that could still halt?
23 comments
[ 4.8 ms ] story [ 86.9 ms ] threadDoes anyone knows or has a good write up about it?
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-theo...
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 ....
The proposition MyTheoremsAreEnumerable is true but unprovable.
Adding MyTheoremsAreEnumerable to a foundational theory
makes the theory inconsistent.
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.
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
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.
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
propositions not being provable.
See the following for contradictions in foundations:
https://papers.ssrn.com/abstract=3603021
Your intuition is correct in that Gödel's proposition
I'mUnprovable does indeed lead to an inconsistency in foundations.
However, there are foundational theories that can be proved
to be free of contradiction. For example, see the following:
https://papers.ssrn.com/abstract=3418003
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
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.
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.
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
By using the type system would we exlude potentially consistent theories? Is it similar to how limitimg ourselves to a decidable language instead of a turing complete one would prevent us from writing potentially never halting programms that could still halt?
https://www.amazon.com/G%C3%B6del-Without-Too-Many-Tears/dp/...
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:
Inferential incompleteness is that there are true propositionsin a foundational theories can cannot be proved. For example,
the following proposition is true but unprovable:
See the following for more information:https://papers.ssrn.com/abstract=3603021
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://archive.is/eQezI