Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

How Gödel's Proof Works (2020)

quantamagazine.org

Post reply on HN
Print view View original

51–60 of 74 posts

Re: How Gödel's Proof Works (2020)

#51

Post by bell-cot »

gradschool wrote: post #50

I'm aware that very smart people have thought carefully about all this, but I still can't help thinking that this argument is unnecessarily complicated. It seems to me that a proof is something that can be written down as a finite string of symbols, so any proof system admits only countably many proofs. On the other hand, it's easy to make up an example of an uncountable set of propositions. That's too many for each…

Does your uncountable set of propositions include some which cannot be written as a finite string of symbols?

If "yes" - how might such as proposition be proven true with a finite string of symbols?

(If your proof symbols are from an infinite character set, that has its own issues.)

Re: How Gödel's Proof Works (2020)

#52

Post by GoblinSlayer »

pfdietz wrote: post #26

You can also obtain incompleteness from the unsolvability of the halting problem, by noting that if every statement in (say) Peano arithmetic were provable, one could solve the halting problem. Encode a halting execution of a TM as an integer using Gödel numbers and write a statement that the execution halts. Either that statement or its negation would be provable, so search for proofs for each at the same time. An a…

That won't work. Gödel number encodes a paradox, but a halting execution of a TM is not a paradox, so can't be written as a Gödel number.

Re: How Gödel's Proof Works (2020)

#53

Post by gradschool »

bell-cot wrote: post #51
gradschool wrote: post #50

I'm aware that very smart people have thought carefully about all this, but I still can't help thinking that this argument is unnecessarily complicated. It seems to me that a proof is something that can be written down as a finite string of symbols, so any proof system admits only countably many proofs. On the other hand, it's easy to make up an example of an uncountable set of propositions. That's too many for each…

Does your uncountable set of propositions include some which cannot be written as a finite string of symbols? If "yes" - how might such as proposition be proven true with a finite string of symbols? (If your proof symbols are from an infinite character set, that has its own issues.)

I'm assuming a finite alphabet and a finitely axiomatizable proof system per convention. I can't think of an uncountable set of propositions in which each can be written as a finite string of symbols, so that's what I was missing. Thank you for clearing this up for me.

Re: How Gödel's Proof Works (2020)

#54

Post by Xmd5a »

> Mathematician Gregory Chaitin deeply admires Kurt Gödel’s work, viewing the incompleteness theorems as monumental. However, rather than relying on the liar’s paradox like Gödel, Chaitin reframed incompleteness through information theory and computer size (using the Berry paradox). He argues that Gödel’s proof makes incompleteness look like a rare, pathological exception, whereas his own information-theoretic approach shows it is natural, universal, and everywhere in math.

Google AI. Trust me bros, he said something along those lines. Understanding Godel's proof is terribly challenging even for teenage Chaitin.

Found this lovely anecdote

>Robert J. Marks: So you cold called him then. [...]

>Gregory Chaitin: So he said, “Okay, send me a paper of yours on this topic. I’ll take a look at it. And if like it, maybe I’ll give you an appointment to visit.” [...] So he had taken a look at it and immediately perceived a crucial aspect of the definition of complexity that I was proposing. And he gave me an appointment. [...]

>Gregory Chaitin: I was all set for the great day — and it snowed! And this was the week before Easter. So that’s unusual, a spring snowstorm but it wasn’t a big snowstorm. Nothing was going to stop me from visiting my hero. So there I am in my office at the IBM Watson Center, about to leave. I figured out how much time I needed. About to leave and unfortunately — very unfortunately — the phone rang. It was Gödel ’s secretary saying Gödel is very careful with his health. And because it snowed, he’s not coming in to his office today. And therefore your appointment is canceled.

>So that was a surreal experience. And there was no way to reschedule because I was going to leave just in a few days, heading back to Argentina, to Buenos Aires. But actually this surreal story actually fits better Gödel and his legend, because for example, when Gödel died, they found lots of answers typed up to letters he received, but were never sent. They were never mailed. So there was a surreal quality to Gödel and to communicating with Gödel.

https://mindmatters.ai/2021/03/gregory-chaitins-almost-meeti...

Re: How Gödel's Proof Works (2020)

#55

Post by Xmd5a »

gradschool wrote: post #53
bell-cot wrote: post #51

Earlier quoted context omitted.

Does your uncountable set of propositions include some which cannot be written as a finite string of symbols? If "yes" - how might such as proposition be proven true with a finite string of symbols? (If your proof symbols are from an infinite character set, that has its own issues.)

I'm assuming a finite alphabet and a finitely axiomatizable proof system per convention. I can't think of an uncountable set of propositions in which each can be written as a finite string of symbols, so that's what I was missing. Thank you for clearing this up for me.

If you substitute uncountability in your intuition with algorithmic incompressibility (too much information to be captured by shorter descriptions) you have Chaitin's incompleteness theorem.

Kudos for the well-placed hunch!

Re: How Gödel's Proof Works (2020)

#56

Post by rramadass »

gregfjohnson wrote: post #31

Show HN: I recently gave a talk on the incompleteness theorem, specifically expressed in the language of software. It starts with a bit of historical background and a discussion of some of the philosophical context in which he carried out his work. The second half of the talk is my attempt to show the beautiful essential idea at the core of Godel's idea, pitched to a technically knowledgeable general audience. These…

Very Nice; Thank You!

Is there a way to get a pdf of the slides?

Re: How Gödel's Proof Works (2020)

#57

Post by rramadass »

fhe wrote: post #45
gregfjohnson wrote: post #31

Show HN: I recently gave a talk on the incompleteness theorem, specifically expressed in the language of software. It starts with a bit of historical background and a discussion of some of the philosophical context in which he carried out his work. The second half of the talk is my attempt to show the beautiful essential idea at the core of Godel's idea, pitched to a technically knowledgeable general audience. These…

I hope you don't mind, but just in case anyone is curious like I am, here i think is the video to the talk https://www.youtube.com/watch?v=KdZq5JvhPVQ

Thank You.

This is key to understanding the slide deck shared by the author.

Re: How Gödel's Proof Works (2020)

#59

Post by scotty79 »

For me this proof was always a cautionary tale about being careful about recursion when you use any language.

It's the same thing as with set theory. Once you let yourself talk about sets of sets without any restrictions other than the language itself puts on what you are talking about, you'll end up with sort of contradictory recursion that ends up in a paradox. The message is not "set theory is incomplete, or invalid" but rather "we were a bit too cavalier with words and not everything we can say about sets makes sense just because it's grammatically correct so we need to be more careful about defining what a set is and what it can and cannot contain".

For me "provability" is a direct equivalent of unrestricted sets of sets. If you don't restrict what provability means and how it can be used in context of the rest of math you end up with contradictory recursion that makes you believe there are true but unprovable things. It's easier to spot how bonkers it is on sets because there you end up with a set that is and isn't its own element at the same time (because sets are so generic that can produce paradoxical recursion on themselves without any other concept involved), but things being unprovable and true at the same time is the same category of absurdity.

Post reply on HN