I was reading Eliezer’s cartoon proof of Lob’s theorem the other day and I didn’t get it. My assumption was that in order to understand it, I would need a decent background in mathematical logic, e.g. actually know what Peano Arithmetic is as opposed to abstracting it away as a talking head that tells us things. (I know vector calculus, linear algebra, programming, and basic logic but that’s about as far as I go.) If Lob’s theorem is something that I should be able to understand the proof of given that background, I’d be interested to know that.
The book does not have any prerequisites. It starts out with plain English logic puzzles that you need to solve (detailed solutions at the end of each chapter), and later introduces you to formal logic by translating those puzzles into propositional logic.
I have not yet finished the book, so I can’t tell if it fits the purpose of understanding Löb’s theorem. But what I can already tell is that it is really engaging and fascinating. Highly recommended!
ETA: To give a taste of Raymond M. Smullyan’s style, check out his ‘World’s shortest explanation of Gödel’s theorem’:
We have some sort of machine that prints out statements in some sort of language. It needn’t be a statement-printing machine exactly; it could be some sort of technique for taking statements and deciding if they are true. But let’s think of it as a machine that prints out statements.
In particular, some of the statements that the machine might (or might not) print look like these:
P*x (which means that the machine will print x)
NP*x (which means that the machine will never print x)
PR*x (which means that the machine will print xx)
NPR*x (which means that the machine will never print xx)
For example, NPR*FOO means that the machine will never print FOOFOO. NP*FOOFOO means the same thing. So far, so good.
Now, let’s consider the statement NPR*NPR*. This statement asserts that the machine will never print NPR*NPR*.
Either the machine prints NPR*NPR*, or it never prints NPR*NPR*.
If the machine prints NPR*NPR*, it has printed a false statement. But if the machine never prints NPR*NPR*, then NPR*NPR* is a true statement that the machine never prints.
So either the machine sometimes prints false statements, or there are true statements that it never prints.
So any machine that prints only true statements must fail to print some true statements.
Or conversely, any machine that prints every possible true statement must print some false statements too.
The problem I find with all pop-level proofs of Gödel’s theorems and similar material, including this one, is that they gloss over a key component: how to make a machine that talks about itself. After the part quoted above, a blogger (not Smullyan) does go on to say:
The proof of Gödel’s theorem shows that there are statements of pure arithmetic that essentially express NPRNPR; the trick is to find some way to express NPRNPR as a statement about arithmetic, and most of the technical details (and cleverness!) of Gödel’s theorem are concerned with this trick.
No explanation of this essential part of the proof is given. Unless you do that part, there’s nothing in the supposed proof to limit it to systems that include arithmetic.
Thank you for sharing that little snippet because I’m going to have to read italicsForever Undecideditalics now. Those last four lines were the photon my brain has waited for.
If you already understand Gödel’s first and second incompleteness theorems, then you can find a much simpler proof of Löb’s theorem in this pdf, pages 6-7.
I was reading Eliezer’s cartoon proof of Lob’s theorem the other day and I didn’t get it. My assumption was that in order to understand it, I would need a decent background in mathematical logic, e.g. actually know what Peano Arithmetic is as opposed to abstracting it away as a talking head that tells us things. (I know vector calculus, linear algebra, programming, and basic logic but that’s about as far as I go.) If Lob’s theorem is something that I should be able to understand the proof of given that background, I’d be interested to know that.
In order to understand it, I am currently reading Forever Undecided: A Puzzle Guide to Gödel. The book features a whole chapter about Löb’s theorem.
The book does not have any prerequisites. It starts out with plain English logic puzzles that you need to solve (detailed solutions at the end of each chapter), and later introduces you to formal logic by translating those puzzles into propositional logic.
I have not yet finished the book, so I can’t tell if it fits the purpose of understanding Löb’s theorem. But what I can already tell is that it is really engaging and fascinating. Highly recommended!
ETA: To give a taste of Raymond M. Smullyan’s style, check out his ‘World’s shortest explanation of Gödel’s theorem’:
We have some sort of machine that prints out statements in some sort of language. It needn’t be a statement-printing machine exactly; it could be some sort of technique for taking statements and deciding if they are true. But let’s think of it as a machine that prints out statements.
In particular, some of the statements that the machine might (or might not) print look like these:
P*x (which means that the machine will print x)
NP*x (which means that the machine will never print x)
PR*x (which means that the machine will print xx)
NPR*x (which means that the machine will never print xx)
For example, NPR*FOO means that the machine will never print FOOFOO. NP*FOOFOO means the same thing. So far, so good.
Now, let’s consider the statement NPR*NPR*. This statement asserts that the machine will never print NPR*NPR*.
Either the machine prints NPR*NPR*, or it never prints NPR*NPR*.
If the machine prints NPR*NPR*, it has printed a false statement. But if the machine never prints NPR*NPR*, then NPR*NPR* is a true statement that the machine never prints.
So either the machine sometimes prints false statements, or there are true statements that it never prints.
So any machine that prints only true statements must fail to print some true statements.
Or conversely, any machine that prints every possible true statement must print some false statements too.
The problem I find with all pop-level proofs of Gödel’s theorems and similar material, including this one, is that they gloss over a key component: how to make a machine that talks about itself. After the part quoted above, a blogger (not Smullyan) does go on to say:
No explanation of this essential part of the proof is given. Unless you do that part, there’s nothing in the supposed proof to limit it to systems that include arithmetic.
A few years ago, I tried to write a friendly introduction to this technical part.
Thank you for sharing that little snippet because I’m going to have to read italicsForever Undecideditalics now. Those last four lines were the photon my brain has waited for.
If you already understand Gödel’s first and second incompleteness theorems, then you can find a much simpler proof of Löb’s theorem in this pdf, pages 6-7.