Good post tilly. (++ btw). I hope I won't come across as too pedantic if I offer a small correction.
in reply to Re: Re: Re: (OT) Where is programming headed?
in thread (OT) Where is programming headed?
You stated the first incompleteness theorem as:
No consistent finite first order axiom system which includes arithmetic can prove its own consistency.
Now, that's actually a statement of the second incompleteness theorem. Also, the word "finite" is out of place, and severely weakens the claim. Even PA (Peano Arithmetic) can't be finitely axiomatised in first-order logic, because induction has to be defined using an infinite scheme. I expect you meant "recursive" instead of "finite". (In other words, there has to be a mechanical procedure which can decide whether or not any given sentence is an axiom, but the total number of axioms might be infinite.)
The first incompleteness theorem (as strengthened by Rosser) states:
In any consistent recursive first-order theory which includes arithmetic, there is a sentence which can be neither proved nor disproved in the theory. I.e. the theory is incomplete.
(Gödel's original version only applies to theories which have a somewhat artificial property which he called omega-consistency.)
If anyone is seriously interested in logic and the theory of computation, I would strongly recommend Boolos & Jeffrey which is remarkably well-written and complete. (Substantial notes are online here.) But be warned: even though the authors have done a fantastic job of making it as easy as possible to understand, it isn't light reading.
Update: (thanks sevensven) I should add that Douglas Hofstadter's Gödel, Escher, Bach is an inspiring, idiosyncratic book which (among other things) explains Gödel's proof of the first incompleteness theorem. At the very least it might inspire you to learn more about the subject. (It did for me!)