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?
Does anyone knows or has a good write up about it?
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:
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?
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.
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...
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.
in a foundational theories can cannot be proved. For example,
the following proposition is true but unprovable:
Theorems can be enumerated.
https://www.amazon.com/G%C3%B6del-Without-Too-Many-Tears/dp/...
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:
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:
propositions not being provable.
See the following for contradictions in foundations:
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:
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: