Description du poste
The simplest interesting player in MIRI's provability bot prisoner's dilemma tournament was FairBot, which cooperates if it can prove its opponent cooperates.
It cooperates with another FairBot despite the apparent infinite regress, by Löb's theorem (some might say magic).
A related line of work was how to represent statements like "if I take this action, it will have that consequence" in provability logic.
For example there's these old slides by Vladimir Slepnev that I came across on the MIRI website.
A post by James Payor brings these together.
Well, maybe he didn't think of it like that.
But I think of it as alternate FairBots, which look like different formalizations of the consequence of an action.
Like, a bot that cooperates if and only if it can prove its cooperation results in its opponent's cooperation.
Such bots are equivalent to FairBot conditional on Löb's theorem, but the idea was to cut off the infinite regress without Löb's theorem.
I'm writing this post to share some formula manipulations, simple substitutions really.
It turns out it's very easy to see that these bots are equivalent, assuming Löb's theorem.
But more importantly, we can clearly see the machinery by which Löb's theorem cuts off the infinite regress, and how these alternate formulations accomplish the same thing.
Substituting in the FairBot formula
I'll start by just showing you the substitutions I have in mind.
FairBot:
mjx-math {
display: inline-block;
text-align: left;
line-height: 0;
text-indent: 0;
font-style: normal;
font-weight: normal;
font-size: 100%;
font-size-adjust: none;
letter-spacing: normal;
border-collapse: collapse;
word-wrap: normal;
word-spacing: normal;
white-space: nowrap;
direction: ltr;
padding: 1px 0;
}
mjx-container[jax="CHTML"][display="true"] {
display: block;
text-align: center;
margin: 1em 0;
}
mjx-container[jax="CHTML"][display="true"][width="full"] {
display: flex;
}
mjx-container[jax="CHTML"][display="true"]