What was Gödel's real achievement?

Question

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.

1. Formalizing the notions of proof, model, etc. so that the question could be considered rigorously.

2. Daring to think that there might be true but unprovable statements in Peano arithmetic.

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

Answer 1

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

Answer 2

Hilbert, in his 1922 "New Grounding of Mathematics" and subsequent papers, developed an approach to axiomatisation of proof that Goedel's result can be seen to have continued, whilst at the same time upsetting Hilbert's hopes. Hilbert and his coworkers had already understood the special status of proofs of consistency — finding a basis system that could prove its own consistency was a fundamental goal of Hilbert's Program — and had taken an ingenious view of the significance of mathematical statements that is somewhat misleadingly called formalist. I think both points one and two were already appreciated in the Hilbertian tradition.

I think it is easier to appreciate Goedel's insight when you take into account his 1929 completeness proof. This result gives a complete model, based on an essentially proof-theoretic algorithm, for Peano arithmetic (PA). The problem with it is that it makes counter-intuitive claims, and in particular concerning consistency statements: the model holds that PA is inconsistent.

Equipped with such powerful machinery, and the Hilbertian concern with consistency made asking the questions Goedel asked natural. What is astonishing is the energy and ingenuity that he brought to answering them.

Answer 3

Tarski came pretty close to proving the incompleteness actually. At that time He was around Gödel. Tarski proved the "twin theorem" of the incompleteness: the undefinability of a truth definition. In from Frege to Gödel of Van Heijenoort, Quine (if my memory serves me well) claims in one of the preface of an article of Skolem that he also came close to the incompleteness but was not aware it. Also as was mentioned by John Stillwell, Emil Post worked a lot in obtaining unsolvable problems.

P.S: Russell was mentioned in the thread. On the fom forum Alasdair Urquhart posted that he actually never really believed in Gödel's Theorem and thought they were paradoxical. It was also mentioned that his misunderstanding comes from him not making the difference between proof and truth. This is another big discovery of Gödel: the difference between proof and truth.

Answer 4

If I remember correctly, the notion of a model is already present in Hilbert-Bernays where finite structures are used for proving absolute consistency of some theories, and is probably older. Again, if I remember correctly, Frege, Russel, and Hilbert did have formal systems and the notion of a formal proof. Skolem's construction of a term model (which is now famous as Skolem's Paradox because the set of real numbers of the model turns out to be countable) is in his 1922 paper, where the Godel's completeness theorem is from 1929. In other words, it seems that Skolem did already have all the tools necessary for proving completeness in 1922. It seems that Hilbert had even stated the question of completeness for first-order theories before this date and Godel has learned about this problem in Carnap's logic course in 1928.

Hilbert's 10-th problem from his famous 23 problems asks for an algorithm to decide existence of solutions for Diophantine equations. I think there were attempts after this for understanding what is an algorithm. There were many definitions which came out before Turing's definition which were equivalent to his definition, although they were not philosophically satisfactory, at least Godel did not accept any of them as capturing the intuitive notion of computability before Turing's definition.

Godel's collected works can shed more light on these issues.

EDIT: Also

Solomon Feferman, "Gödel on finitism, constructivity and Hilbert’s program" http://math.stanford.edu/~feferman/papers/bernays.pdf

Hilbert and Ackermann posed the fundamental problem of the completeness of the first-order predicate calculus in their logic text of 1928; Gödel settled that question in the affirmative in his dissertation a year later. [page 2]

Hilbert introduced first order logic and raised the question of completeness much earlier, in his lectures of 1917-18. According to Awodey and Carus (2001), Gödel learned of this completeness problem in his logic course with Carnap in 1928 (the one logic course that he ever took!). [page 2, footnote]

Martin Davis, "What did Gödel believe and when did he believe it", BSL, 2005

Godel has emphasized the important role that his philosophical views had played in his discoveries. Thus, in a letter to Hao Wang of December 7, 1967, explaining why Skolem and others had not obtained the completeness theorem for predicate calculus, ... [page 1]