LESSWRONG
Petrov Day
LW

Thanks for taking the time to think about this! But it seems to me that Löb's theorem should not be required to prove proposition 3 for a properly defined A. I'm guessing that you inadvertently defined A asymmetrically, as described in "AI cooperation in practice", instead of the symmetric way described in "model of UDT with a halting oracle" where swapping C and D shouldn't affect anything except the chicken stage.

[-]Nisan14y60

Ah, I see. The agent described in "A model of UDT with a halting oracle" is more symmetric, because it has a choice of three actions: "Cooperate", "Defect", and "Break down and cry" (if we count failing to act as an action).

I think I see a way to prove the proposition without using Löb's theorem, and I don't even need to change the definition of A. I'll post here whether it works out.

Thanks for the comment!

[-]orthonormal14y30

Did it work out?

[-]Nisan14y40

I still intend to write up an answer to that question.

[-]orthonormal14y00

Great!

[-]Nisan13y70

I finally did it, and I believe it works.

[-]Nisan14y100

I'm having trouble proving Conjecture 4. I seem to need the intermediate result

$\\vdash \\forall x \\neq 0 \\operatorname\{Prv\}\(\\underline\{x\} \\neq 0\$ )

And I don't know how to prove that.

EDIT: I now have a proof of this here.

[-]Zetetic14y10

I only looked at this for a bit so I could be totally mistaken, but I'll look at it closely soon, it's a nice write up!

My thoughts:

A change of variables/values in your proof of proposition 3 definitely doesn't yield conjecture 4? At first glance it looks like you could just change the variables and flip the indicies for the projections (use pi_1 instead of pi_0) and in the functions A[U,i]. If you look at the U() defined for conjecture 4, it's exactly the one in proposition 3 with the indices i flipped and C and D flipped, so it's surprising to me if this doesn't work or if there isn't some other minor transformation of the the first proof that yields a proof of conjecture 4.

[-]AlexMennen14y20

The agent function is not defined symmetrically with respect to C and D, so flipping the roles of C and D in the universe without also flipping their roles in the agent function does not guarantee that the outcome would change as desired.

[-]Zetetic14y10

Yes, you're right. Looking at the agent function, the relevant rule seems to be defined for the sole purpose of allowing the agent to cooperate in the even that cooperation is provably better than than defecting. Taking this out of context, it allows the agent to choose one of the actions it can take if it is provably better than the other. It seems like the simple fix is just to add this:

$\\exists a,b\\operatorname\{Prv\}\\biggl\(\(\\psi\(\\ulcorner \\chi\\urcorner\\underline\{i\}\$ =D\to\pi_{\underline{i}}\chi()=\underline{a})\\\mbox{\quad\quad\quad\quad}\wedge(\psi(\ulcorner%20U%20\urcorner,\underline{i})=C\to\pi_{\underline{i}}\chi()=\underline{b})\biggr)\wedge%20a%20%3E%20b)

If you alter the agent definition by replacing the third line with this and the fourth with C you have an agent that is like the original one but can be used to prove conjecture 4 but not prop 3, right? So if you instead add this line to the current agent definition and simply leave D as the last line, then if neither the old third line nor this new one hold we simply pick D, which is neither provably better nor provably worse than C, so that's fine. It seems that we can also prove conjecture 4 by using the new line in lieu of the old one, which should allow us to use a proof that is essentially symmetric to the proof of proposition 3.

Does that seem like a reasonable fix?

[-]Nisan14y20

So you modify the agent so that line 3 says "cooperating is provably better than defecting" and line 4 says "defecting is provably better than cooperating". But line 3 comes before line 4, so in proving Conjecture 4 you'd still have to show that the condition in line 3 does not obtain. Or you could prove that line 3 and line 4 can't both obtain; I haven't figured out exactly how to do this yet.

[-]Zetetic14y00

Well the agent definition contains a series of conditionals. You have as the last three lines: if "cooperating is provably better than defecting", then cooperate; else, if "defecting is provably better than cooperating" then defect; else defect. Intuitively, assuming the agent's utility function is consistent, only one antecedent clause will evaluate to true. In the case that the first one does, the agent will output C. Otherwise, it will move through to the next part of the conditional and if that evaluates to true the agent will output D. If not, then it will output D anyway. Because of this, I would go for proving that line three and 4 can't both obtain.

Or you could prove that line 3 and line 4 can't both obtain; I haven't figured out exactly how to do this yet.

How about this? Suppose condition 3 and 4 both obtain. Then there exists and a and b such that U(C) = #a and U(D) = #b (switching out the underline for '#'). Also, there exists a p and q such that p > q and U(D) = #p and U(C) = #q. Now U(C) = #a > #b = U(D) = #c > #q = U(C) so U(C) > U(C). I may actually be confused on some details, since you indicate that a and b are numbers rather than variables (for instance in proposition 2 you select a and b as rational numbers), yet you further denote numerals for them, but I'm assuming that a >b iff #a > #b. Is this a valid assumption? I feel as though I'm missing some details here, and I'm not 100% sure how to fill them in. If my assumption isn't valid I have a couple of other ideas. I'm not sure if I should be thinking of #a as 'a' under some interpretation.

Going a little bit further, it looks like your lemma 1 only invokes the first two lines and can easily be extended for use in conjecture 4 - look at parts 1 and 3. Part 1 is one step away from being identical to part 3 with C instead of D.
~Con(PA) -> ~ Con(PA + anything), just plug in Con(PA) in there. Adding axioms can't make an inconsistent theory consistent. Getting the analogous lemma to use in conjecture 4 looks pretty straightforward - switching out C with D and vice versa in each of the parts yields another true four part lemma, identical in form but for the switched D's and C's so you can use them analogously to how you used the original lemma 1 in the proof of proposition 3.

[-]Nisan14y20

Yep, this sounds about right. I think one do has to prove "#a > #b if a > b", or rather $a>b \\to \\operatorname\{Prv\}\(\\ulcorner \\dot a> \\dot b \\urcorner\$ )

[-]Nisan14y20

One can try to take the proof of Proposition 3 and switch C and D around, but one quickly runs into difficulty: The second line of that proof contains

$\\exists a,b \\operatorname\{Prv\} \\biggl\( \(A\(\\ulcorner U \\urcorner, 0\$ %20=%20C%20\to%20\pi_0%20U()%20=%20\underline{a}%20)%20\\%20\mbox{\quad\quad\quad\quad}%20\wedge%20(A(\ulcorner%20U%20\urcorner,%200)%20=%20D%20\to%20\pi_0%20U()%20=%20\underline{b})%20\biggr)%20\wedge%20a%3Eb)

"cooperating provably results in a better payoff than defecting". This is enough to convince the agent to cooperate. But if you switch C and D, you end up with a proposition that means "cooperating provably results in a worse payoff than defecting". This is not enough to convince the agent to defect. The agent will defect if there is no proof that cooperating results in a better payoff than defecting. So at least one would have to say a bit more here in the proof.

[-]Karl14y10

I'm confused. What's the distinction between x and $\\underline\{x\}$ here?

[-]Nisan14y20

Briefly, $x$ is a variable, while $\\underline\{x\}$ is a numeral — i.e., the string $1\+\\cdots\+1$ where $1$ occurs x times. I just learned that the standard notation is not $\\underline\{x\}$ but $\\dot\{x\}$ .

Less briefly: As I say in this comment, when I write $\\operatorname\{Prv\}\(\\underline\{x\} \\neq 0\$ ), what I really ought to write is $\\operatorname\{Prv\}\(\\operatorname\{Sub\}\(\\ulcorner y \\neq 0 \\urcorner, x\$ )), where $\\operatorname\{Sub\}\(z,x\$ ) interprets z as the Gödel number of a string of symbols and replaces every occurrence of the first free variable with the string 1+...+1, where 1 occurs x times.

[-]911truther14y80

Your work is wrong. To apply diagonal lemma the definition of phi must be a formula, since you write |- (which is not a formula in PA) I assume you meant it as shorthand for Godels Bew (which is), but you can't existentially quantify Bew like you did in line 3 of the definition.

[-]Vladimir_Nesov14y150

"Your work is wrong" is an unfair characterization of presence of a minor technical inaccuracy.

[-]Nisan14y130

Yes, I really mean phi to be a formula based on the provability predicate. The third line is really shorthand for

$\\exists a,b \\operatorname\{Prv\}\(\\operatorname\{Sub\}\(\\ulcorner \.\.\. = x \.\.\. = y \\urcorner,a,b\$ ))

where Sub is a function that replaces the first two free variables in the Gödelized formula with a and b. So we can quantify over a and b.

I suppose I should mention this in the post.

[-]lukeprog14y70

I'm not mathy enough to understand this post, but...

Thanks for going to all this trouble! Hopefully those more mathy than I can check your work and extend it.
Nice title.

[-]orthonormal14y60

It's awesome of you to write this up! I'm going to have to look through it more carefully tomorrow.

[-]Vladimir_Nesov14y60

One idea I take out of your definition of A is that it's potentially useful to think about decisions as giving "strategies" that respond not just to "observations" (that were "withheld" during a decision), but also to "observations about utility", that could factor out the differences between different agents and allow them to coordinate, the way a single agent can coordinate with its copies or counterfactual variants by deciding on a whole strategy instead of just a single action. Not sure if (or how) that works for PD though...

[-]Nisan13y50

Proof of Proposition 3 (without using Löb's theorem). This proof uses Lemma 6.

For brevity, let $A\_i$ stand for $A\(\\ulcorner U \\urcorner, i\$ ), let $U\_i$ stand for $\\pi\_i U\(\$ ), and let $\\phi\_i\(a,b\$ ) stand for $\(A\_i = C \\to U\_i = a\$ %20\wedge%20(A_i%20=%20D%20\to%20U_i%20=%20b)).

First, notice that

$\\begin\{align\*\} \\vdash \\forall a,b \( a>b &\\to \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \(a = 1 \\wedge b = 0\$ %0A\\%20\vee%20&%20(a%20\neq%20-1%20\wedge%20a%20\neq%201)%0A\\%20\vee%20&%20(b%20\neq%200%20\wedge%20b%20\neq%202)%0A\end{array}%0A\\&\to%20\begin{array}[t]{r@{\,}ll}%0A&%20\operatorname{Prv}(%20\dot{a}%20=%201%20\wedge%20\dot{b}%20=%200)%20&%20\mbox{by%20Lemma%206(b),(f)}%0A\\%20\vee%20&%20\operatorname{Prv}(\dot{a}%20\neq%20-1%20\wedge%20\dot{a}%20\neq%201)%20&%0A\\%20\vee%20&%20\operatorname{Prv}(%20\dot{b}%20\neq%200%20\wedge%20\dot{b}%20\neq%202))%20&%0A\end{array}%0A\end{align*})

$\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_0%20=%20C%20\to)

$\\begin\{align\*\} &\\to \\exists a,b \(\\operatorname\{Prv\}\(\\phi\_0\(\\dot\{a\},\\dot\{b\}\$ )%20\wedge%20a%20%3E%20b)%20&%0A\\&\to%20\exists%20a,b%20(\begin{array}[t]{r@{\,}l}%0A&\operatorname{Prv}(%20\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}=1%20\wedge%20\dot{b}%20=%200)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}%20\neq%20-1%20\wedge%20\dot{a}%20\neq%201)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{b}%20\neq%200%20\wedge%20\dot{b}%20\neq%202))%0A\end{array}%20&%0A\\&\to%20\exists%20a,b%20(%20\begin{array}[t]{r@{\,}l}%0A&%20\operatorname{Prv}((A_0%20=%20C%20\to%20U_0%20=%201)%20\wedge%20(A_0%20=%20D%20\to%20U_0%20=%200))%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20C%20\to%20U_0%20\neq%20-1%20\wedge%20U_0%20\neq%201)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20D%20\to%20U_0%20\neq%200%20\wedge%20U_0%20\neq%202))%0A\end{array}%20&%20\mbox{by%20definition%20of%20}%20\phi_0%0A\end{align*})

$\\begin\{align\*\} \\qquad\\qquad &\\to \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \\operatorname\{Prv\}\(\(A\_0 = C \\to A\_1 = C\$ %20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20D))%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20C\to%20\bot)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20=%20D\to%20\bot)%0A\end{array}%20&%0A\\&\to%20\begin{array}[t]{r@{\,}l}%0A&%20\operatorname{Prv}(A_0%20=%20A_1)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20C)%0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20D)%0A\end{array}%20&%0A\\&\to%20\operatorname{Prv}(A_0%20=%20A_1)%20&%20\mbox{by%20Lemma%201.1,3}%0A\\&\to%20\operatorname{Prv}(\phi_0(1,0))%20&%0A\\&\to%20\exists%20a,b%20\operatorname{Prv}(\phi_1(\dot{a},\dot{b}))%20\wedge%20a%3Eb%20&%0A\\&\to%20A_1%20=%20C%0A\end{align*})

Similarly,

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_1%20=%20C%20\to%20A_0%20=%20C)

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_0%20=%20A_1)

$\\begin\{align\*\} PA & \\vdash \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \\neg \\operatorname\{Con\}\(\\operatorname\{PA\}\$ %0A\\%20\vee%20&%20(%20\operatorname{Con}(\operatorname{PA})%20\wedge%20\neg%20\operatorname{Con}(\operatorname{PA}%20+%20\operatorname{Con}(\operatorname{PA})))%20%0A\\%20\vee%20&%20(\operatorname{Con}(\operatorname{PA}%20+%20\operatorname{Con}(\operatorname{PA}))%20\wedge%20A_0%20=%20A_1)%0A\end{array}%20&%0A\\%20&%20\vdash%20\begin{array}[t]{r@{\,}l}%0A&%20A_0%20=%20D%20=%20A_1%0A\\%20\vee%20&%20A_0%20=%20C%20=%20A_1%0A\\%20\vee%20&%20A_0%20=%20A_1%0A\end{array}%20&%20\mbox{by%20Lemma%201.2,4}%0A\\%20&%20\vdash%20A_0%20=%20A_1%0A\\%20&%20\vdash%20\phi_0(1,0)%0A\end{align*})

So there exist natural numbers $a$ and $b$ such that $\\operatorname\{Prv\}\(\\phi\_0\(\\dot\{a\},\\dot\{b\}\$ )%20\wedge%20a%3Eb) is true. Therefore, assuming consistency of $PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ ), by the definition of $A$ , we have $A\_0 = C$ . Similarly, $A\_1 = C$ .

$\\square$

[-]Nisan13y40

Proof of Proposition 4. This is kinda similar to the new proof of Proposition 3. It uses Lemma 6.

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_0%20=%20C%20\to)

$\\begin\{align\*\} &\\to \\exists a,b \(\\operatorname\{Prv\}\(\\phi\_0\(\\dot\{a\},\\dot\{b\}\$ )%20\wedge%20a%20%3E%20b)%20&%0A\\&\to%20\exists%20a,b%20(\operatorname{Prv}(\phi_0(\dot{a},\dot{b}))%20\wedge%20(%20\begin{array}[t]{r@{\,}l}%0A&%20(a%20\neq%200%20\wedge%20a%20\neq%202)%0A\\%20\vee%20&%20(b%20\neq%20-1%20\wedge%20b%20\neq%201)%0A\\%20\vee%20&%20(a%20=%200%20\wedge%20b%20=%20-1)%0A\\%20\vee%20&%20(a%20=%202%20\wedge%20b%20=%201)%0A\\%20\vee%20&%20(a%20=%202%20\wedge%20b%20=%20-1)))%0A\end{array}%20&%0A\\&\to%20\exists%20a,b%20(%20\begin{array}[t]{r@{\,}l}%0A&%20\operatorname{Prv}(%20\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}%20\neq%200%20\wedge%20\dot{a}%20\neq%202)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{b}%20\neq%201%20\wedge%20\dot{b}%20\neq%201)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}%20=%200%20\wedge%20\dot{b}%20=%20-1)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}%20=%202%20\wedge%20\dot{b}%20=%201)%0A\\%20\vee%20&%20\operatorname{Prv}(\phi_0(\dot{a},\dot{b})%20\wedge%20\dot{a}%20=%202%20\wedge%20\dot{b}%20=%20-1))%0A\end{array}%20&%20\mbox{by%20Lemma%206(b),(f)}%0A\end{align*})

$\\begin\{align\*\} &\\to \\exists a,b \( \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \\operatorname\{Prv\}\( A\_0 \\neq C\$ %0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20D)%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20C)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C))%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20D))%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C)))%0A\end{array}%20&%0A\end{align*})

$\\begin\{align\*\} &\\to \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \\operatorname\{Prv\}\(A\_0 \\neq C\$ %0A\\%20\vee%20&%20\operatorname{Prv}(A_0%20\neq%20D)%0A\\%20\vee%20&%20\operatorname{Prv}(A_1%20=%20C)%0A\\%20\vee%20&%20\operatorname{Prv}(A_1%20=%20D)%0A\\%20\vee%20&%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C))%0A\end{array}%20&%0A\\&\to%20\operatorname{Prv}((A_0%20=%20C%20\to%20A_1%20=%20D)%20\wedge%20(A_0%20=%20D%20\to%20A_1%20=%20C))%20&%20\mbox{by%20Lemma%201.1,3}%0A\\&\to%20\operatorname{Prv}((A_1%20=%20C%20\to%20A_0%20=%20D)%20\wedge%20(A_1%20=%20D%20\to%20A_0%20=%20C))%20&%0A\\&\to%20\operatorname{Prv}((A_1%20=%20C%20\to%20U_1%20=%202)%20\wedge%20(A_1%20=%20D%20\to%20U_1%20=%20-1))%20&%0A\\&\to%20\exists%20a,b%20(\operatorname{Prv}(\phi_1(\dot{a},\dot{b}))%20\wedge%20a%3Eb)%20&%0A\\&\to%20A_1%20=%20C%20&%0A\end{align*})

Similarly,

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_1%20=%20C%20\to%20A_0%20=%20C)

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_0%20=%20A_1)

$\\begin\{align\*\} PA & \\vdash \\begin\{array\}\[t\]\{r@\{\\,\}l\} & \\neg \\operatorname\{Con\}\(\\operatorname\{PA\}\$ %0A\\%20\vee%20&%20(\operatorname{Con}(\operatorname{PA})%20\wedge%20\neg%20\operatorname{Con}(\operatorname{PA}%20+%20\operatorname{Con}(\operatorname{PA})))%20%0A\\%20\vee%20&%20(\operatorname{Con}(\operatorname{PA}%20+%20\operatorname{Con}(\operatorname{PA}))%20\wedge%20A_0%20=%20A_1)%0A\end{array}%20&%20\mbox{by%20definition%20of%20}%20A%0A\\%20&%20\vdash%20\begin{array}[t]{r@{\,}l}%0A&%20A_0%20=%20D%20=%20A_1%0A\\%20\vee%20&%20A_0%20=%20C%20=%20A_1%0A\\%20\vee%20&%20A_0%20=%20A_1%0A\end{array}%20&%20\mbox{by%20Lemma%201.2,4}%0A\\%20&%20\vdash%20A_0%20=%20A_1%20&%0A\\%20&%20\vdash%20\phi_0(0,1)%20&%0A\end{align*})

Suppose also that $\\vdash \\phi\(\\dot\{a\}, \\dot\{b\}\$ ) for some $a \\neq 0$ and some $b$ . Then

$\\begin\{align\*\} & \\vdash \\phi\_0\(0, 1\$ %20\wedge%20\phi_0(\dot{a},%20\dot{b})%0A\\&%20\vdash%20(A_0%20=%20C%20\to%20U_0%20=%200)%20\wedge%20(A_0%20=%20C%20\to%20U_0%20=%20\dot{a})%0A\\&%20\vdash%20A_0%20=%20C%20\to%200%20=%20U_0%20=%20\dot{a}%0A\\&%20\vdash%20A_0%20=%20C%20\to%20\bot%0A\\&%20\vdash%20A_0%20\neq%20C%0A\end{align*})

Assuming consistency of $\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ ), this is impossible by Lemma 1.3. So if $\\vdash \\phi\_0\(\\dot\{a\}, \\dot\{b\}\$ ), then $a$ must be $0$ . Similarly, one can prove that $b$ must be $1$ . Thus, assuming consistency of $\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ ),

$\\nexists a,b \\in \\mathbb\{Q\} \(\(\\vdash \\phi\_0\(\\dot\{a\}, \\dot\{b\}\$ )%20\wedge%20a%20%3E%20b))

So, by the definition of $A$ , we have $A\_0 = D$ . Similarly, $A\_1 = D$ .

$\\square$

[-]AlexMennen14y40

Here's my meager attempt at contribution. And my apologies for not knowing LaTeX.

if exists a,b: provable([A(U,i)=C implies pi(i)(U())=a] and [A(U,i)=D implies pi(i)(U())=b] and [a>b]):
C
else:
D

You can do a lot better than this. Consider, for instance:

if exists a: provable([A(U,i)=C implies p(i)(U())>=a] and [A(U,i)=D implies pi(i)(U())<=a]):
C
else:
D

Consider the set S of all sets S(k) such that provable(A(U,i)=C implies pi_i(U()) is in S(k)). Then A(U,i)=C implies pi_i(U()) is in intersection(S). I don't know much about formal arithmetic, so I couldn't say whether it is necessary true that provable(A(U,i)=C implies pi(i)(U()) is in intersection(S)). But if that is true, then intersection(S)) is in S, and thus there exists a unique most specific S(k) such that provable(A(U,i)=C implies pi(i)(U()) is in S(k)). If it is possible in formal arithmetic to identify this set, then you can establish a utility function over such minimal sets of possible values of pi(i)(U()) implied by A(U,i)=C. For example, if that set is finite, the its utility could just be the average of its members. And then you could do the same sort of thing for A(U,i)=D and compare the utilities of the resulting sets of possibilities. This would essentially give you a single utility value for each choice, and you wouldn't get stuck if you can't prove that each output of A implies some unique value of pi(i)(U()).

What is the correct generalization of that can choose between n actions, and not just two? How about infinitely many actions?

For finite sets of actions, one possibility is that you can compare every pair of actions, giving you a partial ordering of the set, and then you could choose a maximal element. Alternatively, if my earlier idea for improving on the comparisons works, you can assign a utility to each possible action, so you can just choose the best one. If you have infinitely many possible actions, this will of course give you problems, since it can turn into a "name the biggest number" contest.

Note that we are intending to talk about agents that optimize over how U() works, but your framework also allows the creation of agents that optimize over how pi(i)(_) works. For instance, consider the following scenario:
U(): return (0, 0)
pi(i)(a,b): return 1 if A(U,i)=C, else 0
In this case, A(U,i) would output C, but not because it would imply anything about U. It might make sense to have some computability restriction on pi so that all such agents will actually be optimizing the world function rather than their own utility functions.

[-]Nisan13y20

Proof of Proposition 6. This proof uses Fact 5, the converse Barcan formula.

Strictly speaking, variables in Peano arithmetic are supposed to refer to natural numbers, and axioms like $\\forall x \. x \+ 1 > 0$ reflect this. But in this post, we have been treating variables like rational numbers! In fact, there are ways of talking about rational numbers using Peano arithmetic, and so far in this post we haven't bothered to write them out. But for this proof it will be important to distinguish between naturals and rationals. First we'll prove literal readings of (a) - (e) — that is, we'll assume variables refer to natural numbers. Then we'll indicate how to extend the proofs to rational versions of the Lemma.

(a)

$\\begin\{align\*\} & \\vdash \\forall x\_1, \\dots, x\_k \(P\(x\_1, \\dots, x\_k\$ %20\to%20Q(x_1,%20\dots,%20x_k))%20&%0A\\&%20\vdash%20\operatorname{Prv}(\forall%20x_1,%20\dots,%20x_k%20(P(x_1,%20\dots,%20x_k)%20\to%20Q(x_1,%20\dots,%20x_k)))%20&%0A\\&%20\vdash%20\forall%20x_1,%20\dots,%20x_k%20\operatorname{Prv}(P(\dot{x}_1,%20\dots,%20\dot{x}_k)%20\to%20Q(\dot{x}_1,%20\dots,%20\dot{x}_k))%20&%20\mbox{(converse%20Barcan%20formula)}%0A\\&%20\vdash%20\forall%20x_1,%20\dots,%20x_k%20\operatorname{Prv}(P(\dot{x}_1,%20\dots,%20\dot{x}_k))%20\to%20\operatorname{Prv}(Q(\dot{x}_1,%20\dots,%20\dot{x}_k))%20&%0A\end{align*})

(b)

$\\begin\{align\*\} & \\vdash \\forall x\. x = x & \\\\& \\vdash \\operatorname\{Prv\}\(\\forall x\. x = x\$ %20&%0A\\&%20\vdash%20\forall%20x%20\operatorname{Prv}(\dot{x}%20=%20\dot{x})%20&%20\mbox{(converse%20Barcan%20formula)}%0A\\&%20\vdash%20\forall%20x%20\operatorname{Prv}(\operatorname{Sub}(\ulcorner%20x%20=%20x%20\urcorner,%20x))%20&%0A\\&%20\vdash%20\forall%20x%20\operatorname{Prv}(\operatorname{Sub}(\ulcorner%20x%20=%20y%20\urcorner,%20x,%20x))%20&%0A\\&%20\vdash%20\forall%20x,%20y%20(%20x%20=%20y%20\to%20\operatorname{Prv}(\operatorname{Sub}(\ulcorner%20x%20=%20y%20\urcorner,%20x,%20y)))%20&%0A\\&%20\vdash%20\forall%20x,%20y%20(x%20=%20y%20\to%20\operatorname{Prv}(\dot{x}%20=%20\dot{y}))%20&%0A\end{align*})

$\\begin\{align\*\} & \\vdash \\forall z \\operatorname\{Prv\}\(\\operatorname\{Sub\}\(\\ulcorner z = z \\urcorner, z\$ )%0A\\&%20\vdash%20\forall%20x,y%20\operatorname{Prv}(\operatorname{Sub}(\ulcorner%20z%20=%20z%20\urcorner,%20x%20+%20y))%0A\\&%20\vdash%20\forall%20x,y%20\operatorname{Prv}(\operatorname{Concat}(\operatorname{Sub}(\ulcorner%20z%20\urcorner,%20x%20+%20y),%20\ulcorner%20=%20\urcorner,%20\operatorname{Sub}(\ulcorner%20z%20\urcorner,%20x%20+%20y))%0A\end{align*})

$\\operatorname\{Concat\}$ is a recursive function such that $\\operatorname\{Concat\}\(\\ulcorner \\alpha \\urcorner, \\ulcorner \\beta \\urcorner, \\ulcorner \\gamma \\urcorner\$ %20=%20\ulcorner%20\alpha%20\beta%20\gamma%20\urcorner). Now by messing around with Gödel numbers and numerals, one can prove

$\\vdash \\forall x,y \\operatorname\{Sub\}\(\\ulcorner z \\urcorner, x \+ y\$ %20=%20\operatorname{Sub}(\ulcorner%20x%20+%20y%20\urcorner,%20x,%20y))

$\\begin\{align\*\} & \\vdash \\forall x,y \\operatorname\{Prv\}\(\\operatorname\{Concat\}\(\\operatorname\{Sub\}\(\\ulcorner z \\urcorner, x \+ y\$ ,%20\ulcorner%20=%20\urcorner,%20\operatorname{Sub}(\ulcorner%20x%20+%20y%20\urcorner,%20x,%20y)))%0A\\&%20\vdash%20\forall%20x,y%20\operatorname{Prv}(\dot{x%20+%20y}%20=%20\dot{x}%20+%20\dot{y})%0A\end{align*})

(d) We proceed by induction on $y$ . The base case:

$\\begin\{align\*\} & \\vdash \\forall x\. 0 = x \\times 0 & \\\\& \\vdash \\operatorname\{Prv\}\( \\forall x\. 0 = x \\times 0\$ %20&%0A\\&%20\vdash%20\forall%20x%20\operatorname{Prv}(%200%20=%20\dot{x}%20\times%200)%20&%20\mbox{(converse%20Barcan%20formula)}%0A\\&%20\vdash%20\forall%20x%20\operatorname{Prv}(%20\dot{\overbrace{x%20\times%200}}%20=%20\dot{x}%20\times%200)%20&%0A\end{align*})

Now for the induction step, which implicitly uses part (a) in almost every step:

$\\begin\{align\*\} \\vdash \\forall x,y \\operatorname\{Prv\}\(\\dot\{\\overbrace\{xy\}\} = \\dot\{x\} \\times \\dot\{y\}\$ %20\to%20\operatorname{Prv}(\dot{\overbrace{x(y+1)}}%20&%20=%20\dot{\overbrace{xy%20+%20x}}%20&%0A\\&%20=%20\dot{\overbrace{xy}}%20+%20\dot{x}%20&%20\mbox{by%20(c)}%0A\\&%20=%20\dot{x}%20\times%20\dot{y}%20+%20\dot{x}%20&%0A\\&%20=%20\dot{x}%20\times%20(\dot{y}%20+%201)%20&%0A\\&%20=%20\dot{x}%20\times%20\dot{\overbrace{y%20+%201}}%20)%20&%20\mbox{%20by%20(c)}%0A\end{align*})

(e)

$\\begin\{align\*\} \\vdash \\forall x,y \( x > y & \\to \\exists z\. x = y \+ z \+ 1 & \\\\& \\to \\exists z \\operatorname\{Prv\}\( \\dot\{x\} = \\dot\{\\overbrace\{y \+ z \+ 1\}\}\$ %20&%20\mbox{by%20(b)}%0A\\&%20\to%20\exists%20z%20\operatorname{Prv}(%20\dot{x}%20=%20\dot{y}%20+%20\dot{z}%20+%201)%20&%20\mbox{by%20(c)}%0A\\&%20\to%20\exists%20z%20\operatorname{Prv}(%20\dot{x}%20%3E%20\dot{y})%20&%0A\\&%20\to%20\operatorname{Prv}(%20\dot{x}%20%3E%20\dot{y})%0A\end{align*})

Now we consider rational numbers. Every rational number $x$ can be written as

$x = \\frac\{x \- x'\}\{x'' \+ 1\}$

where $x, x',$ and $x''$ are natural numbers. So one way to represent a rational-valued variable in Peano arithmetic is with a triple $\(x, x', x''\$ ) of natural-valued variables. Two rational numbers are equal to each other when

$\\frac\{x \- x'\}\{x'' \+ 1\} = \\frac\{y \- y'\}\{y'' \+ 1\}$

Rearranging, we get $xy'' \+ x \+ y'x'' \+ y' = yx'' \+ y \+ x'y'' \+ x'$

This condition is expressible in Peano arithmetic, and is how we can express equality of two rationals.

We can prove a rational version of (b) using the natural version of (b) and repeated application of the natural versions of (c) and (d):

$\\begin\{align\*\} \\vdash \\forall x,x',x'',y,y',y'' \( & x \\times y'' \+ x \+ y' \\times x'' \+ y' = y \\times x'' \+ y \+x' \\times y'' \+ x' \\\\ & \\to \\operatorname\{Prv\}\(\\dot\{\\overbrace\{x \\times y'' \+ x \+ y' \\times x'' \+ y'\}\} = \\dot\{\\overbrace\{y \\times x'' \+ y \+x' \\times y'' \+ x'\}\}\$ %20&%20%0A\\%20&%20\to%20\operatorname{Prv}(\dot{x}%20\times%20\dot{y}''%20+%20\dot{x}%20+%20\dot{y}'%20\times%20\dot{x}''%20+%20\dot{y}'%20=%20\dot{y}%20\times%20\dot{x}''%20+%20\dot{y}%20+\dot{x}'%20\times%20\dot{y}''%20+%20\dot{x}')%20&%20%0A\end{align*})

With similar strategies one can prove rational versions of (a), (c), (d), and (e). Then we can prove the rational version of (f) directly:

(f)

$\\begin\{align\*\} \\vdash \\forall x,y\( x \\neq y &\\to x > y \\vee y > x & \\\\&\\to \\operatorname\{Prv\}\(\\dot\{x\} > \\dot\{y\}\$ %20\vee%20\operatorname{Prv}(\dot{y}%20%3E%20\dot{x})%20&%20\mbox{by%20(e)}%0A\\&\to%20\operatorname{Prv}(\dot{x}%20\neq%20\dot{y})%20\vee%20\operatorname{Prv}(\dot{y}%20\neq%20\dot{x})%20&%0A\\&\to%20\operatorname{Prv}(\dot{x}%20\neq%20\dot{y})%0A\end{align*})

$\\square$

[-]Nisan13y20

Fact 5 (Converse Barcan formula). For every formula $\\phi\(x\$ ) with one free variable,

$\\vdash \\operatorname\{Prv\}\( \\forall x \\phi\(x\$ )%20\to%20\forall%20x%20\operatorname{Prv}(\phi(\dot{x}))).

(The formula $\\operatorname\{Prv\}\(\\phi\(\\dot\{x\}\$ )) is shorthand for $\\operatorname\{Prv\}\(\\operatorname\{Sub\}\(\\ulcorner \\phi\(x\$ %20\urcorner,%20x))). Whenever a free variable appears inside the $\\operatorname\{Prv\}$ predicate, there's an implicit $\\operatorname\{Sub\}$ predicate there. I'm using a dot instead of an underline now.)

This fact is the converse of the Barcan formula in quantified provability logic. I'm not going to prove this, because it would be tedious and it would depend on the exact definition of $\\operatorname\{Prv\}$ , which I want to avoid in this post. Fact 5 is asserted without proof here, and Boolos[1] asserts it with barely more than no proof.

The converse Barcan formula implies some theorems of the form $\\vdash \\forall x \( \\phi\(x\$ %20\to%20\operatorname{Prv}(\phi(\dot{x})))). This doesn't work for all predicates $\\phi\(x\$ ) — for example, take $\\phi\(x\$ ) to be a sentence that is true for the natural numbers but not provable. Here are the theorems we will need:

Lemma 6.

(a) If $\\vdash \\forall x\_1, \\dots, x\_k \(P\(x\_1, \\dots, x\_k\$ %20\to%20Q(x_1,%20\dots,%20x_k))),

then $\\vdash \\forall x\_1, \\dots, x\_k \( \\operatorname\{Prv\}\(P\(\\dot\{x\}\_1, \\dots, \\dot\{x\}\_k\$ )%20\to%20\operatorname{Prv}(Q(\dot{x}_1,%20\dots,%20\dot{x}_k))))

(b) $\\vdash \\forall x,y\. \(x=y \\to \\operatorname\{Prv\}\(\\dot\{x\} = \\dot\{y\}\$ ))

(d) $\\vdash \\forall x,y \\operatorname\{Prv\}\(\\dot\{\\overbrace\{xy\}\} = \\dot\{x\} \\times \\dot\{y\}\$ )

(e) $\\vdash \\forall x,y \(x > y \\to \\operatorname\{Prv\}\(\\dot\{x\} > \\dot\{y\}\$ ))

(f) $\\vdash \\forall x,y \(x \\neq y \\to \\operatorname\{Prv\}\(\\dot\{x\} \\neq \\dot\{y\}\$ ))

You may want to skip the proof if you're mainly interested in how the decision agent works. Now we can give a proof of Proposition 3 that doesn't use Löb's theorem, and we can finally prove Conjecture 4 (now Proposition 4).

[1] Boolos, George. The Logic of Provability. Cambridge University Press: 1993. Ch. 17.

[-]gRR14y20

Continuing from here...

Is there a particular reason to define U as a constant? What if it was defined as a function, taking the agent function as its argument? For example:

U(#X) =
(a, 0) if X(#U,0) = C;
(b, 0) if X(#U,0) = D

Then A could be defined as:
A(#X, i) = y, such that there exists #z, such that z(#X, i)=y and forall #z' p_i(X(#z)) >= p_i(X(#z'))
[Some uniquness condition on y can be added for the cases where several actions may have equal maximal utility]

Then it should be provable that a>b => A(#U,0)=C and a A(#U,0)=D

This should also work with the toy PD. (But not with the real one - the agent's definition won't work because it is impossible to impersonate some other agent if you have to present your own Goedelian number).

[-]Nisan14y00

The problem with your definition of U(#X) is that it is not a recursive function. There is no recursive function that takes the Gödel number of a function and computes the value of that function. So there is no formula representing U, and so U doesn't have a Gödel number.

[-]gRR14y-20

There is no recursive function that takes the Gödel number of a function and computes the value of that function.

Huh? Of course, there is - the Universal Turing Machine. You were probably thinking of the halting problem, but here we can just assume every function halts.

[The agent idea was naive though. I was young and stupid when I wrote the grandfather comment :)]

[-]Nisan14y00

The agent described in the OP is definitely not a Turing machine that halts.

[-]gRR14y20

Hmm. The agent is a recursive function, so it is equivalent to a Turing machine that halts, no?

But I see your point. There is no simple formula, so if nothing else, it's inelegant.

[-]Nisan14y20

Whoops! I said in the OP that the precursor to A (before diagonalization) is a recursive function, but it's not. It's not computable because it has to check whether several propositions are theorems of Peano arithmetic, and also because of that existential quantifier in the definition of A. If A itself were recursive, then it would provably (in PA) cooperate or defect; but it cooperates or defects unprovably (in PA). I'll edit the OP to make it correct.

The rest of the post still works because all the functions are representable — they can be represented by formulas in arithmetic — even if they're not recursive. Thanks for bringing this to my attention.

EDIT: Oy, they're not even "representable" in the technical sense. They're only definable.

[-][anonymous]14y00

Continuing from here...

Is there a particular reason to define U as a constant? What if it was defined as a function, taking the agent function as its argument? For example:

U(#X) =
(a, 0) if X(#U, 0) = C;
(b, 0) if X(#U, 0) = D

Then it should be provable that a>b => A(#U,0)=C and a A(#U,0)=D

[This comment is no longer endorsed by its author]Reply

Moderation Log

More from Nisan

Curated and popular this week

34Comments

Comment Permalink

Nisan13y50

Proof of Proposition 3 (without using Löb's theorem). This proof uses Lemma 6.

First, notice that

$\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_0%20=%20C%20\to)

Similarly,

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_1%20=%20C%20\to%20A_0%20=%20C)

$PA \+ \\operatorname\{Con\}\(\\operatorname\{PA\} \+ \\operatorname\{Con\}\(\\operatorname\{PA\}\$ )%20\vdash%20A_0%20=%20A_1)

$\\square$

See in context

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()$ , a $0$ -ary function¹ that outputs an ordered pair $(a,b) \in \mathbb{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 \mathbb{N}$ is some sort of indexical information.

We want to define our agent such that

$A(\ulcorner \chi \urcorner,i) = \left\{ \begin{array}{ll}D & \mbox{if } \vdash A(\ulcorner \chi \urcorner, \underline{i}) = C \mbox{; else}\\C & \mbox{if } \vdash A(\ulcorner \chi \urcorner, \underline{i}) = D \mbox{; else}\\C & \mbox{if } \exists a,b ( \vdash ( A(\ulcorner \chi \urcorner,\underline{i}) = C \to \pi_{\underline{i}}(\chi()) = \underline{a})\\ & \mbox{\quad} \wedge \mbox{\quad} (A(\ulcorner \chi \urcorner,\underline{i}) = D \to \pi_{\underline{i}}(\chi()) = \underline{b} ))\\ & \mbox{\quad} \wedge \mbox{\quad}a > b \mbox{; else}\\ D &\end{array} \right.$

( $\ulcorner \omega \urcorner$ denotes the Gödel number of $\omega$ . $\vdash \omega$ means that $\omega$ is provable in Peano arithmetic. $\underline{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 $\phi$ as follows:

$\phi(\ulcorner \chi \urcorner,i,\ulcorner \psi \urcorner) = \left\{ \begin{array}{ll}D & \mbox{if } \vdash \psi(\ulcorner \chi \urcorner, \underline{i}) = C \mbox{; else}\\C & \mbox{if } \vdash \psi(\ulcorner \chi \urcorner, \underline{i}) = D \mbox{; else}\\C & \mbox{if } \exists a,b ( \vdash ( \psi(\ulcorner \chi \urcorner,\underline{i}) = C \to \pi_{\underline{i}}(\chi()) = \underline{a})\\ & \mbox{\quad} \wedge \mbox{\quad} (\psi(\ulcorner \chi \urcorner,\underline{i}) = D \to \pi_{\underline{i}}(\chi()) = \underline{b} ))\\ & \mbox{\quad} \wedge \mbox{\quad}a > b \mbox{; else}\\ D &\end{array} \right.$

This function can be defined by a formula. Then the diagonal lemma gives us a formula $A$ such that $\vdash A(x,i) = \phi(x,i,\ulcorner A \urcorner)$ .

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$ ,

$\vdash \operatorname{Prv}( A(\ulcorner \chi \urcorner, \underline{i}) = C) \to \neg \operatorname{Con}(\operatorname{PA})$
$\vdash \neg \operatorname{Con}(\operatorname{PA}) \to A(\ulcorner \chi \urcorner, \underline{i}) = D$
$\vdash \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i})=D) \to \neg\operatorname{Con}(\operatorname{PA}+\operatorname{Con}(\operatorname{PA}))$
$\vdash \operatorname{Con}(\operatorname{PA}) \wedge \neg\operatorname{Con}(\operatorname{PA}+\operatorname{Con}(\operatorname{PA})) \to A(\ulcorner \chi \urcorner,\underline{i}) = C$

( $\operatorname{Prv}$ is a binary-valued function such that $\operatorname{Prv}(\ulcorner \omega \urcorner)$ is true exactly when there is a proof of $\omega$ in Peano arithmetic. For brevity we write $\operatorname{Prv}(\omega)$ instead. $\operatorname{Con}(\operatorname{PA}+\operatorname{Con}(\operatorname{PA}))$ 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{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) & \to A(\ulcorner \chi \urcorner,i) = D &\end{align*}$

$\begin{align*}\quad\quad \vdash \operatorname{Prv}(\operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C)) & \to \operatorname{Prv}(A(\ulcorner \chi \urcorner,i) = D) &\end{align*}$
$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) & \to \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) \wedge \operatorname{Prv}(\operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C)) &\\& \to \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) \wedge \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) &\\& \to \neg \operatorname{Con}(\operatorname{PA}) &\end{align*}$

(2) By the principle of explosion,

$\begin{align*}\quad\quad \vdash \neg \operatorname{Con}(\operatorname{PA}) & \to \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) &\\ & \to A(\ulcorner \chi \urcorner,\underline{i}) = D &\end{align*}$

(3) By the definition of $A$ ,

$\begin{align*}\quad\quad \vdash \neg \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) \wedge \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) & \to A(\ulcorner \chi \urcorner,\underline{i}) = C &\end{align*}$
$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) & \to \biggl( \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) \wedge \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) \biggr) \vee A(\ulcorner \chi \urcorner,\underline{i}) = C &\\& \to \neg \operatorname{Con}(\operatorname{PA}) \vee A(\ulcorner \chi \urcorner,\underline{i}) = C\end{align*}$
$\begin{align*}\quad\quad \vdash \operatorname{Prv}(\operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D)) & \to \operatorname{Prv} \biggl( \neg\operatorname{Con}(\operatorname{PA}) \vee A(\ulcorner \chi \urcorner,\underline{i}) = C \biggr) &\end{align*}$
$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) & \to \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) \wedge \operatorname{Prv}(\operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D)) &\\& \to \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) \wedge \operatorname{Prv} \biggl(\neg \operatorname{Con}(\operatorname{PA}) \vee A(\ulcorner \chi \urcorner,\underline{i}) = C \biggr) &\\& \to \operatorname{Prv} \biggl( A(\ulcorner \chi \urcorner,\underline{i}) = D \wedge \biggl(\neg\operatorname{Con}(\operatorname{PA}) \vee A(\ulcorner \chi \urcorner,\underline{i}) = C \biggr) \biggr) &\\& \to \operatorname{Prv}(\neg\operatorname{Con}(\operatorname{PA})) &\\& \to \neg\operatorname{Con}(PA + \operatorname{Con}(\operatorname{PA})) &\end{align*}$

(4)

$\begin{align*}\quad\quad \vdash \neg\operatorname{Con}(\operatorname{PA} + \operatorname{Con}(\operatorname{PA})) & \to \operatorname{Prv}(\neg\operatorname{Con}(\operatorname{PA})) &\\& \to \operatorname{Prv}(\operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C)) &\\& \to \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) &\end{align*}$
$\begin{align*}\quad\quad \vdash \operatorname{Con}(\operatorname{PA}) \wedge \neg\operatorname{Con}(\operatorname{PA} + \operatorname{Con}(\operatorname{PA})) & \to \operatorname{Con}(\operatorname{PA}) \wedge \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) &\\& \to \neg\operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = C) \wedge \operatorname{Prv}(A(\ulcorner \chi \urcorner,\underline{i}) = D) &\\& \to A(\ulcorner \chi \urcorner,\underline{i}) = C &\end{align*}$

$\square$

If we assume consistency of $\operatorname{PA} + \operatorname{Con}(\operatorname{PA})$ (which entails consistency of $\operatorname{PA}$ ), then parts (1) and (3) of Lemma 1 tell us that for any $i$ , $\nvdash A(\ulcorner \chi \urcorner,\underline{i}) = C$ and $\nvdash A(\ulcorner \chi \urcorner,\underline{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 \mathbb{Q}$ and suppose

$U() = \left\{ \begin{array}{ll}(\alpha, 0) & \mbox{\rm if } A(\ulcorner U \urcorner,0) = C\\ (\beta, 0) & \mbox{\rm if } A(\ulcorner U \urcorner,0) = D\end{array} \right.$

Assume consistency of $\operatorname{PA}+\operatorname{Con}(\operatorname{PA})$ . Then $A(\ulcorner U \urcorner,0) = C$ if and only if $\alpha > \beta$ .

Proof. If we assume consistency of $\operatorname{PA} + \operatorname{Con}(\operatorname{PA})$ , 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{align*}\quad\quad \vdash \biggl( A(\ulcorner U \urcorner,0) = C \to \pi_0 U() = \underline{\alpha} \biggr) \wedge \biggl( A(\ulcorner U \urcorner,0) = D \to \pi_0 U() = \underline{\beta} \biggr) &&\end{align*}$

Suppose $\alpha > \beta$ . Then clearly

$\begin{align*}\quad\quad \exists a,b \vdash \biggl( A(\ulcorner U \urcorner,0) = C \to \pi_0 U() = \underline{a} \biggr) \wedge \biggl( A(\ulcorner U \urcorner,0) = D \to \pi_0 U() = \underline{b} \biggr) \wedge a > b &&\end{align*}$

So $A(\ulcorner U \urcorner,0) = C$ .

As for the converse: We have $\vdash (A(\ulcorner U \urcorner,0) = C \to \pi_0 U() = \underline{\alpha})$ . If also

$\begin{align*}\quad\quad \vdash (A(\ulcorner U \urcorner,0) = C \to \pi_0 U() = \underline{a}) &&\end{align*}$

and $a \neq \alpha$ , then $\vdash(A(\ulcorner U \urcorner,0) = D)$ . By Lemma 1(3) and consistency of $\operatorname{PA} + \operatorname{Con}(\operatorname{PA})$ , this cannot happen. So

$\begin{align*}\quad\quad \nvdash (A(\ulcorner U \urcorner,0) = C \to \pi_0 U() = \underline{a}) &&\end{align*}$

Similarly, we have

$\begin{align*}\quad\quad \nvdash (A(\ulcorner U \urcorner,0) = D \to \pi_0 U() = \underline{b}) &&\end{align*}$

for all $b \neq \beta$ . So

$\begin{align*}\quad\quad \nexists a,b \vdash(A(\ulcorner U \urcorner,0) = C \to \pi_0 U() = \underline{a}) \wedge (A(\ulcorner U \urcorner,0) = D \to \pi_0 U() = \underline{b}) \wedge a>b &&\end{align*}$

So the agent doesn't decide that $C$ is optimal, and $A(\ulcorner U \urcorner,0) = D$ .

$\square$

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

Proposition 3. Let

$U() = \left\{ \begin{array}{ll}(1,1) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=C \wedge A(\ulcorner U \urcorner,1)=C\\ (-1,2) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=C \wedge A(\ulcorner U \urcorner,1)=D\\ (2,-1) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=D \wedge A(\ulcorner U \urcorner,1)=C\\ (0,0) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=D \wedge A(\ulcorner U \urcorner,1)=D\end{array} \right.$

Then, assuming consistency of $\operatorname{PA} + \operatorname{Con}(\operatorname{PA})$ , we have $A(\ulcorner U \urcorner,0) = C = A(\ulcorner U \urcorner,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{align*}\quad\quad \vdash A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1) & \to \biggl(\biggl( A(\ulcorner U \urcorner,0)=C \to \pi_0 U() = 1 \biggr) \wedge \biggl( A(\ulcorner U \urcorner,0)=D \to \pi_0 U() = 0 \biggr)\biggr) &\end{align*}$
$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1)) & \to \exists a,b. \operatorname{Prv}\biggl((A(\ulcorner U \urcorner,0)=C \to \pi_0 U() = \underline{a}) &\\& \quad\quad \wedge (A(\ulcorner U \urcorner,0)=D \to \pi_0 U() = \underline{b})\biggr) \wedge a > b &\end{align*}$
Looking at the definition of $A$ , we see that

$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1)) & \to \operatorname{Prv}(A(\ulcorner U \urcorner,0)=C) \vee \operatorname{Prv}(A(\ulcorner U \urcorner,0)=D) &\\&\quad\quad \vee A(\ulcorner U \urcorner,0)=C &\end{align*}$
By Lemma 1, (1) and (3),

$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1)) & \to \neg \operatorname{Con}(\operatorname{PA}) \vee \neg \operatorname{Con}(\operatorname{PA} + \operatorname{Con}(\operatorname{PA})) \vee A(\ulcorner U \urcorner,0)=C &\end{align*}$

Similarly,

$\begin{align*} \label{ast}(*)\quad \vdash \operatorname{Prv}(A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1)) & \to \neg \operatorname{Con}(\operatorname{PA}) \vee \biggl(\operatorname{Con}(\operatorname{PA}) \wedge \neg \operatorname{Con}(\operatorname{PA} + \operatorname{Con}(\operatorname{PA})) \biggr) &\\&\quad\quad \vee A(\ulcorner U \urcorner,0)=C=A(\ulcorner U \urcorner,1) &\end{align*}$

Applying Lemma 1(2) and (4),

$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1)) & \to A(\ulcorner U \urcorner,0) = D = A(\ulcorner U \urcorner,1) &\\&\quad\quad \vee A(\ulcorner U \urcorner,0) = C = A(\ulcorner U \urcorner,1) &\\&\quad\quad \vee A(\ulcorner U \urcorner,0)=C=A(\ulcorner U \urcorner,1) &\\& \to A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1) &\end{align*}$

By Löb's theorem,

$\begin{align*}\quad\quad \vdash A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1) &&\end{align*}$
$\begin{align*}\quad\quad \vdash \operatorname{Prv}(A(\ulcorner U \urcorner,0) = A(\ulcorner U \urcorner,1)) &&\end{align*}$

By $(*)$ , we have

$\begin{align*}\quad\quad \vdash \neg \operatorname{Con}(\operatorname{PA}) \vee \biggl(\operatorname{Con}(\operatorname{PA}) \wedge \neg \operatorname{Con}(\operatorname{PA} + \operatorname{Con}(\operatorname{PA})) \biggr) \vee A(\ulcorner U \urcorner,0)=C=A(\ulcorner U \urcorner,1) &&\end{align*}$

So, assuming $\operatorname{Con}(\operatorname{PA} + \operatorname{Con}(\operatorname{PA}))$ , we conclude that $A(\ulcorner U \urcorner,0)=C=A(\ulcorner U \urcorner,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\{ \begin{array}{ll}(0,0) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=C \wedge A(\ulcorner U \urcorner,1)=C\\ (2,-1) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=C \wedge A(\ulcorner U \urcorner,1)=D\\ (-1,2) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=D \wedge A(\ulcorner U \urcorner,1)=C\\ (1,1) & \mbox{\rm if } A(\ulcorner U \urcorner,0)=D \wedge A(\ulcorner U \urcorner,1)=D\end{array} \right.$

Then, assuming consistency of $\operatorname{PA} + \operatorname{Con}(\operatorname{PA})$ , we have $A(\ulcorner U \urcorner,0) = D = A(\ulcorner U \urcorner,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{align*} \quad\quad \vdash \exists a,b & (A(\ulcorner U\urcorner,\underline{i})=C \to \pi_{\underline{i}} U() = a) \\& \wedge ( A(\ulcorner U \urcorner,\underline{i})=D \to \pi_{\underline{i}} U() = b) \\& \wedge a > b \end{align*}$

? 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 $\phi(x_1, \dots, x_k, y)$ with $k+1$ free variables such that $\vdash \exists y. \phi(x_1, \dots, x_k, y)$ and $\vdash \phi(x_1, \dots, x_k, y) \wedge \phi(x_1, \dots, x_k, y') \to y = y'$ . 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 $\phi$ that defines it.