Gödel Without (Too Many) Tears
logicmatters.net
logicmatters.net
The author, Peter Smith. has a wonderful blog on topics in Logic at [0]. He is planning on releasing a series of posts that will become GWT2, but his most recent post [1] explain why this has been delayed. He is also the author of a textbook on Introduction to Gödel’s Theorems [2], of which GWT is a compression. A second edition of Introduction to Gödel’s Theorems was recently released. He also has a fantastic resource, Teach Yourself Logic Guide [3], which is a collection of pointers of resources to teach yourself properly mathematical logic. He has plenty of other helpful resources that I won't directly point out, except to look under the heading Explore all this site on the front of his blog, along with the individual posts of course.
[0] http://www.logicmatters.net/blogfront/
[1] http://www.logicmatters.net/2013/09/gwt-and-tyl-on-hold/
[2] http://www.logicmatters.net/igt/
[3] http://www.logicmatters.net/2013/08/tyl-17-the-teach-yoursel...
Currently it's Kantor->Gödel(+ some historical background on Hilbert program/Principia etc.)->Turing(halting problem as it relates to the incompleteness theorems)->Cohen on the math front (+Chaitin numbers and some other random ideas)
He is a fine writer. Would love to take his TYL class
Now I know most HNers are no stranger to this book, but if you haven't read it I encourage you to pick up a copy. A lot of people will say that it "changed the way they think about everything" without going into much more detail, so I'll just tell you how it did so for me. I've always been an analytical thinker, but the most useful thing this book did for me was teach me how to think mathematically. It showed me there was immense beauty in mathematical thought.
Some of his books, the aforementioned in particular, are works of insight and genius. Others, such as his recent book on metaphor-as-thought, are speculative steps onto a bit thinner ice.
(Note: I realize Hofstadter and his colleagues have spent decades exploring metaphor-based AI, and that there might be something quite real to it -- but he doesn't make a convincing case for the sufficiency of this hypothesis, though he insists it's there).
Yeah, I know it's not an ideal format for Kindle, e.g. the illustrations and... a few other features I won't give away here. But still. What a great thing to have at-hand anytime you wanted to dive in and read part of it. Sigh.
[1] http://www.amazon.com/Gödels-Proof-Ernest-Nagel/dp/081475837...
Then again, most books I've read I forget about much sooner than a few months. If you want a good read, go for it, but its not some holy grail that will change your life forever.
Keith Devlin's popular mathematics works also have much the same appeal.
That it was heavy in your bag isn't really saying much about the book. Are you familiar with Russell's Paradox? If reading about Russell's Paradox for the first time demands that you work it around in your head for the next hour as though some outside force is compelling you to understand its implications, then the book is probably for you. If that sounds miserable, then it probably isn't.
And I read it as a kid. I've picked it up recently, I have a degree in advanced math. I kind of like Hofstadter's take on AI. But I think GEB is just terrible. I mean, it has long, clever discussions that half-explain thing so I think it makes people feel like they sort of understand things. But have to say I think it gives the opposite of a solid math approach by never being fully clear, concise or complete.
I assume GEB may be both informing and interest piquing for some people. For us, it just didn't ever get clear about what it was about and was mostly frustrating for that reason. Maybe none of us were "normal".
(happy to be corrected on this)
1) Consistency of PA
2) http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theore...
[1]: https://en.wikipedia.org/wiki/List_of_statements_undecidable...
Then, defending the value of the Halting Problem as a real problem is easy, relatively generally through Rice's Theorem: http://en.wikipedia.org/wiki/Rice%27s_theorem
In colloquial terms, one can render Rice's Theorem as "Would you like to produce a program that can prove anything remotely interesting across the set of all possible inputs? TOO BAD!" That's glib, but less inaccurate than we'd like.
Godel's theorem is, as Scott said, really sort of ad hoc and hard to easily apply in your head the way you're asking about. The Halting Problem, on the other hand, turns up everywhere, in real life (though many people still often don't realize it).
However, my [unverified] gut feeling is that we can prove halting/nonhalting (via static analysis and restricting types of code that are allowed) for the large class of things that we actually use (or should use) in practice and vice versa - we should push the convoluted cases (where analysis isn't possible) away from practical usage, since if a well-designed computer system can't reason about them, then likely the programmer can't as well and that part is buggy in some corner case.
I.e., if your webservice isn't provably halting, guaranteeing a return value within a (short) bounded time - then it's too complex and is 99.9% likely to have a security flaw that allows denial of service or execution of arbitrary code in which case, naturally, you can't reason about it as the halting theorem proves.
We don't even need to know a "proper" answer to the halting question - guaranteed to finish under X steps/whatever: okay; not guaranteed (maybe halting in X+1 steps): suspect/bad. That would be good enough for practical purposes in most systems.
you can also soundly construct an analysis that asks "is this program safe" and answers with one of {yes, no, maybe I don't know}. and then, you interpret a result of "no" and "maybe I don't know" to mean the same thing and re-write the program until you get a "yes"...
If the former, you should know you are not alone and serious attempts to create such programming languages are afoot. It's hard for me to find any solid, single web page to point you at, but you want to look at the more theoretical end of Haskell, and Agda and Coq, for some examples. Interesting Google terms include "structural recursion" and various other recursion schemes, and also things like http://blog.sigfpe.com/2007/07/data-and-codata.html .
The thing is Goedel shaped the development of logic itself tremendously. Before Goedel, the idea was that proven theorems were essentially the true theorems. The concept of theory proving as a simply mechanical process wasn't there, the idea of models and true-but-not-provable theories wasn't there etc. Contrawise, once you have this machinery, the theorem is fairly simple (if sometimes tedious) to produce.
So sketching Goedel's theorem can't help but be sketching early twentieth century logic.
Scott Aaronson had a throwaway 2 line 'proof' (not technically) of the theorem that intuitively clicked for me:
>First, though, let's see how the Incompleteness Theorem is proved. People always say, "the proof of the Incompleteness Theorem was a technical tour de force, it took 30 pages, it requires an elaborate construction involving prime numbers," etc. Unbelievably, 80 years after Gödel, that's still how the proof is presented in math classes!
>Alright, should I let you in on a secret? The proof of the Incompleteness Theorem is about two lines. The caveat is that, to give the two-line proof, you first need the concept of a computer.
>When I was in junior high, I had a friend who was really good at math, but maybe not so good at programming. He wanted to write a program using arrays, but he didn't know what an array was. So what did he do? He associated each element of the array with a unique prime number, then he multiplied them all together; then, whenever he wanted to read something out of the array, he factored the product. (If he was programming a quantum computer, maybe that wouldn't be quite so bad!) Anyway, what my friend did, that's basically what Gödel did. He made up an elaborate hack in order to program without programming.
The rest here: http://www.scottaaronson.com/democritus/lec3.html