A while ago, drnickbone showed in a LessWrong post that for any decision theory, there is a "fair" decision problem on which that decision theory fails---that is, gets a low reward, even though a simple alternative decision theory gets a high reward. Although drnickbone's argument was given in words, it's intuitively clear that it could be formalized as math---except, what exactly do "decision theory" and "decision problem" mean in this context?
In this post, I'll propose definitions of these notions in the context of provability logic, as used in Vladimir Slepnev's modal version of UDT, and give a formalization of drnickbone's result. This implies that no single modal decision theory, including UDT, can behave optimally on all "fair" decision problems. But in my next post, I'll show that modal UDT is nevertheless optimal in a weaker sense: For every provably "fair" modal decision problem, there is a finite set of true axioms that can be added to PA, such that modal UDT using this extension of PA performs optimally on that decision problem. (This is a modal logic version of a result which Kenny Easwaran, Nate Soares and I recently showed in the context of bounded proof length, and which hasn't been published yet.)
Prerequisite: A primer on provability logic.
def U(): # Fill boxes, according to predicted action. box1 = 1000 box2 = 1000000 if (A() == 1) else 0 # Compute reward, based on actual action. return box2 if (A() == 1) else (box1 + box2)
In other words, we have a universe program, , which makes calls to an agent program, .
The agent program, in turn, uses quining to refer to the source code of the universe program. But while the universe is allowed to call the agent to figure out how it will behave, the agent can't just call the universe---or we'll have an infinite regress. Instead, we generally consider agents that use abstract reasoning in the form of proofs to reason about the universe they're in.
So a universe is a parameterless program, and a decision problem is a universe with a slot in it for an agent program. Similarly, an agent is a parameterless program, and a decision theory is an agent with a slot in it for the universe program. The universe can refer to the agent by calling it, but the agent can refer to the universe's source (and to its own source) only inside quoted formulas.
Let's say that a sequence of modal formulas are provably mutually exclusive and exhaustive, or p.m.e.e. for short, if proves that exactly one of them is true: For example, , and are p.m.e.e. if
We'll say that a (-outcome) modal universe is a sequence , or for short, of closed p.m.e.e. formulas, where is interpreted as the proposition that the 'th of the possible outcomes occurs.
Given a preference ranking on these possible outcomes, which has equivalence classes, we'll write for the modal formula asserting that one of the outcomes in the 'th ranked equivalence class has occurred; for example, if the preference ordering is such that , and are the most preferred outcomes, then . Clearly, (or for short) is a sequence of p.m.e.e. formulas; for brevity, we can avoid talking about , and call the sequence an -level universe.
(I'm using to mean "same formula".)
Similarly, an (-action) modal agent is a sequence , or for short, of closed p.m.e.e. formulas, where is interpreted as saying that the agent takes its 'th available action.
A modal (-action, -level) decision problem is an -level universe with a slot for an -action agent : that is, a p.m.e.e. sequence , or for short, where .
Similarly, a decision theory is an agent with a slot for a universe. However, the definition of decision theories isn't exactly analogous to that of decision problems, because we want to reflect the idea that the agent can't directly simulate the universe it's living in, but can only make reference to it inside quoted formulas; in the modal logic world, this translates to: "inside boxes". Thus, we define a modal (-action, -level) decision theory to be a p.m.e.e. sequence of fully modalized formulas , or for short, where .
(Aside: We could require one of these to be provably mutually exclusive and exhaustive only under the assumption that its argument is p.m.e.e., but my current guess is that it's not worth it.)
Now we can use the fixed point theorem to show that any modal decision theory has a well-defined output on any modal decision problem, and vice versa: Since is fully modalized, so is ---if we substitute the for , and all instances of were inside boxes, then all instances of in the resulting formula will be inside boxes as well. Thus, we can find a fixed point satisfying (which I'm using as shorthand for stating that holds for ).
By the uniqueness theorem, for any satisfying , we have , so our decision theory's action is well-defined. Moreover, by the rule about substitution of equivalent formulas, it follows that , meaning that the preference level that our decision theory achieves on this decision problem is well-defined as well.
Thus, for every pair of sequences , there's a pair such that and ; and this pair is unique up to provable equivalence.
Extensional (= "fair") decision problems
drnickbone's result states that for every decision theory, there is a "fair" decision problem which on which this decision theory fails, where "fair" means that an agent's reward depends only on its actions, not on its source code: Any two agents which output the same actions will achieve the same outcome. We can formalize this in modal logic as where I'm writing for the conjunction of the . We'll say that a modal decision problem is provably extensional if GL proves the above fairness condition.
There is one case in which provable extensionality is easy to show: If all occurrences of propositional variables in are outside boxes, then the fairness condition is a simple propositional tautology, and all such tautologies are provable in GL.
(Aside: One might wonder whether provable extensionality doesn't follow for all decision problems from the rule about substitution of equivalent formulas, but that's only an inference rule: if you can prove in GL that , and you can also prove , then it follows that you can prove , but GL does not in general prove . Here's a counterexample: Note that says "PA proves a contradiction", so says "PA is consistent". Hence, GL does not prove that , because that reduces to , which says "if PA is consistent, then PA proves its own consistency". That statement is false, and by soundness, GL only proves true things.)
Intuitively, given a -action, -level decision theory (where ), drnickbone's "evil" extensional decision problem works as follows: First, checks what would do on this same decision problem. Then it checks whether does the same thing. If so, the agent gets the second-best outcome; but if differs from 's action, the agent gets the best outcome.
To implement this idea, we first define a sequence , where stands for the action of the actual agent and stands for the action that would have taken, as follows:
- ; and
Now, we use the fixed point theorem to find a sequence such that for . Finally, we let . It's clear from the definition of that the formulas in are p.m.e.e., as required for a decision problem; and only occurs outside boxes in , so is provably extensional.
The point of this is that is now clearly the action of on the decision problem : is equivalent to , which is equivalent to , and is exactly the defining condition of " says what does on ". Therefore, now implements the intuitive definition of the evil problem: it checks whether takes the same action as ; if so, it returns the second-best outcome; otherwise, it returns the best.
So gets only the second best outcome, but the following decision theory gets the best one: