I recently posted about an optimality result for modal UDT, which shows that for every modal decision problem $\overrightarrow{P}\left(\overrightarrow{a}\right)$, there is a closed modal formula $\phi$ such that the version of modal UDT that searches for proofs in $PA+\phi$ will perform optimally on $\overrightarrow{P}\left(\overrightarrow{a}\right)$.

Paul commented on this post and suggested a stronger version: For every modal decision theory $\overrightarrow{T}\left(\overrightarrow{u}\right)$ and every provably extensional modal decision problem $\overrightarrow{P}\left(\overrightarrow{a}\right)$, modal UDT will do at least as well on $\overrightarrow{P}\left(\overrightarrow{a}\right)$ as $\overrightarrow{T}\left(\overrightarrow{u}\right)$ does if it is using a proof system that can prove what action $\overrightarrow{T}\left(\overrightarrow{u}\right)$ chooses on this decision problem, and which outcome it obtains as a result. In this post, I give a detailed proof of this.

Prerequisite: An optimality result for modal UDT, and the prerequisites therein.

Let $({\overrightarrow{A}}^{\left(T\right)},{\overrightarrow{U}}^{\left(T\right)})$ be the fixed point of $\overrightarrow{T}\left(\overrightarrow{u}\right)$ and $\overrightarrow{P}\left(\overrightarrow{a}\right)$, and recall my notation ${\overrightarrow{\chi }}^{\left(i\right)}$ for the sequence of formulas which has $\top$ as the $i$'th entry, and $\perp$ as all of its other entries (with the length of the sequence being clear from context). Now suppose that $\phi$ is a true closed formula in the language of $GL$ such that $$GL⊢\phi \to (({\overrightarrow{A}}^{\left(T\right)}\leftrightarrow {\overrightarrow{\chi }}^{\left(i_T^{\ast }\right)})\wedge ({\overrightarrow{U}}^{\left(T\right)}\leftrightarrow {\overrightarrow{\chi }}^{\left(j_T^{\ast }\right)}));$$ that is, $GL+\phi$ proves that $\overrightarrow{T}\left(\overrightarrow{u}\right)$ chooses action $i_T^{\ast }$, and achieves the outcome $j_T^{\ast }$ as a result. (By saying that $\phi$ is a "true" formula we mean that its translation to the language of arithmetic is true about the standard natural numbers: $N\models \phi$.) It's ok to talk about ${\overrightarrow{A}}^{\left(T\right)}$ and ${\overrightarrow{U}}^{\left(T\right)}$ in the definition of $i_T^{\ast }$ and $j_T^{\ast }$ because fixed points are unique (up to provable equivalence), and $GL$ can prove that the fixed point is in fact a fixed point.

My claim, then, is that ${\overrightarrow{UDT}}^{\left(\phi \right)}\left(\overrightarrow{u}\right)$ will perform at least as well as $\overrightarrow{T}\left(\overrightarrow{u}\right)$ on the decision problem $\overrightarrow{P}\left(\overrightarrow{a}\right)$; that is, the outcome it achieves will be ranked $\le j_T^{\ast }$.

Intuitively, this is straight-forward. $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ searches through all pairs $(j,i)$ of outcomes and actions in lexicographical order, until it finds a pair such that it can prove that if it takes action $i$, it will achieve outcome $j$; as soon as it finds such a pair, it takes action $i$. (This is justified becaues it searches outcomes best-first, so it takes an action that leads to as good an outcome as it's able to prove it can get.) So if it can prove that taking action $i_T^{\ast }$ will lead to outcome $j_T^{\ast }$, it will either take that action and get that outcome, or there's some pair $(j,i)<(j_T^{\ast },i_T^{\ast })$ such that it takes action $i$ and obtains outcome $j\le j_T^{\ast }$. (Remember that outcomes are numbered from best to worst.)

Let's go through the details of showing that it actually works out that way.

Let's write $(\overrightarrow{A},\overrightarrow{U})$ for the fixed point of $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{u}\right)$ with $\overrightarrow{P}\left(\overrightarrow{a}\right)$. The part in our argument that we need to check carefully is that UDT will in fact stop at the pair $(j_T^{\ast },i_T^{\ast })$ if it hasn't already stopped before that; i.e., $$GL⊢\phi \to ({UDT}_{i_T^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j_T^{\ast }}).$$ If this is satisfied, then we're done: We know that there will be some pair $(j^{\ast },i^{\ast })\le (j_T^{\ast },i_T^{\ast })$ such that $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{U}\right)$ outputs $i^{\ast }$ and such that $$GL⊢\phi \to ({UDT}_{i^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j^{\ast }}),$$ and hence, since (a) $GL$ is sound on $N$, (b) $N\models \phi$, and (c) by assumption, $N\models {UDT}_{i^{\ast }}^{\left(\phi \right)}$, it follows that $N\models U_{j^{\ast }}$, i.e., ${UDT}^{\left(\phi \right)}\left(\overrightarrow{U}\right)$ achieves the outcome $j^{\ast }\le j_T^{\ast }$. Thus, let's check that $GL$ does indeed prove $\phi \to \left({UDT}_{i_T^{\ast }}^{\left(\phi \right)}\right(\overrightarrow{U})\to U_{j_T^{\ast }})$.

To do so, we make use of provable extensionality, that is, of the fact that $$GL⊢(\overrightarrow{a}\leftrightarrow \overrightarrow{b})\to (\overrightarrow{P}\left(\overrightarrow{a}\right)\leftrightarrow \overrightarrow{P}\left(\overrightarrow{b}\right)).$$ Since as a modal decision theory, $\overrightarrow{{UDT}^{\left(\phi \right)}}$ is a p.m.e.e. sequence (provably mutually exclusive and exhaustive), $GL$ proves that ${UDT}_{i_T^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)$ implies $\overrightarrow{{UDT}^{\left(\phi \right)}}\left(\overrightarrow{U}\right)\leftrightarrow {\overrightarrow{\chi }}^{\left(i_T^{\ast }\right)}$, i.e., $\overrightarrow{A}\leftrightarrow {\overrightarrow{\chi }}^{\left(i_T^{\ast }\right)}$. Hence, together with provable extensionality, we obtain $$GL⊢{UDT}_{i_T^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to (\overrightarrow{U}\leftrightarrow \overrightarrow{P}\left({\chi }^{\left(i_T^{\ast }\right)}\right))$$ (since $GL⊢\overrightarrow{P}\left(\overrightarrow{A}\right)\leftrightarrow \overrightarrow{U}$ by definition of $\overrightarrow{U}$). But on the other hand, recall our initial assumption that $$GL⊢\phi \to (({\overrightarrow{A}}^{\left(T\right)}\leftrightarrow {\overrightarrow{\chi }}^{\left(i_T^{\ast }\right)})\wedge ({\overrightarrow{U}}^{\left(T\right)}\leftrightarrow {\overrightarrow{\chi }}^{\left(j_T^{\ast }\right)}));$$ again by provable extensionality, this implies $$GL⊢\phi \to ((\overrightarrow{P}\left({\overrightarrow{A}}^{\left(T\right)}\right)\leftrightarrow \overrightarrow{P}\left({\overrightarrow{\chi }}^{\left(i_T^{\ast }\right)}\right))\wedge ({\overrightarrow{U}}^{\left(T\right)}\leftrightarrow {\overrightarrow{\chi }}^{\left(j_T^{\ast }\right)})),$$ and since $GL⊢\overrightarrow{P}\left({\overrightarrow{A}}^{\left(T\right)}\right)\leftrightarrow {\overrightarrow{U}}^{\left(T\right)}$ by definition of ${\overrightarrow{U}}^{\left(T\right)}$, this simplifies to $$GL⊢\phi \to (P\left({\overrightarrow{\chi }}^{\left(i_T^{\ast }\right)}\right)\leftrightarrow {\overrightarrow{\chi }}^{\left(j_T^{\ast }\right)}).$$ But together with our earlier result, this implies $$GL⊢(\phi \wedge {UDT}_{i_T^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right))\to (\overrightarrow{U}\leftrightarrow {\overrightarrow{\chi }}^{\left(j_T^{\ast }\right)}),$$ which is equivalent to $$GL⊢\phi \to ({UDT}_{i_T^{\ast }}^{\left(\phi \right)}\left(\overrightarrow{U}\right)\to U_{j_T^{\ast }}),$$ as desired.