According to the first step of the algorithm, A will play chicken with the universe and return 1, making S inconsistent. So if S is consistent, that can’t happen.
Is this right? I’m wondering if you’re assuming soundness relative to the natural semantics about A, because in step one, it isn’t clear that there is a contradiction in S rather than a failure of S to be sound with respect to the semantics it’s supposed to model (what actions A can take and their utility). I might be confused, but wouldn’t this entail contradiction of the soundness of S rather than entailing that S is inconsistent? S would only be inconsistent if it can prove both A() = a and A()≠a, but unless you have further hidden assumptions about S I don’t see why A returning a would entail that S proves A() = a.
This is how I want to interpret this:
S is some deduction system capable of talking about all actions A() can make, and proving some range of utility results about them. S is also consistent and sound.
Play chicken with the universe: if S proves that A()≠a for some action a, then return a.
If S proves for all a there is some u such that [A() = a ⇒ U() = u] , output argmax (a) else exit and output nothing.
Since proving A can’t take an action a ( that is, A()≠a ) entails that S is not sound (because A will take such an action in step 1), S can’t prove any such result. Also, since proving that an action has two distinct utility values leads to A≠a, the soundness and consistency of S entails that this can’t happen. Does this seem right?
Also, step two seems too strong. Wouldn’t it suffice to have it be:
1) For all actions a, if there is some u such that [A() = a ⇒ U() = u] and u > 0, (), else add [A() = a ⇒ U() = 0] to the axioms of S (only for the duration of this decision)
2) output argmax (a)
My thought is that there could be some possible actions the agent can take that might not have provable utility and it seems like you should assign an expected utility of 0 to them (no value being privileged, it averages out to 0), but if you can prove that at least one action has positive utility, then you maximize expected utility by choosing the one with the highest positive utility.
This is weaker than the current step two but still seems to have the desired effect. Does this hold water or am I missing something?
I’m wondering if you’re assuming soundness relative to the natural semantics about A
You’re right. Misha already pointed that out and I edited the post.
For all actions a, if there is some u such that [A() = a ⇒ U() = u] and u > 0, else add [A() = a ⇒ U() = 0] to the axioms of S
Yeah, such a variation would work, but I’m uncomfortable calling A the optimal algorithm in a universe where some actions don’t have provable utility. Such universes often arise from non-symmetric multiplayer games and I’d rather not insinuate that I have a good solution for those.
Is this right? I’m wondering if you’re assuming soundness relative to the natural semantics about A, because in step one, it isn’t clear that there is a contradiction in S rather than a failure of S to be sound with respect to the semantics it’s supposed to model (what actions A can take and their utility). I might be confused, but wouldn’t this entail contradiction of the soundness of S rather than entailing that S is inconsistent? S would only be inconsistent if it can prove both A() = a and A()≠a, but unless you have further hidden assumptions about S I don’t see why A returning a would entail that S proves A() = a.
This is how I want to interpret this: S is some deduction system capable of talking about all actions A() can make, and proving some range of utility results about them. S is also consistent and sound.
Play chicken with the universe: if S proves that A()≠a for some action a, then return a.
If S proves for all a there is some u such that [A() = a ⇒ U() = u] , output argmax (a) else exit and output nothing.
Since proving A can’t take an action a ( that is, A()≠a ) entails that S is not sound (because A will take such an action in step 1), S can’t prove any such result. Also, since proving that an action has two distinct utility values leads to A≠a, the soundness and consistency of S entails that this can’t happen. Does this seem right?
Also, step two seems too strong. Wouldn’t it suffice to have it be:
1) For all actions a, if there is some u such that [A() = a ⇒ U() = u] and u > 0, (), else add [A() = a ⇒ U() = 0] to the axioms of S (only for the duration of this decision)
2) output argmax (a)
My thought is that there could be some possible actions the agent can take that might not have provable utility and it seems like you should assign an expected utility of 0 to them (no value being privileged, it averages out to 0), but if you can prove that at least one action has positive utility, then you maximize expected utility by choosing the one with the highest positive utility.
This is weaker than the current step two but still seems to have the desired effect. Does this hold water or am I missing something?
You’re right. Misha already pointed that out and I edited the post.
Yeah, such a variation would work, but I’m uncomfortable calling A the optimal algorithm in a universe where some actions don’t have provable utility. Such universes often arise from non-symmetric multiplayer games and I’d rather not insinuate that I have a good solution for those.