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.

Background

Here’s an example of how we usually talk about decision problems (Vladimir Slepnev’s formalization of Newcomb’s problem from “A model of UDT with a halting oracle”):

  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, $U ()$ , which makes calls to an agent program, $A ()$ .

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.

Definitions

Let’s say that a sequence of modal formulas $φ_{1}, \dots, φ_{n}$ are provably mutually exclusive and exhaustive, or p.m.e.e. for short, if $G L$ proves that exactly one of them is true: For example, $φ_{1}$ , $φ_{2}$ and $φ_{3}$ are p.m.e.e. if $G L ⊢ (φ_{1} \land \neg φ_{2} \land \neg φ_{3}) \lor (\neg φ_{1} \land φ_{2} \land \neg φ_{3}) \lor (\neg φ_{1} \land \neg φ_{2} \land φ_{3}) .$

We’ll say that a ( $k$ -outcome) modal universe is a sequence $O_{1}, \dots, O_{k}$ , or $\to O$ for short, of closed p.m.e.e. formulas, where $O_{i}$ is interpreted as the proposition that the $i$ ’th of the $k$ possible outcomes occurs.

Given a preference ranking on these $k$ possible outcomes, which has $n \leq k$ equivalence classes, we’ll write $U_{i}$ for the modal formula asserting that one of the outcomes in the $i$ ’th ranked equivalence class has occurred; for example, if the preference ordering is such that $O_{2}$ , $O_{5}$ and $O_{7}$ are the most preferred outcomes, then $U_{1} \equiv O_{2} \lor O_{5} \lor O_{7}$ . Clearly, $U_{1}, \dots, U_{n}$ (or $\to U$ for short) is a sequence of p.m.e.e. formulas; for brevity, we can avoid talking about $\to O$ , and call the sequence $\to U$ an $n$ -level universe.

(I’m using $\equiv$ to mean “same formula”.)

Similarly, an ( $m$ -action) modal agent is a sequence $A_{1}, \dots, A_{m}$ , or $\to A$ for short, of closed p.m.e.e. formulas, where $A_{i}$ is interpreted as saying that the agent takes its $i$ ’th available action.

A modal ( $m$ -action, $n$ -level) decision problem is an $n$ -level universe with a slot for an $m$ -action agent $\to A$ : that is, a p.m.e.e. sequence $P_{1} (\to a), \dots, P_{n} (\to a)$ , or $\to P (\to a)$ for short, where $\to a \equiv (a_{1}, \dots, a_{m})$ .

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 ( $m$ -action, $n$ -level) decision theory to be a p.m.e.e. sequence of fully modalized formulas $T_{1} (\to u), \dots, T_{m} (\to u)$ , or $\to T (\to u)$ for short, where $\to u = (u_{1}, \dots, u_{n})$ .

(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.)

Fixed points

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 $\to T (\to u)$ is fully modalized, so is— $\to T (\to P (\to a))$ if we substitute the $P_{i} (\to a)$ for $u_{i}$ , and all instances of $u_{i}$ were inside boxes, then all instances of $\to a$ in the resulting formula will be inside boxes as well. Thus, we can find a fixed point $\to A$ satisfying $G L ⊢ \to A \leftrightarrow \to T (\to P (\to A))$ (which I’m using as shorthand for stating that $G L ⊢ A_{i} \leftrightarrow T_{i} (\to P (\to A))$ holds for $i = 1, \dots, m$ ).

By the uniqueness theorem, for any $\to B$ satisfying $G L ⊢ \to B \leftrightarrow \to T (\to P (\to B))$ , we have $G L ⊢ \to A \leftrightarrow \to B$ , so our decision theory’s action is well-defined. Moreover, by the rule about substitution of equivalent formulas, it follows that $G L ⊢ \to P (\to A) \leftrightarrow \to P (\to B)$ , meaning that the preference level $\to U :\equiv \to P (\to A)$ that our decision theory achieves on this decision problem is well-defined as well.

Thus, for every pair of sequences $(\to T (\to u), \to P (\to a))$ , there’s a pair $(\to A, \to U)$ such that $G L ⊢ \to A \leftrightarrow T (\to U)$ and $G L ⊢ \to U \leftrightarrow P (\to A)$ ; 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 $(\to a \leftrightarrow \to b) \to (\to P (\to a) \leftrightarrow \to P (\to b)),$ where I’m writing $\to φ \leftrightarrow \to ψ$ for the conjunction of the $φ_{i} \leftrightarrow ψ_{i}$ . 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 $\to P (\to a)$ 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 $φ \leftrightarrow φ^{'}$ , and you can also prove $ψ (φ)$ , then it follows that you can prove $ψ (φ^{'})$ , but GL does not in general prove $(φ \leftrightarrow φ^{'}) \to (ψ (φ) \leftrightarrow ψ (φ^{'}))$ . Here’s a counterexample: Note that $□ ⊥$ says “PA proves a contradiction”, so $\neg □ ⊥$ says “PA is consistent”. Hence, GL does not prove that $(⊤ \leftrightarrow \neg □ ⊥) \to (□ ⊤ \leftrightarrow □ (\neg □ ⊥))$ , because that reduces to $\neg □ ⊥ \to □ \neg □ ⊥$ , which says “if PA is consistent, then PA proves its own consistency”. That statement is false, and by soundness, GL only proves true things.)

Evil problems

Intuitively, given a $m$ -action, $n$ -level decision theory $\to T (\to u)$ (where $m, n \geq 2$ ), drnickbone’s “evil” extensional decision problem $\to P (\to a)$ works as follows: First, $\to P (\to a)$ checks what $\to T (\to u)$ would do on this same decision problem. Then it checks whether $\to a$ does the same thing. If so, the agent gets the second-best outcome; but if $\to a$ differs from $\to T (\to u)$ ’s action, the agent gets the best outcome.

To implement this idea, we first define a sequence $F_{1} (\to a, \to b), \dots, F_{m} (\to a, \to b)$ , where $\to a$ stands for the action of the actual agent and $\to b \equiv (b_{1}, \dots, b_{m})$ stands for the action that $\to T (\to u)$ would have taken, as follows:

$F_{1} (\to a, \to b) :\equiv \neg (\to a \leftrightarrow \to b)$ ;
$F_{2} (\to a, \to b) :\equiv (\to a \leftrightarrow \to b)$ ; and
$F_{j + 2} (\to a, \to b) :\equiv ⊥$ .

Now, we use the fixed point theorem to find a sequence $\to B$ such that $G L ⊢ B_{i} \leftrightarrow T_{i} (\to F (\to B, \to B))$ for $i = 1, \dots, m$ . Finally, we let $\to P (\to a) :\equiv \to F (\to a, \to B)$ . It’s clear from the definition of $\to F (\to a, \to b)$ that the formulas in $\to P (\to a)$ are p.m.e.e., as required for a decision problem; and $\to a$ only occurs outside boxes in $\to P (\to a)$ , so $\to P (\to a)$ is provably extensional.

The point of this is that $\to B$ is now clearly the action of $\to T (\to u)$ on the decision problem $\to P (\to a)$ : $B_{i}$ is equivalent to $T_{i} (\to F (\to B, \to B))$ , which is equivalent to $T_{i} (\to P (\to B))$ , and $G L ⊢ \to B \leftrightarrow \to T (\to P (\to B))$ is exactly the defining condition of ” $\to B$ says what $\to T (\to u)$ does on $\to P (\to a)$ ”. Therefore, $\to P (\to a)$ now implements the intuitive definition of the evil problem: it checks whether $\to a$ takes the same action as $\to T (\to u)$ ; if so, it returns the second-best outcome; otherwise, it returns the best.

So $\to T (\to u)$ gets only the second best outcome, but the following decision theory ${\to T}^{'} (\to u)$ gets the best one:

$T_{1}^{'} (\to u) :\equiv \neg T_{1} (\to u)$ ;
$T_{2}^{'} (\to u) :\equiv T_{1} (\to u)$ ;
$T_{j + 2}^{'} (\to u) :\equiv ⊥$ .

“Evil” decision problems in provability logic

Background

Definitions

Fixed points

Extensional (= “fair”) decision problems

Evil problems