Even without trying to follow the proof proper, the sub-sections of the second part are interesting on their own, particularly Gödel numbering and primitive recursive functions. Here is another translation that covers just this part:
It's true that if you know nothing about formal logic, history of metamathematics, and decidability, then it's going to be particularly hard going, but there are a lot of accessible resources for each of those topics and the paper is well structured (meaning you can concentrate on the pieces).
The encoding that Gödel used for formulas should be fascinating for anyone familiar with Turing work on decidability as well as how computers work generally. Primitive recursive functions don't handle computation generally, but seem to be a first step in understanding what it means. Anyone familiar with Alonzo Church, lambda calculus, functional programming, McCarthy's first paper on Lisp would probably be interested in this bit.
Of course, Gödel's result on formal systems shattered the idea of an axiomatic basis for mathematics, but I personally think its greater long-term impact is helping to usher in computation. It's worth recognizing both.
http://www.w-k-essler.de/pdfs/goedel.pdf
Here's an English translation (with a lengthy introduction)
http://jacqkrol.x10.mx/assets/articles/godel-1931.pdf
Even without trying to follow the proof proper, the sub-sections of the second part are interesting on their own, particularly Gödel numbering and primitive recursive functions. Here is another translation that covers just this part:
http://www.research.ibm.com/people/h/hirzel/papers/canon00-g...
It's true that if you know nothing about formal logic, history of metamathematics, and decidability, then it's going to be particularly hard going, but there are a lot of accessible resources for each of those topics and the paper is well structured (meaning you can concentrate on the pieces).
The encoding that Gödel used for formulas should be fascinating for anyone familiar with Turing work on decidability as well as how computers work generally. Primitive recursive functions don't handle computation generally, but seem to be a first step in understanding what it means. Anyone familiar with Alonzo Church, lambda calculus, functional programming, McCarthy's first paper on Lisp would probably be interested in this bit.
Of course, Gödel's result on formal systems shattered the idea of an axiomatic basis for mathematics, but I personally think its greater long-term impact is helping to usher in computation. It's worth recognizing both.