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.
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.