Beefy Boxes and Bandwidth Generously Provided by pair Networks
Pathologically Eclectic Rubbish Lister

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 the web crawler heard nothing...

How do I use this? | Other CB clients
Other Users?
Others imbibing at the Monastery: (4)
As of 2018-10-20 05:12 GMT
Find Nodes?
    Voting Booth?
    When I need money for a bigger acquisition, I usually ...

    Results (112 votes). Check out past polls.

    • (Sep 10, 2018 at 22:53 UTC) Welcome new users!