The stupid question is the question not asked PerlMonks

### Gödel's incompleteness theorems

by robin (Chaplain)
 on Dec 16, 2001 at 19:34 UTC ( #132351=note: print w/replies, xml ) Need Help??

in reply to Re: Re: Re: (OT) Where is programming headed?
in thread (OT) Where is programming headed?

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

Create A New User
Node Status?
node history
Node Type: note [id://132351]
help
Chatterbox?
 [erix]: a few years ago there was suddenly the news that the Kremlin was using typewriters again. Heard nothing about it afterward [erix]: (maybe that means it worked) [oiskuu]: Yeah, it might work as long as there are no root exploits. ;-) [Corion]: Also, it's much harder to leak paper sheets than it is to leak documents that are available electronically [oiskuu]: tye, do you make use of remote logging? [oiskuu]: erix, this gives a new definition to e-paper: something that records the pressure imprints and is bluetooh capable, looks like ordinary paper. [oiskuu]: So to be really, really sure, you must microwave the paper before you type on it.

How do I use this? | Other CB clients
Other Users?
Others studying the Monastery: (6)
As of 2017-06-23 20:26 GMT
Sections?
Information?
Find Nodes?
Leftovers?
Voting Booth?
How many monitors do you use while coding?

Results (555 votes). Check out past polls.