What was Gödel's real achievement?

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.

-
I would say that the very title of Gödel's article (to become his Habilitationsschrift) 'Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I' shows his awareness of the existing preoccupations with formalization of the notion of proof at the time. Apart from Russell and Whitehead, the names of Carnap, Brouwer, Hilbert-Ackermann,von Neumann come to mind.So I think that common sense indeed prevails over popular accounts on this question. – Georges Elencwajg Apr 3 '10 at 10:14
I think it is a bit unfair to refer to Gödel's incompleteness theorems simply as "Gödel's theorem". To me it trivializes Gödel other fundamental contributions to logic (such as his completeness theorem or the development of the constructible hierarchy). – Richard Dore Jul 14 '10 at 15:31
Please check: Kurt Gödel and the foundations of mathematics, Cambridge Univ. Press, Cambridge, 2011, and especially the article Macintyre, Angus: The impact of Gödel's incompleteness theorems on mathematics (pp. 3–25). – Margaret Friedland Jan 30 '13 at 16:15

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

-
My understanding is that logicians knew they needed a definition of computation, but didn't have a satisfactory one until Turing -- Goedel used guarded recursive equations, Church used lambda-calculus, etc. But the philosophical analysis that this indeed properly captured the idea of algorithm was what was lacking until Turing, and why they saw it as such a triumph. – Neel Krishnaswami Apr 3 '10 at 12:13
I'm not sure that logicians, other than Post, knew they needed a definition of computation until around 1935, when Church proposed lambda-calculus. Gödel at first thought that diagonalization would make a definition impossible, and it was Turing's definition that brought him round. Incidentally, Post came up with essentially the same definition as Turing at almost the same time. But he published only a very terse 3-page paper on it, and it was certainly Turing's analysis of human vs. machine computation that convinced people. – John Stillwell Apr 3 '10 at 21:01
This is very interesting, thanks! I was under the impression that defining computation was part of the debate about what "finitary methods" were. But if I understand you, this view is a modern reconstruction/reinterpretation of their concerns in light of our current understanding of computability. – Neel Krishnaswami Apr 4 '10 at 11:15

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.

-
I don't understand what you mean by "the model holds that PA is inconsistent." This sounds uncomfortably close to the common error that Gödel proved that PA is inconsistent. Could you clarify? – John Stillwell Apr 3 '10 at 21:10
Charles, after thinking a little longer, I've come up with a valid way to interpret "the model holds that PA is inconsistent." Gödel's second incompleteness theorem, discovered independently by him and von Neumann, states that Con(PA) is a particular sentence that PA neither proves nor disproves. Here Con(PA) is sentence expressing the consistency of PA. It follows that PA + not Con(PA) is a consistent set of sentences, and hence this set of sentences has a model, by the proof of Gödel's completeness theorem. Thus the model in a sense "holds that" PA is inconsistent. Is this what you meant? – John Stillwell Apr 4 '10 at 0:35

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.

-
Urquhart made his comment more precise later; the relevant posts are - cs.nyu.edu/pipermail/fom/2010-March/014508.html - cs.nyu.edu/pipermail/fom/2010-April/014514.html – François G. Dorais Apr 5 '10 at 0:37
In Feferman's book about Tarski life there is note that Tarski was very close to Goedel ideas. They contact each other, and also Tarski proved ( but published it after 2nd war) that Euclidean Geometry (and the theory of real closed fields as well - which is used here) is complete. Some remarks about relation to Goedel work may be found in Tarski article on that topics. – kakaz Jun 10 '10 at 11:19

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]

-