= 27d567bc2d48d9f40e9ccc20ea370b15)
arundelo comments on Welcome to Less Wrong! - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (1953)
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.