I think I don’t understand the Löb’s theorem example.
If A=5⇒U=5∧A=10⇒U=0 is provable, then A=5, so it is true (because the statement about A=10 is vacuously true). Hence by Löb’s theorem, it’s provable, so we get A=5.
If A=10⇒U=0∧A=10⇒U=10 is provable, then it’s true, for the dual reason. So by Löb, it’s provable, so A=10.
The broader point about being unable to reason yourself out of a bad decision if your prior for your own decisions doesn’t contain a “grain of truth” makes sense, but it’s not clear we can show that the agent in this example will definitely get stuck on the bad decision—if anything, the above argument seems to show that the system has to be inconsistent! If that’s true, I would guess that the source of this inconsistency is assuming the agent has sufficient reflective capacity to prove “If I can prove A=5, then A=5. Which would suggest learning the lesson that it’s hard for agents to reason about their own behaviour with logical consistency.
The agent has been constructed such that Provable(“5 is the best possible action”) implies that 5 is the best (only!) possible action. Then by Löb’s theorem, 5 is the only possible action. It cannot also be simultaneously constructed such that Provable(“10 is the best possible action”) implies that 10 is the only possible action, because then it would also follow that 10 is the only possible action. That’s not just our proof system being inconsistent, that’s false!
(There was a LaTeX error in my comment, which made it totally illegible. But I think you managed to resolve my confusion anyway).
I see! It’s not provable that Provable(A=10⇒U=10) implies A=10. It seems like it should be provable, but the obvious argument relies on the assumption that, if *A=10⇒U=0 is provable, then it’s not also provable that A=10⇒U=10 - in other words, that the proof system is consistent! Which may be true, but is not provable.
The asymmetry between 5 and 10 is that, to choose 5, we only need a proof that 5 is optimal, but to choose 10, we need to not find a proof that 5 is optimal. Which seems easier than finding a proof that 10 is optimal, but is not provably easier.
I think I don’t understand the Löb’s theorem example.
If A=5⇒U=5∧A=10⇒U=0 is provable, then A=5, so it is true (because the statement about A=10 is vacuously true). Hence by Löb’s theorem, it’s provable, so we get A=5.
If A=10⇒U=0∧A=10⇒U=10 is provable, then it’s true, for the dual reason. So by Löb, it’s provable, so A=10.
The broader point about being unable to reason yourself out of a bad decision if your prior for your own decisions doesn’t contain a “grain of truth” makes sense, but it’s not clear we can show that the agent in this example will definitely get stuck on the bad decision—if anything, the above argument seems to show that the system has to be inconsistent! If that’s true, I would guess that the source of this inconsistency is assuming the agent has sufficient reflective capacity to prove “If I can prove A=5, then A=5. Which would suggest learning the lesson that it’s hard for agents to reason about their own behaviour with logical consistency.
The agent has been constructed such that Provable(“5 is the best possible action”) implies that 5 is the best (only!) possible action. Then by Löb’s theorem, 5 is the only possible action. It cannot also be simultaneously constructed such that Provable(“10 is the best possible action”) implies that 10 is the only possible action, because then it would also follow that 10 is the only possible action. That’s not just our proof system being inconsistent, that’s false!
(There was a LaTeX error in my comment, which made it totally illegible. But I think you managed to resolve my confusion anyway).
I see! It’s not provable that Provable(A=10⇒U=10) implies A=10. It seems like it should be provable, but the obvious argument relies on the assumption that, if *A=10⇒U=0 is provable, then it’s not also provable that A=10⇒U=10 - in other words, that the proof system is consistent! Which may be true, but is not provable.
The asymmetry between 5 and 10 is that, to choose 5, we only need a proof that 5 is optimal, but to choose 10, we need to not find a proof that 5 is optimal. Which seems easier than finding a proof that 10 is optimal, but is not provably easier.