Gödel Without (Too Many) Tears(logicmatters.net)
logicmatters.net
Gödel Without (Too Many) Tears
http://www.logicmatters.net/igt/further-notes/godel-without-tears/
30 comments
This is a great blog. I was looking for a github link - this stuff would be good as book/classes on there.
He is a fine writer. Would love to take his TYL class
He is a fine writer. Would love to take his TYL class
Thanks. This looks like some interesting reading material. I have included an untitled chapter that is a mixed bag of philosophical issues etc. in my AI lecture (as a follow up to the chapters on propositional calculus and first order logic) and am always on the lookout for simpler ways to explain things.
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)
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)
Mandatory recommendation for Gödel, Escher, Bach: An Eternal Golden Braid [1] by Douglas Hofstadter.
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.
[1] http://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach
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.
[1] http://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach
It's a good read, but you have to be careful with it, because it can take up a lot of your time and you'll quickly run into diminishing returns. Hofstadter is smarter than I am, and I know he's smarter than I am, so I'm never sure whether I've understood anything properly. It's a perfectly laid Dunning-Kruger trap, and it ensnares probably too much of my processor time when I fall into it.
The problem with reading Hofstadter is that, because he's so brilliant and so lucid, you'll often find yourself readily him uncritically: thoroughly convinced by anything he's saying, and simply absorbing it all.
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).
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).
It annoying having GEB discussion be the top thread in a discussion about a rigorous or accessible exposition of Goedels' theorem. If those who don't find GEB tedious, overblown and overlong would to agree it's just not about Goedel's theorem. I mean really not. It's about self-reference and stuff. But it absolutely not any kind of exposition of Goedel's theorem at all, just stop.
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.
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.
if you have a degree in advanced maths, i would postulate the book isn't written for people like you. Its a laymen's book, written for the general public with no indepth knowledge of maths - and yet it manages to both inform, and pique the interest of readers. Sure, it isn't vigorous like one would have to be for a published scientific paper, but a normal person don't read that sort of thing anyway.
I first encountered GEB when my mother read it to me and my sister when we were my sister was nine and I was fourteen.
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".
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".
For anyone looking for a brief, accessible explanation of the proof itself, I cannot recommend the Nagel and Newman [1] highly enough.
[1] http://www.amazon.com/Gödels-Proof-Ernest-Nagel/dp/081475837...
[1] http://www.amazon.com/Gödels-Proof-Ernest-Nagel/dp/081475837...
While I loved the first few chapters of the book, and they were mind-opening, I found the explanation of the proof unsatisfactory. As I recall, it was mentioned in the preface that the book will give a complete outline of the actual proof. I did not find this to be the case, the outline seemed to jump quite a bit from one thought to another leaving me with more questions about the proofs than answers. I still do not understand the proofs (though I now nearly understand an analogous result in computer science via Jeff Ulmann's book).
I has been a few decades since I read it for the first time, so I may be glossing it in my mind.
Is it really that great? I started reading it when in college, got tired of lugging a huge dead-tree book around in my bag, and eventually just sort of put it down. Maybe I didn't get far enough in to hit the parts that would be interesting to someone who's already long-since done basic programming and math?
It's probably not that earth-shattering if you already have an appreciation for the beauty of mathematical patterns and thought, but if you're a 19 year old college kid like I was who thought he hated math, it will definitely cause you to rethink your position.
Keith Devlin's popular mathematics works also have much the same appeal.
Keith Devlin's popular mathematics works also have much the same appeal.
It definitely blew my mind when I first read it, but I think its also gained a big cult following creating a lot of hype. I thought about it a lot for a few months after I read it, but I certainly haven't thought about it in over a year and it definitely hasn't shaped the way I think about things now (at least not that I'm aware of). If you haven't taken the math behind it, its awesome and you should definitely read the first 14 chapters if you're interested. But after that, its basically a bunch of Hofstatdler's musings on DNA and AI, a lot of which seems outdated and like a lot of speculation (the book was published ~25 years ago).
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.
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.
I started reading it when in college, got tired of lugging a huge dead-tree book around in my bag, and eventually just sort of put it down.
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.
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.
GEB high on my list of books that I own on dead trees, but also want on Kindle. Even if it didn't qualify for Amazon's deal to get it cheaper if you already bought it from them -- even if I had to pay a lot for it.
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.
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.
Even if it doesn't have a profound effect on your perspective or if you find the conclusions uninteresting, the journey itself is very informative. Read if you don't already have much exposure to: first order logic / predicate calculus; formal systems; DNA; Escher and Bach; number theory; Goedel's incompleteness theorem; Turing machines; neuroscience; information theory...
What I don't get about Goedel's Incompleteness Theorem is why it's considered a problem in the general sense. It shows that in any formal system (of sufficient power etc. etc.) you can produce a Goedel number which cannot be interpreted via the system as both provable and true at the same time. So in the strictest sense the system cannot be complete... but have we shown that it is missing anything except these incredibly tortuous, specific Goedel numbers? Isn't it a bit of a dead end?
(happy to be corrected on this)
(happy to be corrected on this)
It's easier to answer that question about the Halting Problem, so here's Scott Aaronson proving it as a corollary to the Halting Problem: http://www.scottaaronson.com/blog/?p=710
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).
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).
My personal pet peeve is the Halting problem - yes, we can't prove interesting things for 'set of all possible inputs'.
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.
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.
It is unclear to me whether you are advocating for a programming style that you think is desirable but nonexistent, or if you're advocating for a programming style without naming it.
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 .
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 .
you're right.
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"...
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"...
Keep in mind that real world computers just have a very large (but not unbounded) amount of tape. Since they have constant space, they are really just DFAs.
Does taking input from the outside (e.g. internet) change this?
If Peano arithmetic (PA) is consistent, the following statements are true but not provable in PA:
1) Consistency of PA
2) http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theore...
3) http://en.wikipedia.org/wiki/Goodstein%27s_theorem
1) Consistency of PA
2) http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theore...
3) http://en.wikipedia.org/wiki/Goodstein%27s_theorem
But that's not much of a practical problem, since ZF set theory proves them both.
Ah, but the consistency of ZFC itself is undecidable from within ZFC! [1] I see what you're saying; it's quite the rabbit hole, however.
[1]: https://en.wikipedia.org/wiki/List_of_statements_undecidable...
[1]: https://en.wikipedia.org/wiki/List_of_statements_undecidable...
You are correct that Goedel really isn't hard. And, of course, its not a problem but a theory.
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.
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.
I've read through Godel Escher Bach, and I loved it, but I never really felt like I had a handle on Incompleteness theorem.
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
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
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...