Prerequisites: Provability logic, Updateless decision theory

Outline

• Introduction
• Formal setting
• Main claim describing halting agent behavior
• Example
• Proof of main claim
• Corollary on uniqueness of UDT
• Discussion of assumptions

Introduction

(This post was going to be a description of my paper UDT with known search order, but instead it obsoletes that paper.)

Consider the following argument that UDT is the unique decision procedure that performs optimally in simple universes.

Suppose an agent $A$, with a provability oracle for statements like "if $A$ does action $a$, then utility $u$ results," doesn't play chicken for some possible action $a$. In other words, the agent is not committed to taking action $a$ whenever it sees that $A$ provably does not take action $a$. Then this fact would be visible to $\text{PA}$; using Lob's theorem, we could prove that $A$ actually does not take action $a$. This argument looks like it is independent of the universe, so in some simple universes where action $a$ would give a large reward, $A$ actually fails to take $a$. Therefore optimal agents must diagonalize against actions that they provably don't take.

This post will carry through a precise version of this argument. First we'll analyze exactly how agents behave when they only have to worry about finitely many possible outcomes. Then we'll apply this to the case where there are unboundedly many possible outcomes.

The busy reader could read just the description of the formal setting, and then skip to the corollary towards the end. The only crucial thing for the statement of the corollary is the notion of an agent that halts for every "possible" consequences oracle. However, the analysis in the main claim gives more information; namely, it says how to compute the behavior of any halting agent in any universe, as long as that universe is transparent in a sense to be defined later.

---

Formal setting

A universe $U\left[A\right]$ is any algorithm that outputs a utility in the set $U\subset N$. A universe is parameterized by the choice of an agent $A$, and it may make calls to some level of halting oracle to compute what $A$ does. The set $U$ of possible utilities may be infinite, and we assume that our preference ordering on $U$ is the ordering $<$ on $N$. An agent is an algorithm $A\left[U\right]$ (usually written $A$) that selects some action from the finite set $A$. The universe can observe the behavior of $A$, but the agent only gains information about $U$ through its oracle, which depends on $U$.

The agent $A$ makes calls to a consequences oracle $C : A \times U \to {0,1} $, which is always implicitly dependent on $A$ and $U$. We'll work in $\text{PA}$, which can talk about $U\left[A\right]$ and $A\left[U\right]$ via quining. So, the oracle call $C(a,u)$ returns 1 if $\text{PA}⊢A\left[U\right]=a\to U\left[A\right]=u$, and $C(a,u)$ returns 0 otherwise.

We make a transparency assumption on the universe: $$\forall a\in A\exists u\in U:\text{PA}⊢A\left[U\right]=a\to U\left[A\right]=u.$$ This is a strong assumption, but we are trying to prove that UDT is \emph{required} for optimal behavior in simple universes. We could just as well assume that the universe is a simple map $A\to U$, i.e. $U$ simply checks the action of $A$ and then looks up a corresponding utility in a table. The transparency assumption above is all we need to analyze the behavior of our agents, but we will see that UDT is necessary for optimal behavior even in the simple universes.

For each action $a$, if $C(a,u_1)=C(a,u_2)=1$ for some $u_1\ne u_2$, then $\text{PA}⊢A\ne a$, and in fact $C(a,u)=1$ for all $u\in U$. By the transparency of $U$, for each $a\in A$ we have either $C(a,u)=1$ for all $u\in U$, or else $C(a,u)=1$ for exactly one $u$. So, we define a consequence profile for $A,U$ to be any map $\gamma :A\to U\cup \left\{\perp \right\}$ such that $$\forall a\in A,u\in U:\gamma \left(a\right)=u\Rightarrow C(a,u)=1.$$ The interpretation of $\gamma \left(a\right)=u$ is that $C(a,u)=1$ for $u$ only, and the interpretation of $\gamma \left(a\right)=\perp$ is that $C(a,u)=1$ for all $u\in U$; consequence profiles encode all the information that $C$ might contain. We say that a consequence profile $\gamma$ describes an oracle $C$ if for all $a\in A$, $\gamma \left(a\right)=u\Rightarrow$ ($C(a,u)=1$ for only $u$), and $\gamma \left(a\right)=\perp \Rightarrow$ ($C(a,u)=1$ for all $u$).

A consequence profile is full if $\perp$ is not in its range, i.e. it gives an actual utility for each action. Two consequence profiles $\gamma$ and $\delta$ agree if there is no $a\in A$ such that $\perp \ne \gamma \left(a\right)\ne \delta \left(a\right)\ne \perp$; in other words, they agree if they assign the same utility to an action whenever they both assign an actual utility to that action, rather than assigning $\perp$. Given $A$ and $U$, the transparency assumption lets us pick a (possibly non-unique) full consequence profile, which we will denote by $\sigma$.

We require that $U\left[A\right]$ halts as long as $A$ halts. We also require that $A$ halts given any consequence profile $\gamma$ for $A$ and $U$. Such an agent is called a halting agent.

Main claim describing halting agent behavior

We begin with the case where the algorithm $A$ only ever mentions finitely many utilities. Fix $U$, and obtain a full consequence profile $\sigma$ for $A$ and $U$. It is provable in $\text{PA}$ that some $\gamma$ that agrees with $\sigma$ describes $C$, and so $\gamma$ determines $A$'s action. So for any such $\gamma$, we can write $A\left(\gamma \right)=a$ to mean that $A$ outputs $a$ if it is given an oracle described by $\gamma$. By the assumption that $A$ is a halting agent, $A\left(\gamma \right)$ is defined, and by ${\Sigma }_1$ completeness, $\text{PA}$ can see this fact for any specific $\gamma$.

Claim: Define a sequence $⟨{\gamma }_i⟩$ of consequence profiles that agree with $\sigma$, and a sequence $⟨a_i⟩$ of actions. First set ${\gamma }_0\left(a\right)=\perp$ for all $a$, and set $a_0=A\left({\gamma }_0\right)$. Given ${\gamma }_n$ and $a_n$, define ${\gamma }_{n+1}={\gamma }_n[a_n\mapsto \sigma (a_n\left)\right]$, i.e. ${\gamma }_{n+1}$ is ${\gamma }_n$ except that it maps $a_n$ to $\sigma \left(a_n\right)$. Define $a_{n+1}$ to be $A\left({\gamma }_{n+1}\right)$. Then it is the case that $A=a_k$, where $k$ is the least index such that for some $i<k$, $a_i=a_k$. Furthermore, ${\gamma }_k$ describes $C$ for $U$ and $A$. (The ${\gamma }_i$ and $a_i$ do not depend on the choice of $\sigma$, but we will use $\sigma$ in the proof.)

Example

(This section is skippable.)

Before we prove the claim, an example is perhaps in order. Consider a universe $U$ and an agent $A$ with $|A|=3$, and fix a full consequence profile $\sigma$ for $A$ and $U$. What we are looking at here is the strategy that $A$ follows, given the information it might receive from the oracle $C$. $$\begin{array}{cccc}{a}_2& a_0\bullet & & \\ & & & \\ a_0& a_1\bullet & & \\ & & a_1& a_1\\ & & & \\ & & a_x\bullet & a_2\bullet \end{array}$$ (The boxes and bullets are just markers for us to refer to.) The table is meant to be a cube, where the boxed $a_x$ ($x\in \{0,1,2\}$) is the lower left corner closest to us, and the boxed $a_0$ is the upper right corner farthest from us. Each entry in this cube gives the action $A\left(\gamma \right)$ for some $\gamma$ that agrees with $\sigma$. The $i$-th dimension corresponds to whether or not $\gamma \left(a_i\right)=\perp$.

For each action $a$, $A$ might see either just $C(a,\sigma (a\left)\right)=1$, or else $C(a,u)=1$ for all $u$. The up-down dimension corresponds to whether or not $C(a_0,u)$ holds for all $u$; the back-front dimension corresponds to whether or not $C(a_1,u)$ holds for all $u$; and the left-right dimension is for $a_2$. So, the boxed $a_0$ indicates that $A$ will perform action $a_0$ if $C$ returns 1 for every query; the $a_2$ to the left of the boxed $a_0$ indicates that $A$ does $a_2$ if $C$ returns 1 for every query about $a_0$ or $a_1$, and returns 0 for $(a_2,u)$ if $u\ne \sigma \left(a_2\right)$; the boxed $a_x$ indicates that $A$ does $a_x$ if $C$ returns 0 for $(a_i,u)$ if $u\ne \sigma \left(a_i\right)$, for $i\in \{0,1,2\}$; and so on.

Then the claim says that we start at the boxed $a_0$, with ${\gamma }_0\equiv \perp$, and follow the bullets. First ${\gamma }_1\left(a_0\right)=\sigma \left(a_0\right)$; then ${\gamma }_2\left(a_1\right)=\sigma \left(a_1\right)$; and finally ${\gamma }_3\left(a_2\right)=\sigma \left(a_2\right)$ takes us to $a_x$. The conclusion of the claim is that $A$ does $a_x$, since that is the first entry in the bulleted descent that repeats an action. (This is desirable behavior, as we can choose $a_x$ to be the $a_i$ with the greatest $\sigma \left(a_i\right)$. The claim says that in this situation, ${\gamma }_3=\sigma$ describes the true oracle $C$, so this $a_i$ will be optimal.)

If we replaced $a_1\bullet$ with $a_0\bullet$, the claim says that $A$ does $a_0$, as that is the first repeated action. In this case, we could have reached the conclusion pretty easily: by the previous discussion, $\text{PA}$ knows that $A$ does the action dictated by this table. So $\text{PA}$ can prove that if $\square_{\textsf{PA}}\ulcorner {\cal A}[{\cal U}] \ne a_1 \wedge {\cal A}[{\cal U}] \ne a_2 \urcorner $, then $A$ does some action in the back right of the cube. Both of those actions are $a_0$, so $A$ does not do $a_1$ or $a_2$. Hence $$\text{PA}⊢{\square }_{\text{PA}}┌A\left[U\right]\notin \{a_1,a_2\}┐\to A\left[U\right]\notin \{a_1,a_2\},$$ and by Lob's theorem, $\text{PA}⊢A\left[U\right]\notin \{a_1,a_2\}.$ Running the same argument again, we see that $A$ in fact does $a_0$.

Proof of main claim

Recall the claim: we have a sequence $⟨a_i⟩$ of actions and a sequence $⟨{\gamma }_i⟩$ of consequence profiles that agree with $\sigma$. We chose ${\gamma }_0\left(a\right)\equiv \perp$, $a_i=A\left({\gamma }_i\right)$ for all $i$, and ${\gamma }_{n+1}={\gamma }_n[a_n\mapsto \sigma (a_n\left)\right]$. The claim says that $A=a_k$ for the least $k$ such that $a_i=a_k$ for some $i<k$, and the oracle $C$ is described by ${\gamma }_k$. Note that, by definition, ${\gamma }_k\left(a_i\right)=\sigma \left(a_i\right)$ for $i<k$, and ${\gamma }_k\left(a_i\right)=\perp$ for $i\ge k$.

Proof of claim. First we prove, by induction on $k$ starting at zero, the following statement: $$\forall j<k:\text{PA}⊢\square ┌A\left[U\right]\ne a_j┐\to \square ┌A\left[U\right]\in \{a_i\mid i<j\}┐.$$ This is vacuous for $k=0$. So suppose we have the hypothesis for some $k>0$. We want to show that $$\text{PA}⊢\square ┌A\left[U\right]\ne a_k┐\to \square ┌A\left[U\right]\in \{a_i\mid i<k\}┐.$$ Reasoning in $\text{PA}$, suppose that $\square ┌A\left[U\right]\ne a_k┐$, and suppose also that $\square ┌A\left[U\right]\in \{a_i\mid i<k\}┐$.

Let $j$ be the smallest number such that $\square ┌A\left[U\right]\ne a_j┐$. By our suppositions, $j<k$. By the inductive hypothesis, then, $\forall a\notin \{a_i\mid i<j\}:\square ┌A\left[U\right]\ne a┐$. This tells us everything we need to know about $C$ to deduce what $A$ does; we know that $C$ is described by ${\gamma }_j$. Therefore the action is $A\left({\gamma }_j\right)=a_j$. In particular, $A\left[U\right]\in \{a_i\mid i<k\}$.

We have shown that $$\text{PA}⊢\square ┌A\left[U\right]\ne a_k┐\to (\square ┌A[U]\in \{a_i\mid i<k\}┐\to A[U]\in \{a_i\mid i<k\left\}\right).$$ This argument goes through if everything is "one level deeper," i.e. wrapped in an additional $\square$ (or, we can apply ${\Sigma }_1$ completeness of $\text{PA}$ and distributivity of $\square$ over $\to $). This gives $$\text{PA}⊢\square ┌A\left[U\right]\ne a_k┐\to \square ┌\square ┌A\left[U\right]\in \{a_i\mid i<k\}┐\to A\left[U\right]\in \{a_i\mid i<k\}┐.$$ By formalized Lob's theorem, we have the desired conclusion: $$\text{PA}⊢\square ┌A\left[U\right]\ne a_k┐\to \square ┌A\left[U\right]\in \{a_i\mid i<k\}┐.$$ Now, let $k$ be as in the claim, so it is the least index such that $a_i=a_k$ for some $i<k$. Reasoning again in $\text{PA}$, suppose that $\square ┌A\left[U\right]\in \{a_i\mid i<k\}┐$. Then $\forall a\notin \{a_i\mid i<k\}:\square ┌A\left[U\right]\ne a┐$. Using the statement just proved and the previous argument about what $C$ can look like, this gives that $\exists i\le k:A\left[U\right]=A\left({\gamma }_i\right)$. Since all such actions $A\left({\gamma }_i\right)$ are in $\{a_i\mid i<k\}$, this shows that $A\left[U\right]\in \{a_i\mid i<k\}$.

We just proved that $$\text{PA}⊢\square ┌A\left[U\right]\in \{a_i\mid i<k\}┐\to A\left[U\right]\in \{a_i\mid i<k\},$$ so by Lob's theorem, $$\text{PA}⊢A\left[U\right]\in \{a_i\mid i<k\}.$$ Running the same argument again, we know that $\exists i\le k:A\left[U\right]=A\left({\gamma }_i\right)$, and we know that $C$ is described by ${\gamma }_i$ for some $i\le k$. But for $i<k$, ${\gamma }_i\left(a_i\right)=\perp$ and $A\left({\gamma }_i\right)=a_i$. So by soundness, no such ${\gamma }_i$ can describe $C$. Hence ${\gamma }_k$ describes $C$ and $A\left[U\right]=A\left({\gamma }_k\right)=a_k$. QED

Corollary on uniqueness of UDT

Let us consider universes with $|U|$ infinite---there are infinitely many possible outcomes. (Each universe only has finitely many accessible outcomes; we are looking at a set of universes that are allowed to have outcomes in $N$, so the agent will have to ask $C$ about unboundedly many $(a,u)$ pairs.) We restrict to universes that are very simple: they are just maps from $A$ to $U$ that are easy to reason about. Recall that we assumed that agents are algorithms, modulo their oracles. In other words, for any consequence profile, they eventually halt given an oracle described by that profile. Now we give a corollary of the above claim, stating that UDT is unique among halting agents that are optimal for simple universes.

Corollary. Suppose a halting agent $A$ is optimal for all universes that implement a simple function $A\to U$. Then $A$ implements UDT, in the sense that $A$ checks if each action is provably not taken; takes any such action; and otherwise takes the action with the highest provable consequence. The order in which actions are diagonalized against can only depend on the actual consequences of actions that have already been checked. (So there is some action $a$ that $A$ always diagonalizes against; then for each $u\in U$, there is an action $a_u$ such that whenever $C(a,u)=1$, $A$ diagonalizes against $a_u$; for each $u,v\in U$, there is an action $a_{uv}$ such that whenever $C(a,u)=1$ and $C(a_u,v)=1$, $A$ diagonalizes against $a_{uv}$; and so on.)

Proof. Fix some agent $A$ with $|A|=n$. We will show that either $A$ fails on some simple universe $U$, or else $A$ is UDT in the above sense. Suppose that for some simple $U$ that implements the function $f:A\to U$, the oracle $C$ of $A\left[U\right]$ is not full, meaning that for some $a\in A$, $C(a,u)=1$ for all $u\in U$. So $k<n$, where $k$ is the index given by the main claim such that $A\left[U\right]=A\left({\gamma }_k\right)=a_k$.

Notice that the behavior dictated by the claim does not depend on the "true" consequences of all the actions in $A-\{a_i\mid i\le k\}$; we can show that the action $a_k$ happens just knowing what $A$ does for ${\gamma }_i$, $i\le k$. So let's modify $U$ to obtain a simple universe $U^{\prime }$ implementing $f^{\prime }=f[a\mapsto u^{\prime }]$, where $a$ is an action for which $\text{PA}⊢A\left[U\right]\ne a$, and $u^{\prime }$ is some utility larger than any number in the range of $f$. Now $A\left[U^{\prime }\right]\ne a$, and so $A$ is suboptimal in a simple universe.

This characterizes the behavior of any optimal $A$: $A$ must play chicken against each action in turn, and then choose the action with the highest unique consequence. Here, "playing chicken" means that $A\left({\gamma }_i\right)=a_i$, even though ${\gamma }_i\left(a_i\right)=\perp$.

When choosing which action to diagonalize against next, $A$ must choose only based on the provable consequences of the actions it has already diagonalized against; this is just saying that $A\left({\gamma }_i\right)$ is well-defined. If $A$ does not vary this choice, then there is a fixed enumeration $\{a_0,a_1,\dots ,a_{n-1}\}$ of $A$ such that $A$ plays chicken against each $a_i$ in order, in every universe. This recovers the usual formulation of UDT.

---

Discussion of assumptions

The assumption that $A$ must halt can be slightly relaxed; it only needs to halt for each ${\gamma }_i$. However, this might still be too restrictive. It is possible, as far as I know, that there is an agent that doesn't halt given some of those "possible" oracles, and yet performs optimally on simple universes (because none of those oracles ever actually happen, or when they do the default action is the correct one).

The transparency assumption on the universe doesn't weaken the conclusion about uniqueness of UDT, but it prevents applying the analysis of oracle-agent behavior to multi-agent situations, which are the most interesting universes. If there are multiple agents, it can be impossible to prove any consequences, because the other agent also has a provability oracle. Then $A$ can't even prove that the other agent's oracle won't always return 1 (because $\text{PA}$ is inconsistent), so it can't in general prove what happens in the universe.

[Tangent: Restricting to an oracle for statements of the form $\text{PA}⊢A\left[U\right]=a\to U\left[A\right]=u$ is meant to model an agent that has an oracle for expected utility of actions. Allowing an abstract decision procedure to have unrestricted oracles (or rather, any access to the code for $U$) makes it difficult (for me) to define UDT in a reasonable way. For example, say there are two agents, $A_1$ and $A_2$, both using UDT. When $A_1$ considers what strategy would be best for UDT to follow, it decides that it would be a great idea if any UDT that finds itself in the shoes of $A_2$ immediately donates all its resources to $A_1$. This agent is delusional. One way to fix this problem is to make a decision procedure be a function of only the expected utility of actions (or some other sort of information mentioning only the relationship between actions and utility.) The decision procedure should be abstracted from the utility function, so it should be abstracted away from the concrete world model.]