I know this is supposed to be just introductory, but I actually think that the complete reformulation of UDT-with-a-halting-oracle in terms of modal logic is really interesting! For starters, it allows us to compare UDT and modal agents in the same framework (with the right o’s, we can see this version of UDT as a modal agent). It would also be really neat if we could write an “interpreter” that allows us to write UDT as a program calling a halting oracle, and then evaluate what it does by way of modal logic.
But also, it allows us to give a nice definition of “decision theory” and “decision problem” in the context with halting oracles. I was planning on posting soon about the definition that I showed you when you were visiting, which is designed for actually computable agents with bounded proof lengths, and is more complicated because of that. As a stepping stone to that, using the provability logic framework, I think we can define:
a decision theory to be a set of fully modalized formulas Fi(a1,…,am,o1,…,on), for i=1,…,m (fully modalized meaning that the propositional arguments only appear inside boxes);
and a decision problem to be a set of formulas Gj(a1,…,am), for j=1,…,n, which do not need to be modalized (which isn’t a problem because they’re not self-referential).
The condition that Fi must be fully modalized, but Gj doesn’t need to be, seems to be the natural thing corresponding to how in the bounded case, we allow the universe to run the agent, but the agent must use abstract reasoning about the universe, it can’t just run it.
Given such a set, we can define ~Fi(a1,…,am), for i=1,…,m, as follows:
~Fi(a1,…,am):=Fi(a1,…,am,G1(a1,…,am),…,Gn(a1,…,am)).
Then the actual action taken by decision theory F when run on the decision problem G is the modal fixed point of the equations Ai↔~Fi(A1,…,Am), for i=1,…,m.
Yes, modal logic seems to be the most natural setting for these kinds of ideas. Also the “chicken rule” from the usual oracle formulations is gone now, I can’t remember why we needed it anymore.
In a probabilistic setting (with a prior over logical theories), EDT wants to condition on the possible actions with a Bayesian conditional, in order to then find the expected utility of each action.
If the agent can prove that it will take a particular action, then conditioning on this action may yield inconsistent stuff (divide-by-zero error for Bayesian conditional). This makes the result ill-defined.
The chicken rule makes this impossible, ensuring that the conditional probabilities are well defined.
So, the chicken rule at least seems useful for EDT.
A model of UDT with a halting oracle searches only for one utility value for each action. I’m guessing the other formulation just wasn’t obvious at the time? (I don’t remember realizing the possibility of playing chicken implicitly before Will Sawin advertised it to me, though I think he attributed it to you.)
I know this is supposed to be just introductory, but I actually think that the complete reformulation of UDT-with-a-halting-oracle in terms of modal logic is really interesting! For starters, it allows us to compare UDT and modal agents in the same framework (with the right o’s, we can see this version of UDT as a modal agent). It would also be really neat if we could write an “interpreter” that allows us to write UDT as a program calling a halting oracle, and then evaluate what it does by way of modal logic.
But also, it allows us to give a nice definition of “decision theory” and “decision problem” in the context with halting oracles. I was planning on posting soon about the definition that I showed you when you were visiting, which is designed for actually computable agents with bounded proof lengths, and is more complicated because of that. As a stepping stone to that, using the provability logic framework, I think we can define:
a decision theory to be a set of fully modalized formulas Fi(a1,…,am,o1,…,on), for i=1,…,m (fully modalized meaning that the propositional arguments only appear inside boxes);
and a decision problem to be a set of formulas Gj(a1,…,am), for j=1,…,n, which do not need to be modalized (which isn’t a problem because they’re not self-referential).
The condition that Fi must be fully modalized, but Gj doesn’t need to be, seems to be the natural thing corresponding to how in the bounded case, we allow the universe to run the agent, but the agent must use abstract reasoning about the universe, it can’t just run it.
Given such a set, we can define ~Fi(a1,…,am), for i=1,…,m, as follows: ~Fi(a1,…,am):=Fi(a1,…,am,G1(a1,…,am),…,Gn(a1,…,am)). Then the actual action taken by decision theory F when run on the decision problem G is the modal fixed point of the equations Ai↔~Fi(A1,…,Am), for i=1,…,m.
Yes, modal logic seems to be the most natural setting for these kinds of ideas. Also the “chicken rule” from the usual oracle formulations is gone now, I can’t remember why we needed it anymore.
In a probabilistic setting (with a prior over logical theories), EDT wants to condition on the possible actions with a Bayesian conditional, in order to then find the expected utility of each action.
If the agent can prove that it will take a particular action, then conditioning on this action may yield inconsistent stuff (divide-by-zero error for Bayesian conditional). This makes the result ill-defined.
The chicken rule makes this impossible, ensuring that the conditional probabilities are well defined.
So, the chicken rule at least seems useful for EDT.
A model of UDT with a halting oracle searches only for one utility value for each action. I’m guessing the other formulation just wasn’t obvious at the time? (I don’t remember realizing the possibility of playing chicken implicitly before Will Sawin advertised it to me, though I think he attributed it to you.)