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.
> People have been practicing formal mathematics long before Godel
Right, this was pretty much my original point.
> This seems to indicate me that GP comment is right that the inciting incident was understanding the correspondence between mathematics and its encoding.
Doesn't this sentence contradict the previously quoted one? Or, at the very least, the point is far more subtle than the GP's "...it's the conceptual leap to thinking about mathematical statements as mathematical objects..."
I don't see anything in Hilbert's mathematics that indicates he did not "think about mathematical statements as mathematical objects". Very much the opposite, actually.
I'll agree that the key insight was basically about mathematics and its encoding. And that this insight was extremely non-obvious.
But Hilbert's program really was literally all about GP's "[thinking of] mathematical statements as mathematical objects".
Or, to restate this contentious agreement we're having another away: things like the idea to do numbering in the first place are the details, and do not obviously follow from treating mathematical objects as objects of mathematics itself.
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!
Two things: if you can find this text by Fefermann, this is very helpful: Are There Absolutely Unsolvable Problems? Gödel's Dichotomyhttps://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.
Thanks for the pointer to Feferman's (very interesting) article. As for Godel, my university's library turns out to have a set of the Collected Works. So, I'll just check that out. Thanks!
> 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.