This is really nicely written, but unfortunately the main lesson for me is that I don’t understand the Löb’s Theorem. Despite reading the linked PDF file a few times. So I guess I will use this place to ask you a few things, since I like your way of explaining.
First, I may have just ruined my math credentials by admitting that I don’t understand Löb’s Theorem, but it doesn’t mean that I suck at maths completely. I feel pretty confident in elementary- and maybe even high-school math. Let’s say that I am confident I would never tell someone that 2+2=3.
Second, if I understand the rules for implication correctly, if the premise is false, the implication is always true. Things like “if 2+2=3, then Eliezer will build a Friendly AI” should be pretty non-controversial even outside of LessWrong.
So it seems to me that I can safely say “if I tell you that 2+2=3, then 2+2=3”. (Because I know I would never say that 2+2=3.)
But Mr. Löb insists that it means that I just claimed that 2+2=3.
And I feel like Mr. Löb is totally strawmanning me.
Oh thanks; I hope I am able to explain it adequately. Your understanding of implication, and what Löb’s theorem would imply about yourself (assuming you are a formal mathematical system, of course) are both correct. More formally, for any formal system S at least containing Peano Arithmetic, if this system can prove: (If PA proves that 2+2=3, then 2+2 really is 3), then the system will also prove that 2+2=3. This is pretty bad, since 2+2=4, so we must declare the system inconsistent. This flies pretty strongly against most people’s intuition—but since it is true, it’s your intuition that needs to be retrained.
The analogy to ‘being suspicious’ hopefully helps brings in some of the right connotations and intuition. Of course, it’s not a perfect analogy, since as you mentioned, this is kind of an uncharitable way to interpret people.
Anyway, I feel less confident that I can explain the proof of Löb’s theorem intuitively, but here’s a jab at it:
Peano Arithmetic (PA) is surprisingly powerful. In much the same way that we can store and process all sorts of information on computers as binary numbers, we can write all sorts of statements (including statements about PA itself) as numbers. And similar to how all the processing on a computer is reduced to operations with simple transistors, we can encode all the rules of inference for these statements as arithmetic functions.
In particular, we can encode a statement L that says “If a proof of L exists (in PA), then X is true,” where the X can be arbitrary.
Now PA can think, “well if I had a proof of L, then unpacking what L means, I could prove that (if a proof of L exists, then X is true).”
“I also know that if I had a proof of L, then I could prove that I can prove L.”
“So I can just skip ahead and see that—if I had a proof of L, then I could prove that X is true.”
A dishonest PA may then reason—“Since I trust myself, if I knew I had a proof of L, then X would just be true.” @
“I can also prove this fact about myself—that if I had a proof of L, then X is true.”
“But that’s exactly what L says! So I can prove that I can prove L”
“So going back to @, I now know that X is true!”
But X can be literally anything! So this is really bad.
At a coarser level, you can think of BoxXrightarrowX as breathing life into things you imagine about yourself. You can try to be careful to only imagine things you can actually see yourself doing, but there are tricky statements like L that can use this to smuggle arbitrary statements out of your imagination into real life! L says, “if you imagine L, then X is true.” Even though this is just a statement, and is neither true nor false a priori, you still have to be careful thinking about it. You need a solid barrier between the things you imagine about yourself, and the things you actually do, to protect yourself from getting ‘hacked’ by this statement.
Hopefully something in here helps the idea ‘click’ for you. Feel free to ask more questions!
Thanks. I will look at it again tomorrow, but now I guess I have an approximate idea how it goes.
1) We can create various self-referential statements that syntaxtically seem completely innocent. They are composed from the same components and in the same way as ordinary (non-self-referential) statements. So, if the obviously innocent statements are allowed to be made, the clever schemes for creating self-referential statements will be allowed, too. -- This is the first thing to think about, separately from the rest.
2) Self-referential statements are allowed to speak about themselves, and also about me (a given axiomatic system). Thus they can abuse me in various ways which I can’t really avoid. Because even if I tried to refuse thinking about them, they can make themselves mean “Viliam refuses to think about me”, and provide me a step-by-step proof, which I would have to admit is correct. Then they make themselves something like “If Viliam says I am correct, then 2+2=3″, which I cannot avoid or deny, because both would make the statement true, so the only remaining option is to admit it, which means I have admitted that 2+2=3. -- This is another thing to think about., because I don’t feel really convinced by what I wrote. I realize that both avoiding to answer, or saying that the statement is incorrect would be wrong… and yet I somehow can’t imagine in detail how specifically could I say it was true.
Maybe a better intuition instead of seeing myself as an axiomatic system (which I am not) would be to imagine that at the beginning I precommit to use a specific PA-compatible list of rules… and then I follow the rules blindly, even when I see that the clever statements somehow force me to do things that are somehow wrong, but technically okay according to those rules.
Part of the issue is that you are not subject to the principle of explosion. You can assert contradictory things without also asserting that 2+2=3, so you can be confident that you will never tell anyone that 2+2=3 without being confident that you will never contradict yourself. Formal systems using classical logic can’t do this: if they prove any contradiction at all, they also prove that 2+2=3, so proving that they don’t prove 2+2=3 is exactly the same thing as proving that they are perfectly consistent, which they can’t consistently do.
This is really nicely written, but unfortunately the main lesson for me is that I don’t understand the Löb’s Theorem. Despite reading the linked PDF file a few times. So I guess I will use this place to ask you a few things, since I like your way of explaining.
First, I may have just ruined my math credentials by admitting that I don’t understand Löb’s Theorem, but it doesn’t mean that I suck at maths completely. I feel pretty confident in elementary- and maybe even high-school math. Let’s say that I am confident I would never tell someone that 2+2=3.
Second, if I understand the rules for implication correctly, if the premise is false, the implication is always true. Things like “if 2+2=3, then Eliezer will build a Friendly AI” should be pretty non-controversial even outside of LessWrong.
So it seems to me that I can safely say “if I tell you that 2+2=3, then 2+2=3”. (Because I know I would never say that 2+2=3.)
But Mr. Löb insists that it means that I just claimed that 2+2=3.
And I feel like Mr. Löb is totally strawmanning me.
Please help!
Oh thanks; I hope I am able to explain it adequately. Your understanding of implication, and what Löb’s theorem would imply about yourself (assuming you are a formal mathematical system, of course) are both correct. More formally, for any formal system S at least containing Peano Arithmetic, if this system can prove: (If PA proves that 2+2=3, then 2+2 really is 3), then the system will also prove that 2+2=3. This is pretty bad, since 2+2=4, so we must declare the system inconsistent. This flies pretty strongly against most people’s intuition—but since it is true, it’s your intuition that needs to be retrained.
The analogy to ‘being suspicious’ hopefully helps brings in some of the right connotations and intuition. Of course, it’s not a perfect analogy, since as you mentioned, this is kind of an uncharitable way to interpret people.
Anyway, I feel less confident that I can explain the proof of Löb’s theorem intuitively, but here’s a jab at it:
Peano Arithmetic (PA) is surprisingly powerful. In much the same way that we can store and process all sorts of information on computers as binary numbers, we can write all sorts of statements (including statements about PA itself) as numbers. And similar to how all the processing on a computer is reduced to operations with simple transistors, we can encode all the rules of inference for these statements as arithmetic functions.
In particular, we can encode a statement L that says “If a proof of L exists (in PA), then X is true,” where the X can be arbitrary.
Now PA can think, “well if I had a proof of L, then unpacking what L means, I could prove that (if a proof of L exists, then X is true).”
“I also know that if I had a proof of L, then I could prove that I can prove L.”
“So I can just skip ahead and see that—if I had a proof of L, then I could prove that X is true.”
A dishonest PA may then reason—“Since I trust myself, if I knew I had a proof of L, then X would just be true.” @
“I can also prove this fact about myself—that if I had a proof of L, then X is true.”
“But that’s exactly what L says! So I can prove that I can prove L”
“So going back to @, I now know that X is true!”
But X can be literally anything! So this is really bad.
At a coarser level, you can think of BoxXrightarrowX as breathing life into things you imagine about yourself. You can try to be careful to only imagine things you can actually see yourself doing, but there are tricky statements like L that can use this to smuggle arbitrary statements out of your imagination into real life! L says, “if you imagine L, then X is true.” Even though this is just a statement, and is neither true nor false a priori, you still have to be careful thinking about it. You need a solid barrier between the things you imagine about yourself, and the things you actually do, to protect yourself from getting ‘hacked’ by this statement.
Hopefully something in here helps the idea ‘click’ for you. Feel free to ask more questions!
Thanks. I will look at it again tomorrow, but now I guess I have an approximate idea how it goes.
1) We can create various self-referential statements that syntaxtically seem completely innocent. They are composed from the same components and in the same way as ordinary (non-self-referential) statements. So, if the obviously innocent statements are allowed to be made, the clever schemes for creating self-referential statements will be allowed, too. -- This is the first thing to think about, separately from the rest.
2) Self-referential statements are allowed to speak about themselves, and also about me (a given axiomatic system). Thus they can abuse me in various ways which I can’t really avoid. Because even if I tried to refuse thinking about them, they can make themselves mean “Viliam refuses to think about me”, and provide me a step-by-step proof, which I would have to admit is correct. Then they make themselves something like “If Viliam says I am correct, then 2+2=3″, which I cannot avoid or deny, because both would make the statement true, so the only remaining option is to admit it, which means I have admitted that 2+2=3. -- This is another thing to think about., because I don’t feel really convinced by what I wrote. I realize that both avoiding to answer, or saying that the statement is incorrect would be wrong… and yet I somehow can’t imagine in detail how specifically could I say it was true.
Maybe a better intuition instead of seeing myself as an axiomatic system (which I am not) would be to imagine that at the beginning I precommit to use a specific PA-compatible list of rules… and then I follow the rules blindly, even when I see that the clever statements somehow force me to do things that are somehow wrong, but technically okay according to those rules.
So, is the ontological argument a natural language application of Löb’s Theorem?
Part of the issue is that you are not subject to the principle of explosion. You can assert contradictory things without also asserting that 2+2=3, so you can be confident that you will never tell anyone that 2+2=3 without being confident that you will never contradict yourself. Formal systems using classical logic can’t do this: if they prove any contradiction at all, they also prove that 2+2=3, so proving that they don’t prove 2+2=3 is exactly the same thing as proving that they are perfectly consistent, which they can’t consistently do.
Unless I’m missing something, Löb’s theorem is still a theorem of minimal logic, which does not have the principle of explosion.