‘Journey to the Edge of Reason’ Review: Gödel’s Beautiful Mind | Hacker News Reader

‘Journey to the Edge of Reason’ Review: Gödel’s Beautiful Mind

wsj.com

46 pointsVigier22 comments

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?

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.

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

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?

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.

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 ....

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.

>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.

There was this thread a while back: https://news.ycombinator.com/item?id=25115746 (direct link: 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-theo...

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

Gödel Without (Too Many) Tears by Peter Smith

https://www.amazon.com/G%C3%B6del-Without-Too-Many-Tears/dp/...

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

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.

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.

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

It's not about "missing proofs". Instead its about

propositions not being provable.

See the following for contradictions in foundations:

https://papers.ssrn.com/abstract=3603021

Ziroshima:

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

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.

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

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

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.

Paywalled.

https://archive.is/eQezI

Reply on news.ycombinator.com