Formulas of arithmetic that behave like decision agents

[Nisan]

I wrote this post in the course of working through Vladimir Slepnev’s A model of UDT with a halting oracle. This post contains some of the ideas of Slepnev’s post, with all the proofs written out. The main formal difference is that while Slepnev’s post is about programs with access to a halting oracle, the “decision agents” in this post are formulas in Peano arithmetic. They are generally uncomputable and do not reason under uncertainty.

These ideas are due to Vladimir Slepnev and Vladimir Nesov. (Please let me know if I should credit anyone else.) I’m pretty sure none of this is original material on my part. It is possible that I have misinterpreted Slepnev’s post or introduced errors.

We are going to define a world function $U\left(\right)$, a $0$-ary function¹ that outputs an ordered pair $(a,b)\in Q^2$ of payoff values. There are functions ${\pi }_i$ such that ${\pi }_0(a,b)=a$ and ${\pi }_1(a,b)=b$ for any $a,b$. In fact ${\pi }_i(a,b)$ is a function in the three variables $i,a,$ and $b$.

We are also going to define an agent function $A(x,i)$ that outputs the symbol $C$ or $D$. The argument $x$ is supposed to be the Gödel number of the world function, and $i\in N$ is some sort of indexical information.

We want to define our agent such that

$A(┌\chi ┐,i)=\{\begin{array}{cc}D& \text{if}⊢A(┌\chi ┐,\underset{–}{i})=C\text{; else}\\ C& \text{if}⊢A(┌\chi ┐,\underset{–}{i})=D\text{; else}\\ C& \text{if}\exists a,b(⊢(A(┌\chi ┐,\underset{–}{i})=C\to {\pi }_{\underset{–}{i}}\left(\chi \right(\left)\right)=\underset{–}{a})\\ & \text{quad}\wedge \text{quad}\left(A\right(┌\chi ┐,\underset{–}{i})=D\to {\pi }_{\underset{–}{i}}(\chi \left(\right))=\underset{–}{b}))\\ & \text{quad}\wedge \text{quad}a>b\text{; else}\\ D& \end{array}$

($┌\omega ┐$ denotes the Gödel number of $\omega$. $⊢\omega$ means that $\omega$ is provable in Peano arithmetic.$\underset{–}{i}$ represents the numeral for $i$. I don’t care what value $A(x,i)$ has when $x$ isn’t the Gödel number of an appropriate $0$-ary function.)

There is some circularity in this tentative definition, because a formula standing for $A$ appears in the definition of $A$ itself. We get around this by using diagonalization. We’ll describe how this works just this once: First define the function $\varphi$ as follows:

$\varphi (┌\chi ┐,i,┌\psi ┐)=\{\begin{array}{cc}D& \text{if}⊢\psi (┌\chi ┐,\underset{–}{i})=C\text{; else}\\ C& \text{if}⊢\psi (┌\chi ┐,\underset{–}{i})=D\text{; else}\\ C& \text{if}\exists a,b(⊢(\psi (┌\chi ┐,\underset{–}{i})=C\to {\pi }_{\underset{–}{i}}\left(\chi \right(\left)\right)=\underset{–}{a})\\ & \text{quad}\wedge \text{quad}\left(\psi \right(┌\chi ┐,\underset{–}{i})=D\to {\pi }_{\underset{–}{i}}(\chi \left(\right))=\underset{–}{b}))\\ & \text{quad}\wedge \text{quad}a>b\text{; else}\\ D& \end{array}$

This function can be defined by a formula. Then the diagonal lemma gives us a formula $A$ such that $⊢A(x,i)=\varphi (x,i,┌A┐)$.

This is our (somewhat) rational decision agent. If it can prove it will do one thing, it does another; this is what Slepnev calls “playing chicken with the universe”. If it can prove that $C$ is an optimal strategy, it chooses $C$; and otherwise it chooses $D$.

First, a lemma about the causes and consequences of playing chicken:

Lemma 1. For any $\chi$,

1. $⊢\mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)\to \neg \mathrm{Con}\left(\mathrm{PA}\right)$

2. $⊢\neg \mathrm{Con}\left(\mathrm{PA}\right)\to A(┌\chi ┐,\underset{–}{i})=D$

3. $⊢\mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)\to \neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)$

4. $⊢\mathrm{Con}\left(\mathrm{PA}\right)\wedge \neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)\to A(┌\chi ┐,\underset{–}{i})=C$

($\mathrm{Prv}$ is a binary-valued function such that $\mathrm{Prv}(┌\omega ┐)$ is true exactly when there is a proof of $\omega$ in Peano arithmetic. For brevity we write $\mathrm{Prv}\left(\omega \right)$ instead.$\mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)$ is the proposition that Peano arithmetic, plus the axiom that Peano arithmetic is consistent, is a consistent theory.)

Proof. (1) By definition of $A$,

$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)& \to A(┌\chi ┐,i)=D& \end{array}$

So

$\begin{array}{ccc}⊢\mathrm{Prv}\left(\mathrm{Prv}\right(A(┌\chi ┐,\underset{–}{i})=C\left)\right)& \to \mathrm{Prv}\left(A\right(┌\chi ┐,i)=D)& \end{array}$
$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)& \to \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)\wedge \mathrm{Prv}\left(\mathrm{Prv}\right(A(┌\chi ┐,\underset{–}{i})=C\left)\right)& \\ & \to \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)\wedge \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)& \\ & \to \neg \mathrm{Con}\left(\mathrm{PA}\right)& \end{array}$

(2) By the principle of explosion,

$\begin{array}{ccc}⊢\neg \mathrm{Con}\left(\mathrm{PA}\right)& \to \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)& \\ & \to A(┌\chi ┐,\underset{–}{i})=D& \end{array}$

(3) By the definition of $A$,

$\begin{array}{ccc}⊢\neg \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)\wedge \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)& \to A(┌\chi ┐,\underset{–}{i})=C& \end{array}$
$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)& \to (\mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)\wedge \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D))\vee A(┌\chi ┐,\underset{–}{i})=C& \\ & \to \neg \mathrm{Con}\left(\mathrm{PA}\right)\vee A(┌\chi ┐,\underset{–}{i})=C& \end{array}$
$\begin{array}{ccc}⊢\mathrm{Prv}\left(\mathrm{Prv}\right(A(┌\chi ┐,\underset{–}{i})=D\left)\right)& \to \mathrm{Prv}(\neg \mathrm{Con}\left(\mathrm{PA}\right)\vee A(┌\chi ┐,\underset{–}{i})=C)& \end{array}$
$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)& \to \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)\wedge \mathrm{Prv}\left(\mathrm{Prv}\right(A(┌\chi ┐,\underset{–}{i})=D\left)\right)& \\ & \to \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)\wedge \mathrm{Prv}(\neg \mathrm{Con}\left(\mathrm{PA}\right)\vee A(┌\chi ┐,\underset{–}{i})=C)& \\ & \to \mathrm{Prv}(A(┌\chi ┐,\underset{–}{i})=D\wedge (\neg \mathrm{Con}\left(\mathrm{PA}\right)\vee A(┌\chi ┐,\underset{–}{i})=C))& \\ & \to \mathrm{Prv}\left(\neg \mathrm{Con}\right(\mathrm{PA}\left)\right)& \\ & \to \neg \mathrm{Con}\left(PA\mathrm{Con}\right(\mathrm{PA}\left)\right)& \end{array}$

(4)

$\begin{array}{ccc}⊢\neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)& \to \mathrm{Prv}\left(\neg \mathrm{Con}\right(\mathrm{PA}\left)\right)& \\ & \to \mathrm{Prv}\left(\mathrm{Prv}\right(A(┌\chi ┐,\underset{–}{i})=C\left)\right)& \\ & \to \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)& \end{array}$
$\begin{array}{ccc}⊢\mathrm{Con}\left(\mathrm{PA}\right)\wedge \neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)& \to \mathrm{Con}\left(\mathrm{PA}\right)\wedge \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)& \\ & \to \neg \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=C)\wedge \mathrm{Prv}\left(A\right(┌\chi ┐,\underset{–}{i})=D)& \\ & \to A(┌\chi ┐,\underset{–}{i})=C& \end{array}$

$\square$

If we assume consistency of $\mathrm{PA}\mathrm{Con}\left(\mathrm{PA}\right)$ (which entails consistency of $\mathrm{PA}$), then parts (1) and (3) of Lemma 1 tell us that for any $i$, $⊬A(┌\chi ┐,\underset{–}{i})=C$ and $⊬A(┌\chi ┐,\underset{–}{i})=D$. So the agent never actually plays chicken.

Now let’s see how our agent fares on a straightforward decision problem:

Proposition 2. Let $\alpha ,\beta \in Q$ and suppose

$U\left(\right)=\{\begin{array}{cc}(\alpha ,0)& \text{rm if}A(┌U┐,0)=C\\ (\beta ,0)& \text{rm if}A(┌U┐,0)=D\end{array}$

Assume consistency of $\mathrm{PA}\mathrm{Con}\left(\mathrm{PA}\right)$. Then $A(┌U┐,0)=C$ if and only if $\alpha >\beta$.

Proof. If we assume consistency of $\mathrm{PA}\mathrm{Con}\left(\mathrm{PA}\right)$, then Lemma 1 tells us that the agent doesn’t play chicken. So the agent will choose $C$ if and only if it determines that choosing $C$ is optimal.

We have

$\begin{array}{ccc}⊢(A(┌U┐,0)=C\to {\pi }_{0}U\left(\right)=\underset{–}{\alpha })\wedge (A(┌U┐,0)=D\to {\pi }_{0}U\left(\right)=\underset{–}{\beta })& & \end{array}$

Suppose $\alpha >\beta$. Then clearly

$\begin{array}{ccc}\exists a,b⊢(A(┌U┐,0)=C\to {\pi }_{0}U\left(\right)=\underset{–}{a})\wedge (A(┌U┐,0)=D\to {\pi }_{0}U\left(\right)=\underset{–}{b})\wedge a>b& & \end{array}$

So $A(┌U┐,0)=C$.

As for the converse: We have $⊢\left(A\right(┌U┐,0)=C\to {\pi }_{0}U()=\underset{–}{\alpha })$. If also

$\begin{array}{ccc}⊢\left(A\right(┌U┐,0)=C\to {\pi }_{0}U()=\underset{–}{a})& & \end{array}$

and $a\ne \alpha$, then $⊢\left(A\right(┌U┐,0)=D)$. By Lemma 1(3) and consistency of $\mathrm{PA}\mathrm{Con}\left(\mathrm{PA}\right)$, this cannot happen. So

$\begin{array}{ccc}⊬\left(A\right(┌U┐,0)=C\to {\pi }_{0}U()=\underset{–}{a})& & \end{array}$

Similarly, we have

$\begin{array}{ccc}⊬\left(A\right(┌U┐,0)=D\to {\pi }_{0}U()=\underset{–}{b})& & \end{array}$

for all $b\ne \beta$. So

$\begin{array}{ccc}\mathrm{\exists ̸}a,b⊢\left(A\right(┌U┐,0)=C\to {\pi }_{0}U()=\underset{–}{a})\wedge \left(A\right(┌U┐,0)=D\to {\pi }_{0}U()=\underset{–}{b})\wedge a>b& & \end{array}$

So the agent doesn’t decide that $C$ is optimal, and $A(┌U┐,0)=D$.

$\square$

Now let’s see how $A$ fares on a symmetric Prisoner’s Dilemma with itself:

Proposition 3. Let

$U\left(\right)=\{\begin{array}{cc}(1,1)& \text{rm if}A(┌U┐,0)=C\wedge A(┌U┐,1)=C\\ (-1,2)& \text{rm if}A(┌U┐,0)=C\wedge A(┌U┐,1)=D\\ (2,-1)& \text{rm if}A(┌U┐,0)=D\wedge A(┌U┐,1)=C\\ (0,0)& \text{rm if}A(┌U┐,0)=D\wedge A(┌U┐,1)=D\end{array}$

Then, assuming consistency of $\mathrm{PA}\mathrm{Con}\left(\mathrm{PA}\right)$, we have $A(┌U┐,0)=C=A(┌U┐,1)$.

Proof.

(This proof uses Löb’s theorem, and that makes it confusing. Vladimir Slepnev points out that Löb’s theorem is not really necessary here; a simpler proof appears in the comments.)

$\begin{array}{ccc}⊢A(┌U┐,0)=A(┌U┐,1)& \to ((A(┌U┐,0)=C\to {\pi }_{0}U\left(\right)=1)\wedge (A(┌U┐,0)=D\to {\pi }_{0}U\left(\right)=0))& \end{array}$
$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌U┐,0)=A(┌U┐,1\left)\right)& \to \exists a,b.\mathrm{Prv}(\left(A\right(┌U┐,0)=C\to {\pi }_{0}U()=\underset{–}{a})& \\ & \wedge \left(A\right(┌U┐,0)=D\to {\pi }_{0}U()=\underset{–}{b}))\wedge a>b& \end{array}$
Looking at the definition of $A$, we see that

$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌U┐,0)=A(┌U┐,1\left)\right)& \to \mathrm{Prv}\left(A\right(┌U┐,0)=C)\vee \mathrm{Prv}\left(A\right(┌U┐,0)=D)& \\ & \vee A(┌U┐,0)=C& \end{array}$
By Lemma 1, (1) and (3),

$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌U┐,0)=A(┌U┐,1\left)\right)& \to \neg \mathrm{Con}\left(\mathrm{PA}\right)\vee \neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)\vee A(┌U┐,0)=C& \end{array}$

Similarly,

$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌U┐,0)=A(┌U┐,1\left)\right)& \to \neg \mathrm{Con}\left(\mathrm{PA}\right)\vee \neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)\vee A(┌U┐,1)=C& \end{array}$

So

$\begin{array}{ccc}(\ast )⊢\mathrm{Prv}\left(A\right(┌U┐,0)=A(┌U┐,1\left)\right)& \to \neg \mathrm{Con}\left(\mathrm{PA}\right)\vee (\mathrm{Con}\left(\mathrm{PA}\right)\wedge \neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right))& \\ & \vee A(┌U┐,0)=C=A(┌U┐,1)& \end{array}$

Applying Lemma 1(2) and (4),

$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌U┐,0)=A(┌U┐,1\left)\right)& \to A(┌U┐,0)=D=A(┌U┐,1)& \\ & \vee A(┌U┐,0)=C=A(┌U┐,1)& \\ & \vee A(┌U┐,0)=C=A(┌U┐,1)& \\ & \to A(┌U┐,0)=A(┌U┐,1)& \end{array}$

By Löb’s theorem,

$\begin{array}{ccc}⊢A(┌U┐,0)=A(┌U┐,1)& & \end{array}$
$\begin{array}{ccc}⊢\mathrm{Prv}\left(A\right(┌U┐,0)=A(┌U┐,1\left)\right)& & \end{array}$

By $(\ast )$, we have

$\begin{array}{ccc}⊢\neg \mathrm{Con}\left(\mathrm{PA}\right)\vee (\mathrm{Con}\left(\mathrm{PA}\right)\wedge \neg \mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right))\vee A(┌U┐,0)=C=A(┌U┐,1)& & \end{array}$

So, assuming $\mathrm{Con}\left(\mathrm{PA}\mathrm{Con}\right(\mathrm{PA}\left)\right)$, we conclude that $A(┌U┐,0)=C=A(┌U┐,1)$.

$\square$

The definition of $A$ treats the choices $C$ and $D$ differently; so it is worth checking that $A$ behaves correctly in the Prisoner’s Dilemma when the effects of $C$ and $D$ are switched:

Proposition 4. Let

$U\left(\right)=\{\begin{array}{cc}(0,0)& \text{rm if}A(┌U┐,0)=C\wedge A(┌U┐,1)=C\\ (2,-1)& \text{rm if}A(┌U┐,0)=C\wedge A(┌U┐,1)=D\\ (-1,2)& \text{rm if}A(┌U┐,0)=D\wedge A(┌U┐,1)=C\\ (1,1)& \text{rm if}A(┌U┐,0)=D\wedge A(┌U┐,1)=D\end{array}$

Then, assuming consistency of $\mathrm{PA}\mathrm{Con}\left(\mathrm{PA}\right)$, we have $A(┌U┐,0)=D=A(┌U┐,1)$.

A proof appears in the comments.

There are a number of questions one can explore with this formalism: What is the correct generalization of $A$ that can choose between $n$ actions, and not just two? How about infinitely many actions? What about theories other than Peano arithmetic? How do we accomodate payoffs that are real numbers? How do we make agents that can reason under uncertainty? How do we make agents that are computable algorithms rather than arithmetic formulas? How does $A$ fare on a Prisoner’s Dilemma with asymmetric payoff matrix? In a two-person game where the payoff to player $A_0$ is independent of the behavior of $A_1$, can $A_1$ deduce the behavior of $A_0$? What happens when we replace the third line of the definition of $A$ with

$\begin{array}{cc}⊢\exists a,b& \left(A\right(┌U┐,\underset{–}{i})=C\to {\pi }_{\underset{–}{i}}U()=a)\\ & \wedge \left(A\right(┌U┐,\underset{–}{i})=D\to {\pi }_{\underset{–}{i}}U()=b)\\ & \wedge a>b\end{array}$

? What is a (good) definition of “decision problem”? Is there a theorem that says that our agent $A$ is, in a certain sense, optimal?

¹Every $k$-ary function $U$ in this article is defined by a formula $\varphi (x_1,\dots ,x_k,y)$ with $k1$ free variables such that $⊢\exists y.\varphi (x_1,\dots ,x_k,y)$ and $⊢\varphi (x_1,\dots ,x_k,y)\wedge \varphi (x_1,\dots ,x_k,y^{\prime })\to y=y^{\prime }$. By a standard abuse of notation, when the name of a function like $U$ appears in a formula of arithmetic, what we really mean is the formula $\varphi$ that defines it.