Change the choice rule to: Return the action for which S does not prove that A()≠a, and which corresponds to the highest utility found on step 2 among all such actions.
Your scheme doesn’t guarantee that all actions will be considered, or that a known collection of proofs of statements [A()=a ⇒ U()=u] will generate the action that agent actually chooses. If S proves that A()=a1, a1 is what your agent will choose, without any consequentialist reason for this choice apparent in the decision algorithm. You are letting S decide for you, implementing a kind of fatalist decision-making, asking “What do the laws of nature say I’m going to do?” instead of “What should I do?” The chicken rule (diagonal step) is what provides these guarantees (there are likely other ways to this same end).
I visualized the process like this: S would start proving things. It will notice that “if S does not prove A()!=a AND S does not prove A()!=b AND AgentStep2Proves(“A()=a ⇒ U()=u”) AND AgentStep2Proves(“A()=b ⇒ U()=w”) AND u>w THEN A()!=b”, so it would prove A()!=b. Etc.
Which is wrong since it makes S look on itself, which would make it inconsistent. Except it is inconsistent anyway...
On the other hand, this method still does not let the agent prove its decision, since it would make the step 2 explode. Damn, I’m stupid :(
But this should work. It’s just TDT, I think. Does it have serious drawbacks that make UDT/ADT desirable?
Another possible modification of the algorithm:
Remove the playing chicken step.
Keep the step 2 - proving “A()=a ⇒ U()=u”.
Change the choice rule to:
Return the action for which S does not prove that A()≠a, and which corresponds to the highest utility found on step 2 among all such actions.
Your scheme doesn’t guarantee that all actions will be considered, or that a known collection of proofs of statements [A()=a ⇒ U()=u] will generate the action that agent actually chooses. If S proves that A()=a1, a1 is what your agent will choose, without any consequentialist reason for this choice apparent in the decision algorithm. You are letting S decide for you, implementing a kind of fatalist decision-making, asking “What do the laws of nature say I’m going to do?” instead of “What should I do?” The chicken rule (diagonal step) is what provides these guarantees (there are likely other ways to this same end).
I visualized the process like this: S would start proving things. It will notice that “if S does not prove A()!=a AND S does not prove A()!=b AND AgentStep2Proves(“A()=a ⇒ U()=u”) AND AgentStep2Proves(“A()=b ⇒ U()=w”) AND u>w THEN A()!=b”, so it would prove A()!=b. Etc.
Which is wrong since it makes S look on itself, which would make it inconsistent. Except it is inconsistent anyway...
On the other hand, this method still does not let the agent prove its decision, since it would make the step 2 explode. Damn, I’m stupid :(
But this should work. It’s just TDT, I think. Does it have serious drawbacks that make UDT/ADT desirable?