Sure, not a strong motivation, that’s why I said “question suggested by the post” (we are talking of two different questions now...). The second question seems to be mainly about interpreting agent’s activity, not directly about construction of agents, so I don’t expect a game that clearly requires this kind of analysis. (For example, all agents are “just programs” (perhaps with “just oracles”), so any talk of formal systems used by agents is something in addition, a method of understanding them, even if it results in useful designs.)
On the other hand, if we want the agent to remain ignorant of its own actions, adding axioms that decide the actions to agent’s own theory from the very start is not an option, so describing a procedure for adding them later is a way of keeping both of the requirements: a strong theory and consistency of counterfactuals at each decision.
Sure, not a strong motivation, that’s why I said “question suggested by the post” (we are talking of two different questions now...). The second question seems to be mainly about interpreting agent’s activity, not directly about construction of agents, so I don’t expect a game that clearly requires this kind of analysis. (For example, all agents are “just programs” (perhaps with “just oracles”), so any talk of formal systems used by agents is something in addition, a method of understanding them, even if it results in useful designs.)
On the other hand, if we want the agent to remain ignorant of its own actions, adding axioms that decide the actions to agent’s own theory from the very start is not an option, so describing a procedure for adding them later is a way of keeping both of the requirements: a strong theory and consistency of counterfactuals at each decision.