Beefy Boxes and Bandwidth Generously Provided by pair Networks
Do you know where your variables are?

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

Log In?

What's my password?
Create A New User
Node Status?
node history
Node Type: note [id://132351]
and all is quiet...

How do I use this? | Other CB clients
Other Users?
Others taking refuge in the Monastery: (5)
As of 2017-10-22 03:12 GMT
Find Nodes?
    Voting Booth?
    My fridge is mostly full of:

    Results (272 votes). Check out past polls.