I don’t see why the proof fails here; it seems to go essentially as usual.
Reasoning in PA:
Suppose a=cross->u=-10 were provable.
Further suppose a=cross.
Note that we can see there’s a proof that not crossing gets 0, so it must be that a better (or equal) value was found for crossing, which must have been +10 unless PA is inconsistent, since crossing implies that u is either +10 or −10. Since we already assumed crossing gets −10, this leads to trouble in the usual way, and the proof proceeds from there.
(Actually, I guess everything is a little messier since you haven’t stipulated the search order for actions, so we have to examine more cases. Carrying out some more detailed reasoning: So (under our assumptions) we know PA must have proved (a=cross → u=10). But we already supposed that it proves (a=cross → u=-10). So PA must prove not(a=cross). But then it must prove prove(not(a=cross)), since PA has self-knowledge of proofs. Which means PA can’t prove that it’ll cross, if PA is to be consistent. But it knows that proving it doesn’t take an action makes that action very appealing; so it knows it would cross, unless not crossing was equally appealing. But it can prove that not crossing nets zero. So the only way for not crossing to be equally appealing is for PA to also prove not crossing nets 10. For this to be consistent, PA has to prove that the agent doesn’t not-cross. But now we have PA proving that the agent doesn’t cross and also that it doesn’t not cross! So PA must be inconsistent under our assumptions. The rest of the proof continues as usual.)
You are entirely correct; I don’t know why I was confused.
However, looking at the proof again, it seems there might be a potential hole. You use Löb’s theorem within an assumption sub-loop. This seems to assume that from “A→(□B→B)”, we can deduce “A→B”.
But this cannot be true in general! To see this, set A=□B→B. Then A→(□B→B), trivially; if, from that, we could deduce A→B, we would have (□B→B)→B for any B. But this statement, though it looks like Löb’s theorem, is one that we cannot deduce in general (see Eliezer’s “medium-hard problem” here).
Can this hole be patched?
(note that if A→(□AB→B), where □A is a PA proof that adds A as an extra axiom, then we can deduce A→B).
I don’t see why the proof fails here; it seems to go essentially as usual.
Reasoning in PA:
Suppose a=cross->u=-10 were provable.
Further suppose a=cross.
Note that we can see there’s a proof that not crossing gets 0, so it must be that a better (or equal) value was found for crossing, which must have been +10 unless PA is inconsistent, since crossing implies that u is either +10 or −10. Since we already assumed crossing gets −10, this leads to trouble in the usual way, and the proof proceeds from there.
(Actually, I guess everything is a little messier since you haven’t stipulated the search order for actions, so we have to examine more cases. Carrying out some more detailed reasoning: So (under our assumptions) we know PA must have proved (a=cross → u=10). But we already supposed that it proves (a=cross → u=-10). So PA must prove not(a=cross). But then it must prove prove(not(a=cross)), since PA has self-knowledge of proofs. Which means PA can’t prove that it’ll cross, if PA is to be consistent. But it knows that proving it doesn’t take an action makes that action very appealing; so it knows it would cross, unless not crossing was equally appealing. But it can prove that not crossing nets zero. So the only way for not crossing to be equally appealing is for PA to also prove not crossing nets 10. For this to be consistent, PA has to prove that the agent doesn’t not-cross. But now we have PA proving that the agent doesn’t cross and also that it doesn’t not cross! So PA must be inconsistent under our assumptions. The rest of the proof continues as usual.)
You are entirely correct; I don’t know why I was confused.
However, looking at the proof again, it seems there might be a potential hole. You use Löb’s theorem within an assumption sub-loop. This seems to assume that from “A→(□B→B)”, we can deduce “A→B”.
But this cannot be true in general! To see this, set A=□B→B. Then A→(□B→B), trivially; if, from that, we could deduce A→B, we would have (□B→B)→B for any B. But this statement, though it looks like Löb’s theorem, is one that we cannot deduce in general (see Eliezer’s “medium-hard problem” here).
Can this hole be patched?
(note that if A→(□AB→B), where □A is a PA proof that adds A as an extra axiom, then we can deduce A→B).