The stupid question is the question not asked  
PerlMonks 
Gödel's incompleteness theoremsby robin (Chaplain) 
on Dec 16, 2001 at 19:34 UTC ( #132351=note: print w/replies, xml )  Need Help?? 
Good post tilly. (++ btw). I hope I won't come across as too pedantic if I offer a small correction.
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 firstorder 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 firstorder 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 omegaconsistency.) If anyone is seriously interested in logic and the theory of computation, I would strongly recommend Boolos & Jeffrey which is remarkably wellwritten 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!)
In Section
Meditations

