Yesterday, I gave a definition of "decision theory" and "fair decision problem" in the context of provability logic, and gave a formal version of drnickbone's argument that no decision theory can perform optimally on every "fair" decision problem. Today, I prove that for any provably "fair" decision problem $\overrightarrow{P}\left(\overrightarrow{u}\right)$, there is a sound extension of $PA$ by a finite set of formulas, expressible in the language of provability logic, such that Vladimir Slepnev's modal logic version of UDT performs optimally on $\overrightarrow{P}\left(\overrightarrow{u}\right)$ if we have it search for proofs in this extended proof system.

This is a version of a result that Kenny Easwaran, Nate Soares and I proved in the context of UDT with bounded proof length when Kenny visited MIRI for two days earlier this year. (I'll post about the bounded proof length version some other time; it's more complicated, as you'd expect.)

Prerequisites: A primer on provability logic, "Evil" decision problems in provability logic.

Provability in extensions of PA

In order to carry out the idea above, we need to talk about provability in extensions of $PA$, not just about the provability in $PA$ expressed by the $\square (\cdot )$ operator of Gödel-Löb provability logic. Fortunately, the systems we'll need in this post only extend $PA$ by a finite number of axioms which can be expressed as closed formulas in the language of $GL$, and there's a simple trick to reason about such extensions in $GL$ itself:

Suppose that we extend $PA$ by a single axiom, $\phi$. Then, by the deduction theorem for first-order logic, $PA+\phi ⊢\psi$ if and only if $PA⊢\phi \to \psi$. Thus, if both $\phi$ and $\psi$ can be expressed as modal formulas, then we can express the proposition that $\psi$ is provable in $PA+\phi$ by the modal formula $\square (\phi \to \psi )$. The same trick works, of course, if we want to add finitely many different modal formulas to $PA$, since we can simply let $\phi$ be their conjunction.

In this post, when I'm using this trick to talk about $PA+\phi$, I'll emphasize this fact by abbreviating $\square (\phi \to \psi )$ to ${\square }_{\phi }\left(\psi \right)$ (since we often subscript $\square$ by the proof system when it's not clear which system we are referring to).

Modal UDT

The version of modal UDT I'm using in this article is equivalent to the one in Vladimir's article, except for using ${\square }_{\phi }(\cdot )$ instead of $\square (\cdot )$, for an appropriate $\phi$. Nevertheless, let me give a quick recap, which puts a slightly different spin on the system, and check that this does indeed meet the specification of a "modal decision theory".

As a modal decision theory, $m$-action, $n$-preference level modal UDT is a sequence $\overrightarrow{UDT}\left(\overrightarrow{u}\right)$ of $m$ formulas in $n$ parameters, such that ${UDT}_i\left(\overrightarrow{U}\right)$ gives the action UDT chooses in the modal universe $\overrightarrow{U}$. Let's write $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ for the version which uses provability in $PA+\phi$.

I think the easiest way to specify $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ is to say that it's a sequence of modal formulas which describe the behavior of the following an algorithm (which needs a halting oracle):

• For each $j=1,\dots ,n$:
  • For each $i=1,\dots ,m$:
    • If it's provable in $PA+\phi$ that "I take action $i$" implies "I obtain outcome $j$", then return $i$.
• If still here, return $1$.

In other words, UDT starts with the most preferred outcome, and tries to find an action that provably implies that outcome; if there is such an action, it returns it, breaking ties lexicographically. If there isn't, it tries the second-most-preferred outcome, and so on down to the least preferred one. If no actions imply any outcomes, it returns an arbitrary default action.

To actually write out ${UDT}_i^{\left(\phi \right)}$, we need to find a formula that describes when the above algorithm returns the action $i$. Clearly, for actions other than the default action, the condition is that there's some outcome $j$ such that (a) it's provable that $i$ implies $j$; (b) there's no action $i^{\prime }<i$ which provably implies $j$; (c) and there isn't any outcome $j^{\prime }<j$ which is provably implied by any action $i^{\prime }$. The default action $1$ is taken if the condition above holds or if no action provably implies any outcome.

Let's agree to order pairs $(j,i)$ lexicographically, i.e., $(j,i)<(j^{\prime },i^{\prime })$ if $j<j^{\prime }$ or $j=j^{\prime }$ and $i<i^{\prime }$. Then, we can write ${UDT}_i^{\left(\phi \right)}\left(\overrightarrow{u}\right)$ as follows, for $i>1$: $${UDT}_i^{\left(\phi \right)}\left(\overrightarrow{u}\right):\equiv \underset{j=1}{\overset{n}{\bigvee }}\left({\square }_{\phi }({UDT}_i^{\left(\phi \right)}\right(\overrightarrow{u})\to u_j)\wedge \underset{(j^{\prime },i^{\prime })<(j,i)}{\bigwedge }\neg {\square }_{\phi }({UDT}_{i^{\prime }}^{\left(\phi \right)}(\overrightarrow{u})\to u_{j^{\prime }})),$$ and for $i=1$: $$\begin{array}{cc}{UDT}_1^{\left(\phi \right)}\left(\overrightarrow{u}\right)& :\equiv \underset{j=1}{\overset{n}{\bigvee }}\left({\square }_{\phi }({UDT}_1^{\left(\phi \right)}\right(\overrightarrow{u})\to u_j)\wedge \underset{(j^{\prime },i^{\prime })<(j,1)}{\bigwedge }\neg {\square }_{\phi }({UDT}_{i^{\prime }}^{\left(\phi \right)}(\overrightarrow{u})\to u_{j^{\prime }}))\\ & \vee \underset{(j^{\prime },i^{\prime })=(1,1)}{\overset{(m,n)}{\bigwedge }}\neg {\square }_{\phi }({UDT}_{i^{\prime }}^{\left(\phi \right)}\left(\overrightarrow{u}\right)\to u_{j^{\prime }}).\end{array}$$ From this definition, it's straight-forward to see that $\overrightarrow{{UDT}^{\left(\phi \right)}}$ is provably mutually exclusive and exhaustive (p.m.e.e.); we work in $GL$ and distinguish the following cases: There either is no pair $(j,i)$ such that $\square ({UDT}_i^{\left(\phi \right)}\left(\overrightarrow{u}\right)\to u_j)$, or some pair $(j,i)$ is the first one. If there is no such pair, then ${UDT}_1^{\left(\phi \right)}\left(\overrightarrow{u}\right)$ is true, and all other formulas in the sequence are false. If $(j,i)$ is the first such pair, then ${UDT}_i^{\left(\phi \right)}\left(\overrightarrow{u}\right)$ is true, and all the other formulas are false.

Provably extensional problems

Let's call a closed formula in the language of $GL$ sound if its translation into the language of arithmetic is true on the natural numbers; unsurprisingly, we'll write this as $N\models \phi$ for short. My claim is that for every provably extensional decision problem $\overrightarrow{P}\left(\overrightarrow{a}\right)$, there is a sound formula $\phi$ such that $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ performs optimally on $\overrightarrow{P}\left(\overrightarrow{a}\right)$, that is, obtains the best outcome that any decision theory can achieve on this outcome.

Recall that a decision problem $\overrightarrow{P}\left(\overrightarrow{a}\right)$ is defined to be provably extensional if $$GL⊢(\overrightarrow{a}\leftrightarrow \overrightarrow{b})\to (\overrightarrow{P}\left(\overrightarrow{a}\right)\leftrightarrow \overrightarrow{P}\left(\overrightarrow{b}\right)),$$ where $\overrightarrow{\phi }\leftrightarrow \overrightarrow{\psi }$ stands for the conjunction $({\phi }_1\leftrightarrow {\psi }_1)\wedge \cdots \wedge ({\phi }_n\leftrightarrow {\psi }_n)$. (Of course, the two sequences need to be of the same length.)

Intuitively, such a decision problem assigns a single outcome $f\left(i\right)$ to every action $i$, and every agent which chooses action $i$ will obtain outcome $f\left(i\right)$; this is a formalization of the idea that we should consider a decision problem "fair" if it only rewards or punishes you for the actions you decide to take, not for the decision process you used to arrive at these decisions.

This doesn't mean that the mapping $f\left(i\right)$ is all that matters about the decision problem---for example, any particular version of modal UDT fails on its "evil" decision problem, despite the fact that these "evil" problems are provably extensional. That's because it can be difficult to determine which mapping $f(\cdot )$ a particular $\overrightarrow{P}\left(\overrightarrow{a}\right)$ corresponds to.

The idea of the optimality proof in this post is that for any particular $\overrightarrow{P}\left(\overrightarrow{u}\right)$, there is some truth about what the corresponding mapping $f(\cdot )$ is, even if it's hard to determine, and if we run UDT with a proof system strong enough to handle this problem, this version of UDT will simply be able to figure out which action is best and then take it.

How do we find a proof system strong enough to determine the action/outcome mapping $f(\cdot )$ for a given $\overrightarrow{P}\left(\overrightarrow{a}\right)$? The simplest possibility is to just take $PA$ and add to it the information about the true action/outcome mapping.

Let ${\chi }_i^{\left(i\right)}:\equiv \top$ and ${\chi }_{i^{\prime }}^{\left(i\right)}:\equiv \perp$ for $i^{\prime }\ne i$, and write ${\overrightarrow{\chi }}^{\left(i\right)}$ for the corresponding sequence of length $m$ or $n$ (depending on the context). By the true mapping, I mean the mapping $f(\cdot )$ such that for all $i\in \{1,\dots ,m\}$, we have $N\models P_{f\left(i\right)}\left({\overrightarrow{\chi }}^{\left(i\right)}\right)$. This mapping is unique, because $\overrightarrow{P}\left(\overrightarrow{a}\right)$ is a decision problem, which by definition implies that the formulas in this sequence are p.m.e.e. (i.e., exactly one of them is true, for any particular value of the $\overrightarrow{a}$).

Now it's clear how we can encode the fact that this is the true mapping as a formula of $GL$: we simply set $\phi :\equiv {\bigwedge }_{i=1}^n{P}_{f\left(i\right)}\left({\overrightarrow{\chi }}^{\left(i\right)}\right)$.

Optimality

It's now clear the best outcome any agent can obtain on the provably extensional decision problem $\overrightarrow{P}\left(\overrightarrow{a}\right)$ is ${min}_{i}f\left(i\right)$: An agent $\overrightarrow{A}$ is a sequence of closed p.m.e.e. formulas, which means that for any agent $\overrightarrow{A}$ there is some $i$ such that $N\models \overrightarrow{A}\leftrightarrow {\overrightarrow{\chi }}^{\left(i\right)}$, which by extensionality implies $N\models \overrightarrow{P}\left(\overrightarrow{A}\right)\leftrightarrow \overrightarrow{P}\left({\overrightarrow{\chi }}^{\left(i\right)}\right)$, so the outcome obtained by $\overrightarrow{A}$ is $f\left(i\right)$.

Write $(\overrightarrow{A},\overrightarrow{U})$ for the fixed point of $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ and $\overrightarrow{P}\left(\overrightarrow{a}\right)$, with $\phi$ defined as in the previous section. Then, in order to show that $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ performs optimally on this decision problem, we need to show that $N\models \overrightarrow{A}\leftrightarrow {\overrightarrow{\chi }}^{\left(i^{\ast }\right)}$ for some $i^{\ast }$ such that $f\left(i^{\ast }\right)=j^{\ast }:={min}_{i}f\left(i\right)$.

I claim that this holds for $i^{\ast }$ the smallest $i$ such that $f\left(i\right)=j^{\ast }$. Given the way $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ is constructed, in order to show this I need to show that $N\models {\square }_{\phi }({UDT}_{i^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j^{\ast }})$, plus $N\models \neg {\square }_{\phi }({UDT}_{i^{\prime }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j^{\prime }})$ for all $(j^{\prime },i^{\prime })<(j^{\ast },i^{\ast })$.

The first of these statements is equivalent to $$GL⊢\phi \to ({UDT}_{i^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j^{\ast }}),$$ which, given the properties $GL⊢\overrightarrow{A}\leftrightarrow \overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{U}\right)$ and $GL⊢\overrightarrow{U}\leftrightarrow \overrightarrow{P}\left(\overrightarrow{A}\right)$ defining $\overrightarrow{A}$ and $\overrightarrow{U}$, we can rewrite as $$GL⊢\phi \to (A_{i^{\ast }}\to P_{j^{\ast }}\left(\overrightarrow{A}\right)).$$ Since $\overrightarrow{A}$ is p.m.e.e., $A_{i^{\ast }}$ is equivalent to $\overrightarrow{A}\leftrightarrow {\chi }^{\left(i^{\ast }\right)}$, so by provable extensionality of $\overrightarrow{P}\left(\overrightarrow{a}\right)$, we have $GL⊢A_{i^{\ast }}\to (\overrightarrow{P}\left(\overrightarrow{A}\right)\leftrightarrow \overrightarrow{P}\left({\overrightarrow{\chi }}^{\left(i^{\ast }\right)}\right))$. The definition of $\phi$ implies $GL⊢\phi \to (\overrightarrow{P}({\overrightarrow{\chi }}^{\left(i^{\ast }\right)}\leftrightarrow {\overrightarrow{\chi }}^{\left(j^{\ast }\right)})$, so we obtain $GL⊢(\phi \wedge A_{i^{\ast }})\to (\overrightarrow{P}\left(\overrightarrow{A}\right)\leftrightarrow {\overrightarrow{\chi }}^{\left(j^{\ast }\right)})$ or $GL⊢(\phi \wedge A_{i^{\ast }})\to P_{j^{\ast }}\left(\overrightarrow{A}\right)$, which is equivalent to the desired result.

For the second statement, we need to show that ${UDT}_{i^{\prime }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j^{\prime }}$ is not provable in $PA+\phi$ for any $(j^{\prime },i^{\prime })<(j^{\ast },i^{\ast })$. So suppose it were provable, for some such $(j^{\prime },i^{\prime })$. Then $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{U}\right)$ would take the action $i^{\prime }$ corresponding to the smallest such pair; in other words, we would have $N\models {UDT}_{i^{\prime }}^{\left(\phi \right)}$. We can again use the defining properties of $\overrightarrow{A}$ and $\overrightarrow{U}$ to rewrite this as $N\models A_{i^{\prime }}$.

Since $PA$ is sound and $N\models \phi$, the assumption that ${UDT}_{i^{\prime }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j^{\prime }}$ is provable in $PA+\phi$ implies that it is true on $N$. We can rewrite this as well, to $N\models A_{i^{\prime }}\to P_{j^{\prime }}\left(\overrightarrow{A}\right)$. Hence, we have $N\models A_{i^{\prime }}\wedge P_{j^{\prime }}\left(\overrightarrow{A}\right)$.

If $j^{\prime }<j^{\ast }$, this says that $\overrightarrow{A}$ achieves an outcome better than $j^{\ast }$, which we've shown above to be the best outcome that any agent can possibly achieve---contradiction. If $j^{\prime }=j^{\ast }$ and $i^{\prime }<i^{\ast }$, then we have found an $i^{\prime }<i^{\ast }$ such that $f\left(i^{\prime }\right)=j^{\ast }$ (since by extensionality, $N\models A_{i^{\prime }}$ implies $N\models P_{f\left(i^{\prime }\right)}\left(\overrightarrow{A}\right)$, and hence $N\models \neg P_{j^{\prime }}\left(\overrightarrow{A}\right)$ for $j^{\prime }\ne f\left(i^{\prime }\right)$ as $\overrightarrow{P}\left(\overrightarrow{a}\right)$ is p.m.e.e.)---contradiction to the definition of $i^{\ast }$.