Does anyone know a good resource to go with Eliezer’s comic guide on Lob’s Theorem? It’s confusing me a… well, a lot.
Or, if it’s the simplest resource on it out there, are there any prerequisites for learning it/ skills/ knowledge that would help?
I’m trying to build up a basis of skills so I can participate better here, but I’ve got a long way to go. Most of my skills in science, maths and logic are pretty basic.
Or, if it’s the simplest resource on it out there, are there any prerequisites for learning it/ skills/ knowledge that would help?
I’m trying to build up a basis of skills so I can participate better here, but I’ve got a long way to go. Most of my skills in science, maths and logic are pretty basic.
Definitely read Gödel, Escher, Bach. Aside from that, here’s a great list of reading and resources for better understanding various topics discussed on LW. (The things under Mathematics → Logic and Mathematics → Foundations would be the most relevant to Löb’s Theorem.)
I bet if you found the first spot in it where you get
confused and asked about it here, someone could help.
(Maybe not me; I have barely a nodding acquaintance with
Löb’s theorem, and the linked piece has been languishing on
my to-read list for a while.)
Okay. The part where I start getting confused is the statement: ‘Unfortunately, Lob’s Theorem demonstrates that if we could prove the above within PA, then PA would prove 1 + 2 = 5’. How does PA ‘not prov(ing) 1 + 2 = 5’ (the previous statement) mean that it would prove 1 + 2 = 5?
Maybe it’s something I’m not understanding about something proving itself—proof within PA—as I admit I can’t see exactly how this works. It says earlier that Godel developed a system for this, but the theorem doesn’t seem to explain that system… my understanding of the theorem is this: ‘if PA proves that when it proves something it’s right, then what it proves is right.’ That statement makes sense to me, but I don’t see how it links in or justify’s everything else. I mean, it seems to just be word play—very basic concept.
I feel like I’m missing something fundamental and basic. What I do seem to understand is so self-explanatory as to need no mention, and what I don’t seems separate from it. It’s carrying on from points as if they are self-explanatory and link, when I can’t see the explanations or make the links. I also don’t see the point of this as a whole—what, practically, is it used for? Or is it simply an exercise in thinking logically?
Oh, I also don’t know what the arrows and little squares stand for in the problem displayed after the comic. That’s a separate issue, but answers on it would be great.
‘Unfortunately, Lob’s Theorem demonstrates that if we
could prove the above within PA, then PA would prove 1 + 2
= 5’.
I believe that that’s just a statement of Löb’s theorem, and
the rest of the Cartoon Guide is a proof.
It says earlier that Godel developed a system for this,
but the theorem doesn’t seem to explain that system
The exact details aren’t important, but Gödel came up with a
way of using a system that talks about natural numbers to
talk about things like proofs. As
Wikipedia
puts it:
Thus, in a formal theory such as Peano arithmetic in which
one can make statements about numbers and their
arithmetical relationships to each other, one can use a
Gödel numbering to indirectly make statements about the
theory itself.
Actually, going through a proof (it doesn’t need to be
formal) of
Gödel’s incompleteness theorem(s)
would probably be good background to have for the Cartoon
Guide. The one I read long ago was the one in
Gödel, Escher, Bach;
someone else might be able to recommend a good one that’s
available online not embedded in a book (although you should
read GEB at some point anyway).
arrows and little squares
The rightward-pointing arrows
mean “If [thing to the left of
the arrow] then [thing to the right of the arrow]”. E.g.
if A stands for “Socrates is drinking hemlock” and B stands
for “Socrates will die” then “A → B” means “If Socrates is
drinking hemlock then Socrates will die”.
I suspect the squares were originally some other symbol when
this was first posted on Overcoming Bias, and they got
messed up when it was moved here
[Edit:nope, they’re supposed to be squares],
but in any case, here they
mean “[thing to the right of the square] is provable”. And
the parentheses are just used for grouping, like in algebra.
Ah, okay, I think I understand it a bit better now. Thank you!
I think I will order Godel, Escher, Bach. I’ve seen it mentioned a few times around this site, but my library got rid of the last copy a month or so before I heard of it—without replacing it. Apparently it was just too old.
Does anyone know a good resource to go with Eliezer’s comic guide on Lob’s Theorem? It’s confusing me a… well, a lot.
Or, if it’s the simplest resource on it out there, are there any prerequisites for learning it/ skills/ knowledge that would help?
I’m trying to build up a basis of skills so I can participate better here, but I’ve got a long way to go. Most of my skills in science, maths and logic are pretty basic.
Thanks in advance.
Definitely read Gödel, Escher, Bach. Aside from that, here’s a great list of reading and resources for better understanding various topics discussed on LW. (The things under Mathematics → Logic and Mathematics → Foundations would be the most relevant to Löb’s Theorem.)
Thanks! That looks like a great list, just what I need.
I bet if you found the first spot in it where you get confused and asked about it here, someone could help. (Maybe not me; I have barely a nodding acquaintance with Löb’s theorem, and the linked piece has been languishing on my to-read list for a while.)
Edit: cousin_it recommends part of a Scott Aaronson paper.
Okay. The part where I start getting confused is the statement: ‘Unfortunately, Lob’s Theorem demonstrates that if we could prove the above within PA, then PA would prove 1 + 2 = 5’. How does PA ‘not prov(ing) 1 + 2 = 5’ (the previous statement) mean that it would prove 1 + 2 = 5?
Maybe it’s something I’m not understanding about something proving itself—proof within PA—as I admit I can’t see exactly how this works. It says earlier that Godel developed a system for this, but the theorem doesn’t seem to explain that system… my understanding of the theorem is this: ‘if PA proves that when it proves something it’s right, then what it proves is right.’ That statement makes sense to me, but I don’t see how it links in or justify’s everything else. I mean, it seems to just be word play—very basic concept.
I feel like I’m missing something fundamental and basic. What I do seem to understand is so self-explanatory as to need no mention, and what I don’t seems separate from it. It’s carrying on from points as if they are self-explanatory and link, when I can’t see the explanations or make the links. I also don’t see the point of this as a whole—what, practically, is it used for? Or is it simply an exercise in thinking logically?
Oh, I also don’t know what the arrows and little squares stand for in the problem displayed after the comic. That’s a separate issue, but answers on it would be great.
Any help would be appreciated. Thanks.
I believe that that’s just a statement of Löb’s theorem, and the rest of the Cartoon Guide is a proof.
The exact details aren’t important, but Gödel came up with a way of using a system that talks about natural numbers to talk about things like proofs. As Wikipedia puts it:
Actually, going through a proof (it doesn’t need to be formal) of Gödel’s incompleteness theorem(s) would probably be good background to have for the Cartoon Guide. The one I read long ago was the one in Gödel, Escher, Bach; someone else might be able to recommend a good one that’s available online not embedded in a book (although you should read GEB at some point anyway).
The rightward-pointing arrows mean “If [thing to the left of the arrow] then [thing to the right of the arrow]”. E.g. if A stands for “Socrates is drinking hemlock” and B stands for “Socrates will die” then “A → B” means “If Socrates is drinking hemlock then Socrates will die”.
I suspect the squares were originally some other symbol when this was first posted on Overcoming Bias, and they got messed up when it was moved here [Edit: nope, they’re supposed to be squares], but in any case, here they mean “[thing to the right of the square] is provable”. And the parentheses are just used for grouping, like in algebra.
Ah, okay, I think I understand it a bit better now. Thank you!
I think I will order Godel, Escher, Bach. I’ve seen it mentioned a few times around this site, but my library got rid of the last copy a month or so before I heard of it—without replacing it. Apparently it was just too old.