When I first heard of the existence of Gödel's theorem, I was amazed not just at the theorem but at the fact that the question could be made precise enough to answer: how on earth, even in principle, could one show that it was impossible to prove something in a given system? That doesn't bother me now, and that is not my question.
It seems to me that Gödel's theorem is a combination of at least three amazing achievements, namely these.
-
Formalizing the notions of proof, model, etc. so that the question could be considered rigorously.
-
Daring to think that there might be true but unprovable statements in Peano arithmetic.
-
Thinking of the idea of Gödel numbering and getting the proof to work.
One might think that 3 constitutes two separate achievements, but I think that actually getting the proof to work, though pretty good going, is somehow a technicality once you have had the idea that in principle a proof along those lines might be possible. (I'm not saying I could have done it, but Gödel would have been deeply immersed in these ideas.)
My guess is that pretty well all the credit for 2 and 3 goes to Gödel (except that the idea of diagonal proofs was not invented by him). My question is how much he contributed to 1 as well. Had it occurred to anyone else that it might be possible to think about such questions rigorously, or did an entirely new way of thinking appear pretty well out of nowhere? Popular accounts suggest the latter, but common sense would suggest the former, at least to some extent.
Best Answer
I posted this earlier on the "narrowly-missed discoveries" thread, but I think the two paragraphs below address your three questions. For the most recent scholarly account of Post's work, see the article "Emil Post" by Alasdair Urquhart, which may be found here. In a nutshell: Gödel was first to fully formalise the notion of proof in a particular system, but Post came damn close to a more general idea.
Emil L. Post was very close to proving Gödel's incompleteness theorem, and the existence of algorithmically unsolvable problems in the early 1920s. He realized that one could enumerate all algorithms, and hence obtain an unsolvable problem by diagonalization. Moreover, the "problem" can be viewed as a computable list of questions $Q_1,Q_2,Q_3,\ldots$ for which the sequence of answers (yes or no) is not computable. It follows that there cannot be any complete formal system that proves all true sentences of the form "The answer to $Q_i$ is yes" or "The answer to $Q_i$ is no," because this would solve the unsolvable problem.
But then Post was stuck because he needed to formalize the notion of computation. He had in fact (an equivalent of) the right definition, but logicians were not ready for a definition of computation, and did not believe there was such a thing until the Turing machine concept came along in 1936. Gödel avoided this problem when he proved his theorem (1930) by proving incompleteness of a particular system (Principia Mathematica).