6 ms·

> thinking about mathematical statements as mathematical objects... Lock yourself away in a room with nothing but pen and paper (no internet, not books) and tr

> thinking about mathematical statements as mathematical objects... Lock yourself away in a room with nothing but pen and paper (no internet, not books) and try to reproduce Goedel's original proof. Then post the attempt here :) When I tried this a few years ago I made a mistake in the definition of numbering, got through half the proof, ran into trouble, and gave up before I figured out exactly where the mistake was. And I had already committed the overall outline and the tactical steps for each part to memory... Even if you remember the entire outline, it'll be really hard to get the details right.... And, more importantly, the outline itself is actually not obvious. >... much easier for us than for mathematicians of Godel's time because we are familiar with programs and computers Again, it seems unlikely that this was the sticking point. E.g. Hilbert understood mathematics as a symbolic game, thought about this exactly question, and didn't come up with Goedel's proof. And Hilbert was definitely no dullard.

gnulinux 8y ago
It's very hard to believe Godel didn't face problems you faced. He probably did mistakes too, and went back periodically to make sure his proofs are sane. He was probably stuck too, many times even, and solved those problems as other mathematicians solve their problems. After all, it took him many years to complete his proof. And even more years until theorems stabilized to today's form (i.e. Rosser's trick etc). People have been practicing formal mathematics long before Godel, and this cycle of being stuck and solving problems is pretty common in mathematics. His coworkers would have had the same sort of issue. This seems to indicate me that GP comment is right that the inciting incident was understanding the correspondence between mathematics and its encoding. Which brings us to: > E.g. Hilbert understood mathematics as a symbolic game Hilbert had a radically different understanding of the nature of mathematics compared to Godel. Moreover, Hilbert was radical enough that he tried to use his fame to silence people with differing views than him (e.g. Brouwer). Hilbert hardly believed Godel when he published his results, because it was easy to see that it would shake the foundations of "Hilbert's Program" something Hilbert spent half his life on (and logicians still publish papers about the relationship between Godel's Incompleteness theorems and Hilbert's Program). This makes Hilbert orders of magnitude less motivated to think about this issue, probably. On the other hand, Godel had various non-mathematical reasons to prove incompleteness, one being his desire to block materialism; check for Godel's Gibbs Lectures.
- kkylin 8y ago
  Has anyone tried to find a transcript of the Gibbs Lecture? Any luck? It apparently appears in Vol III of Godel's Collected Works, and nowhere else I can see. Thanks!
  - gnulinux 8y ago
    Two things: if you can find this text by Fefermann, this is very helpful: Are There Absolutely Unsolvable Problems? Gödel's Dichotomy https://academic.oup.com/philmat/article-abstract/14/2/134/1471456 https://academic.oup.com/philmat/article-abstract/14/2/134/1... it's super simple and clarifies a lot of things about Godel. Second, I took a philosophy of mathematics course when I was an undergrad studying computer science. And I have a copy of Godel (1951) (I think it's transcripted from his Gibbs Lecture) given to me as a class material. I tried search engines and couldn't find it anywhere, for the love of god. It's such a shame because it's a very important text imho. Since it's probably copyrighted or something, I don't know where to put it. If you're interested PM me and I can send you a pdf. Its title is "Some basic theorems on the foundation of mathematics and their implications". It's mostly about Godel explaining philosophical implications of his theorems and why he thinks they're important. If someone can find pdf, it'd be very helpful.
    - deleted 8y ago
      [deleted]
    - jacobparker 8y ago
      Could you send it to jacob at-sign solidangle.ca? I would greatly appreciate it. I couldn't find your contact information. It might be good to add it to your profile for other people.
      - deleted 8y ago
        [deleted]
      - gnulinux 8y ago
        Sorry, my bad, I never realized HN doesn't have PMs (or does it? Couldn't find an inbox). Sending the pdf to your email.
repsilat 8y ago
It's super easy to prove if you assume the Halting Problem is undecidable. Basically, 1. Assume every either T or ~T is provable for all theorems T, and that our logic is consistent. (The opposite of the incompleteness theorem.) 2. For every Turing machine, there is a proof that it halts or a proof that it doesn't halt. 3. A machine that enumerates and validates proofs will find one of those proofs, so the Halting Problem is decidable -- a contradiction. Easy peasy. (The proof of the Halting Problem undecidability from the Incompleteness Theorem is similarly straightforward.) Godel did his work first though, so he didn't have that machinery (hmm) available.
- pdonis 8y ago
  > It's super easy to prove if you assume the Halting Problem is undecidable. Well, sure, because proving the Halting Problem is undecidable is about as hard as proving Godel's Theorem without having the undecidability of the Halting Problem to start from.
  - chongli 8y ago
    It isn't, actually. The proof of the undecidability of the halting problem is rather straightforward. You just assume you have a program that determines whether or not its input halts or loops. Then you write a program that uses your assumption as a helper and does the opposite: If the input halts, then loop If the input loops, then halt You then pass the program itself as input to itself and you get a contradiction.
    - QuinnWilton 8y ago
      Here's my favourite version of this proof, in the style of a poem by Dr. Seuss: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html
    - deleted 8y ago
      [deleted]
  - jcranmer 8y ago
baddox 8y ago
Whether you have a thing memorized is fairly unrelated to how complex the thing is.
jonahx 8y ago
> Lock yourself away in a room with nothing but pen and paper (no internet, not books) and try to reproduce Goedel's original proof. Then post the attempt here :) We can all agree that would be hard, but your claim that the details are the central thing that makes GP hard is much, much stronger than that. The relevant question would be: How many people alive right now could succeed at your challenge? My guess would be thousands, maybe tens of thousands. And compare that to: The number of people alive who, without any knowledge of GP, could come up with the key insight you describe in your 1 paragraph summary of the proof, and the insight of using godel numbers to label mathematical statements to make that argument rigorous. The answer to that is "somewhere around 0." I get that you're impressed by the proof's details -- they're impressive -- but it seems like an odd take to rate those as more difficult than the incredible creative leaps that produced the high-level ideas behind the proof.
vyodaiken 8y ago
>Again, it seems unlikely that this was the sticking point. Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions. >E.g. Hilbert understood mathematics as a symbolic game, thought about this exactly question, and didn't come up with Goedel's proof. And Hilbert was definitely no dullard. Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic.
- thrmsforbfast 8y ago
  > Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions. Look at the game. Move after move of rooks moving in columns and rows and of bishops moving on the diagonals. :) > Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic. The point was that thinking of mathematics as a game in the first place requires "...the conceptual leap to thinking about mathematical statements as mathematical objects..." Goedel's proof didn't come out of nowhere, and he was NOT the one to first propose thinking of mathematical statements as mathematical objects. In many ways, Goedel's proof was actually a response to/rejection of "mathematical statements as mathematical objects" Goedel's big leap was... the proof itself. Was it the numberings? Well, I guess, but really it was what he did with the numberings. And then how he related that to arithmetic. It's hard to pick out a single piece of the derivation and say "ah ha! That's the key insight!". So I think "the point is in the details" is pretty accurate.
  - vyodaiken 8y ago
    You're missing my point.

gnulinux 8y ago

It's very hard to believe Godel didn't face problems you faced. He probably did mistakes too, and went back periodically to make sure his proofs are sane. He was probably stuck too, many times even, and solved those problems as other mathematicians solve their problems. After all, it took him many years to complete his proof. And even more years until theorems stabilized to today's form (i.e. Rosser's trick etc). People have been practicing formal mathematics long before Godel, and this cycle of being stuck and solving problems is pretty common in mathematics. His coworkers would have had the same sort of issue. This seems to indicate me that GP comment is right that the inciting incident was understanding the correspondence between mathematics and its encoding. Which brings us to: > E.g. Hilbert understood mathematics as a symbolic game Hilbert had a radically different understanding of the nature of mathematics compared to Godel. Moreover, Hilbert was radical enough that he tried to use his fame to silence people with differing views than him (e.g. Brouwer). Hilbert hardly believed Godel when he published his results, because it was easy to see that it would shake the foundations of "Hilbert's Program" something Hilbert spent half his life on (and logicians still publish papers about the relationship between Godel's Incompleteness theorems and Hilbert's Program). This makes Hilbert orders of magnitude less motivated to think about this issue, probably. On the other hand, Godel had various non-mathematical reasons to prove incompleteness, one being his desire to block materialism; check for Godel's Gibbs Lectures.

kkylin 8y ago
Has anyone tried to find a transcript of the Gibbs Lecture? Any luck? It apparently appears in Vol III of Godel's Collected Works, and nowhere else I can see. Thanks!
- gnulinux 8y ago
  Two things: if you can find this text by Fefermann, this is very helpful: Are There Absolutely Unsolvable Problems? Gödel's Dichotomy https://academic.oup.com/philmat/article-abstract/14/2/134/1471456 https://academic.oup.com/philmat/article-abstract/14/2/134/1... it's super simple and clarifies a lot of things about Godel. Second, I took a philosophy of mathematics course when I was an undergrad studying computer science. And I have a copy of Godel (1951) (I think it's transcripted from his Gibbs Lecture) given to me as a class material. I tried search engines and couldn't find it anywhere, for the love of god. It's such a shame because it's a very important text imho. Since it's probably copyrighted or something, I don't know where to put it. If you're interested PM me and I can send you a pdf. Its title is "Some basic theorems on the foundation of mathematics and their implications". It's mostly about Godel explaining philosophical implications of his theorems and why he thinks they're important. If someone can find pdf, it'd be very helpful.
  - deleted 8y ago
    [deleted]
  - jacobparker 8y ago
    Could you send it to jacob at-sign solidangle.ca? I would greatly appreciate it. I couldn't find your contact information. It might be good to add it to your profile for other people.
    - deleted 8y ago
      [deleted]
    - gnulinux 8y ago
      Sorry, my bad, I never realized HN doesn't have PMs (or does it? Couldn't find an inbox). Sending the pdf to your email.

repsilat 8y ago

It's super easy to prove if you assume the Halting Problem is undecidable. Basically, 1. Assume every either T or ~T is provable for all theorems T, and that our logic is consistent. (The opposite of the incompleteness theorem.) 2. For every Turing machine, there is a proof that it halts or a proof that it doesn't halt. 3. A machine that enumerates and validates proofs will find one of those proofs, so the Halting Problem is decidable -- a contradiction. Easy peasy. (The proof of the Halting Problem undecidability from the Incompleteness Theorem is similarly straightforward.) Godel did his work first though, so he didn't have that machinery (hmm) available.

pdonis 8y ago
> It's super easy to prove if you assume the Halting Problem is undecidable. Well, sure, because proving the Halting Problem is undecidable is about as hard as proving Godel's Theorem without having the undecidability of the Halting Problem to start from.
- chongli 8y ago
  It isn't, actually. The proof of the undecidability of the halting problem is rather straightforward. You just assume you have a program that determines whether or not its input halts or loops. Then you write a program that uses your assumption as a helper and does the opposite: If the input halts, then loop If the input loops, then halt You then pass the program itself as input to itself and you get a contradiction.
  - QuinnWilton 8y ago
    Here's my favourite version of this proof, in the style of a poem by Dr. Seuss: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html
  - deleted 8y ago
    [deleted]
- jcranmer 8y ago

baddox 8y ago

Whether you have a thing memorized is fairly unrelated to how complex the thing is.

jonahx 8y ago

> Lock yourself away in a room with nothing but pen and paper (no internet, not books) and try to reproduce Goedel's original proof. Then post the attempt here :) We can all agree that would be hard, but your claim that the details are the central thing that makes GP hard is much, much stronger than that. The relevant question would be: How many people alive right now could succeed at your challenge? My guess would be thousands, maybe tens of thousands. And compare that to: The number of people alive who, without any knowledge of GP, could come up with the key insight you describe in your 1 paragraph summary of the proof, and the insight of using godel numbers to label mathematical statements to make that argument rigorous. The answer to that is "somewhere around 0." I get that you're impressed by the proof's details -- they're impressive -- but it seems like an odd take to rate those as more difficult than the incredible creative leaps that produced the high-level ideas behind the proof.

vyodaiken 8y ago

>Again, it seems unlikely that this was the sticking point. Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions. >E.g. Hilbert understood mathematics as a symbolic game, thought about this exactly question, and didn't come up with Goedel's proof. And Hilbert was definitely no dullard. Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic.

thrmsforbfast 8y ago
> Look at the proof - page after page of work showing how to encode and decode formal propositions using primitive recursive functions. Look at the game. Move after move of rooks moving in columns and rows and of bishops moving on the diagonals. :) > Goedel's theorem is exactly that mathematics is not a symbolic game - that Hilbert's program is not possible. The proof relies on reducing logical deduction to arithmetic. The point was that thinking of mathematics as a game in the first place requires "...the conceptual leap to thinking about mathematical statements as mathematical objects..." Goedel's proof didn't come out of nowhere, and he was NOT the one to first propose thinking of mathematical statements as mathematical objects. In many ways, Goedel's proof was actually a response to/rejection of "mathematical statements as mathematical objects" Goedel's big leap was... the proof itself. Was it the numberings? Well, I guess, but really it was what he did with the numberings. And then how he related that to arithmetic. It's hard to pick out a single piece of the derivation and say "ah ha! That's the key insight!". So I think "the point is in the details" is pretty accurate.
- vyodaiken 8y ago
  You're missing my point.