Summary: we might expect $PA+m$ to be able to predict the behavior of an escalating modal UDT agent using $PA+n$ for $n<m$. However, this is not the case. Furthermore, in environments where $PA+m$ predicts the agent, escalating modal UDT can be outperformed by a constant agent.

For a given logic $X$, we can define $X+1=X+\text{Con}\left(X\right)$ (i.e. $X+1$ has all the axioms of $X$ plus the axiom that $X$ is consistent). We can iteratively get $X+2=(X+1)+1$ and so on.

Now consider $PA+100$. In some sense, it is "more powerful" than PA: it contains additional correct axioms. Therefore, we might find it plausible that $PA+100$ can always correctly predict the behavior of a modal UDT agent using PA.

Ordinary modal UDT can run into issues on some environments due to later stages not be able to use the assumption that logics used in previous stages are consistent. Therefore, define escalating modal UDT to be the same as modal UDT except that the $n$th proof search uses $PA+n$ instead of $PA$. Benja might write a post explaining this system better.

Let $m$ be a number higher than the number of proof searches escalating modal UDT makes. Patrick made the conjecture that if $U$ is a simple function of $A\left(\right)$ (the agent's output) and $PA+m⊢A\left(\right)=a$ (for each action $a$, whether the predictor predicts the agent takes action $a$), where $A\left(\right)$ is escalating modal UDT, then:

1. The predictor is correct (if $A\left(\right)=a$ then $PA+m⊢A\left(\right)=a$)
2. The agent picks the best action conditioned on the predictor being correct (i.e. the action $a$ that maximizes utility when $A\left(\right)=a$ and $PA+m⊢A\left(\right)=a$)

Both parts of the conjecture turn out to be false. First, consider the following environment:

def U():

if $A\left(\right)=\alpha$

if $PA+100⊢A\left(\right)=\beta$

return 10

else

return 0

else

return 5

• First, the agent will determine $PA⊢A\left(\right)=\alpha \to U\left(\right)=10$. For this to be the case $PA$ would have to prove ${\square }_{PA+100}┌A\left(\right)=\beta ┐$. But if $PA$ proves this, then in fact $A\left(\right)=\alpha$, so this would require $PA+100$ to be unsound. Therefore this proof search fails.
• Next, the agent will determine $PA+1⊢A\left(\right)=\beta \to U\left(\right)=10$. This obviously fails.
• Next, the agent will determine $PA+2⊢A\left(\right)=\alpha \to U\left(\right)=5$. This obviously fails.
• Next, the agent will determine $PA+3⊢A\left(\right)=\beta \to U\left(\right)=5$. This obviously succeeds, and the agent takes action $\beta$.

Now consider whether $PA+100⊢A\left(\right)=\beta$. Consider a model $M$ of $PA+100$ in which $$M\models PA+100$$ $$M\models \neg \text{Con}(PA+100)$$

Now: $$M\models {\square }_{PA}┌\neg \text{Con}(PA+100)┐$$ $$M\models {\square }_{PA}┌{\square }_{PA+100}┌A\left(\right)=\beta ┌┐$$ $$M\models {\square }_{PA}┌A\left(\right)=\alpha \to U\left(\right)=10┐$$ $$M\models A\left(\right)=\alpha$$

Since $M\models PA+100$, we have $PA+100⊬A\left(\right)=\beta$. This disproves the first part of the conjecture.

For the second part, consider the following environment:

def U():

if $A\left(\right)=\alpha$

if $PA+100⊢A\left(\right)=\beta$

 return 0

else

 return 10

else

return 5

• First, the agent will determine $PA⊢A\left(\right)=\alpha \to U\left(\right)=10$. This is equivalent to $PA⊢\neg {\square }_{PA+100}┌A\left(\right)=\beta ┐$. But $PA$ cannot prove $PA+100$ consistent, so $PA$ fails to prove this.
• Next, the agent will determine $PA+1⊢A\left(\right)=\beta \to U\left(\right)=10$. This obviously fails.
• Next, the agent will determine $PA+2⊢A\left(\right)=\alpha \to U\left(\right)=5$. This obviously fails.
• Next, the agent will determine $PA+3⊢A\left(\right)=\beta \to U\left(\right)=5$. This obviously succeeds, and the agent takes action $\beta$.

So, part 2 of the conjecture is false. Escalating modal UDT is outperformed by the agent that always takes action $\alpha$.

To create predictors that can always predict modal UDT, we may consider having the predictor using $PA+{\Pi }_1$ (i.e. PA plus all true ${\Pi }_1$ statements, where ${\Pi }_1$ is part of the arithmetic hierarchy).