Obstacle to modal optimality when you're being modalized

post by orthonormal · 2015-08-29T20:41:59.000Z · LW · GW · 0 comments

Contents

No comments

Summary: The optimality result for modal UDT on provably extensional problems doesn't carry over even to very straightforward problems where the agent's action is "predicted" (in the sense that a modalized $A$ is used) rather than just "run" (in the sense that a nonmodalized $A$ is used). In fact, there's a pair of such problems on which no modal decision theory can be simultaneously optimal.

Prerequisites: "Evil" decision problems in provability logic, An optimality result for modal UDT, Improving the modal UDT optimality result

Benja's modal UDT optimality results (especially the fact that $\neg {\square }^n\perp$ is the only axiom schema you'll ever need) are really nifty, but they correspond to exactly the games we might think of as "truly one-player". The agent $A\left(\right)$ depends on the universe $U\left(\right)$ only by proving things about it (all instances of $U\left(\right)$ within $A\left(\right)$ are modalized, by the definition of a modal agent), while the universe depends on the agent only by running it (all instances of $A\left(\right)$ within $U\left(\right)$ are nonmodalized, by the definition of provably extensional).

So in particular, if we want to consider multi-agent problems (or other non-extensional problems), the modal UDT algorithm continues to be perfectly well-defined, but the optimality result no longer has a valid proof. But could something like that result continue to hold?

OK, fine, you've read the summary, so you know that the answer is "no" in the following sense: I can show you two such universes, such that any modal agent fails in at least one case to achieve the best outcome that any modal agent can on that problem.

Let the possible actions in both universes be denoted by $a$ and $\neg a$, and the possible outcomes be denoted by $g$ and $\neg g$. Let's say that $g$ is good and $\neg g$ is bad.

Universe 1 is defined by $\left(U_1\right()=g)\leftrightarrow \square \left(A\right()=a)$ (and similarly, $\left(U_1\right()=\neg g)\leftrightarrow \neg \square \left(A\right()=a)$).

Universe 2 is defined by $\left(U_2\right()=g)\leftrightarrow \square \left(A\right()=\neg a)$ (and similarly, $\left(U_2\right()=\neg g)\leftrightarrow \neg \square \left(A\right()=\neg a)$).

I claim that no modal decision theory (as defined in the "evil" decision problem post) can get the outcome $g$ in both universes, but of course for each universe there exists a modal decision theory that gets the outcome $g$. (The constant strategies are modal decision theories.) Let $\overrightarrow{T}$ be a modal decision theory.

Lemma: $\square \perp \to \left(\overrightarrow{T}\right(U_1)=a\leftrightarrow \overrightarrow{T}(U_2)=a)$.

Given the lemma, we see that $\left(\overrightarrow{T}\right(U_1)=a\wedge \neg \overrightarrow{T}(U_2)=a)\to \neg \square \perp$, so $\square \left(\overrightarrow{T}\right(U_1)=a\wedge \neg \overrightarrow{T}(U_2)=a)\to \square \neg \square \perp$, and as in Gödel's second incompleteness theorem, $\square \neg \square \perp \to \square \perp$. Thus $\neg \square \perp \to \neg \left(\square \overrightarrow{T}\right(U_1)=a\wedge \square \neg \overrightarrow{T}(U_2)=a)$, and by definition of the universes, $\neg \square \perp \to \neg \left(U_1\right(\overrightarrow{T})=g\wedge U_2(\overrightarrow{T})=g)$. Since we're evaluating fixed points in the standard model of the natural numbers, this completes the proof.

Now why should the lemma hold? Because $\overrightarrow{T}$ is modalized, and so $\square \perp$ implies that all subexpressions $\square A$ of $\overrightarrow{T}$ evaluate to true, and this uniquely determines the value of $\overrightarrow{T}$ given $\square \perp$, regardless of its input.

Thus we can't expect much in the way of optimality in non-extensional problems. (This in addition to several other obstacles to optimality in the special case of modal combat, to which this example also belongs.)

P.S. Thanks to Marcello Herreshoff for working this example out with me, and Benja Fallenstein for looking it over (though Benja wishes to register their disapproval for my notation, in which I've used nonmodal expressions like $U_1\left(\right)=g$ and $T\left(U_2\right)=a$ to stand in for the fixed points of the theory).

P.P.S. I'm not happy calling this "modal UDT", because here we're showing that it doesn't succeed at doing what our philosophical intuitions about updateless decision theory ought to do. But the name is getting increasingly entrenched for both of these contexts...

0 comments

Comments sorted by top scores.