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:
where means that the bot cooperates, that its opponent cooperates.
For the first substitution, we'll need Löb's theorem and its trivial converse:
Substituting:
Then, substituting with the FairBot definition:
This is Payor's "Idea #1".
It's also what you would get by straightforwardly applying the formula in the Slepnev slides to formalize "I'll cooperate if that results in my opponent's cooperation".
To get that, we use this theorem of provability logic (by which I mean the system GL):
Using that instead of Löb's theorem, we obtain Idea #2 in the same way as Idea #1.
Cutting off the infinite regress
In this section, I'm going to consider the consequences of , that is, that the bot defects.
Assuming the other bot is also a FairBot, we would like this to result in some kind of contradiction, thus proving cooperation.
If I'm FairBot, it seems consistent that I defect because I can't prove you cooperate, but that's just because you defect because you can't prove I cooperate, because...
We'll start by describing this infinite regress in modal logic formulas instead of in English.
Then we'll see how Löb's theorem cuts it off, and how the alternate formulations accomplish the same thing.
FairBot's infinite regress
FairBot again:
Since we're asking "what if I defect?", we'll negate both sides:
Since the opponent is also a FairBot:
To see the infinite regress, let's get back to substituting.
Substituting out in the first formula using the second formula:
And we can keep going:
We defect on each other all the way down in these possible worlds, however deep we want to look.
Cutting it off with Löb's theorem
Well, let's look at the first substitution we did, using Löb's theorem:
Negating both sides:
I defect if... it's possible that you defect, even though there's a proof you cooperate?
I found this confusing.
But youzicha on Tumblr interpreted it as so: consider the last world in which you defect.
Of course, as we saw previously, there is no last world.
To see that mechanistically, we can try substituting, using the ordinary FairBot formulas ( and ):
The right-hand side can be refuted in provability logic (that is, its negation is a theorem of GL).
The contradicts the two worlds down.
We can't keep substituting forever like we did before; the chain stops here.
is equivalent to a falsehood, so we've proved cooperation.
Cooperation in Idea #1
Repeating Idea #1:
Negating both sides:
Actually I don't see it.
Really I want to get to the next one,
Cooperation in Idea #2
which was
Negating both sides,
I've previously called this condition "betrayal": I defect if it's possible that you betray me, that is, defect even though you can prove I cooperate.
That was in my post trying to walk through the reasoning in plain English.
Back to modal logic.
We only need one substitution with :
Again, the right-hand side is refutable; contradicts one world down.
Now I get that you can cut off infinite regresses with the contrapositive of Löb's theorem:
In provability logic with Löb's theorem, these reformulations simply follow from there.
Of course the point of the reformulations is that they don't require Löb's theorem.
It's like we "already used" Löb's theorem in rewriting the condition, and no longer need it to prove cooperation.
I don't know the ultimate significance of that.
But I've at least shared something of personal significance.
Once I learned why every question "bottoms out" in provability logic, I had to bring it back around to the first time I saw something like that.
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:
where
For the first substitution, we'll need Löb's theorem and its trivial converse:
Substituting:
Then, substituting with the FairBot definition:
This is Payor's "Idea #1". It's also what you would get by straightforwardly applying the formula in the Slepnev slides to formalize "I'll cooperate if that results in my opponent's cooperation".
What about Payor's "Idea #2", the subject of Critch's post? That says
To get that, we use this theorem of provability logic (by which I mean the system GL):
Using that instead of Löb's theorem, we obtain Idea #2 in the same way as Idea #1.
Cutting off the infinite regress
In this section, I'm going to consider the consequences of
If I'm FairBot, it seems consistent that I defect because I can't prove you cooperate, but that's just because you defect because you can't prove I cooperate, because...
We'll start by describing this infinite regress in modal logic formulas instead of in English. Then we'll see how Löb's theorem cuts it off, and how the alternate formulations accomplish the same thing.
FairBot's infinite regress
FairBot again:
Since we're asking "what if I defect?", we'll negate both sides:
Since the opponent is also a FairBot:
To see the infinite regress, let's get back to substituting. Substituting out
And we can keep going:
We defect on each other all the way down in these possible worlds, however deep we want to look.
Cutting it off with Löb's theorem
Well, let's look at the first substitution we did, using Löb's theorem:
Negating both sides:
I defect if... it's possible that you defect, even though there's a proof you cooperate?
I found this confusing. But youzicha on Tumblr interpreted it as so: consider the last world in which you defect. Of course, as we saw previously, there is no last world.
To see that mechanistically, we can try substituting, using the ordinary FairBot formulas (
The right-hand side can be refuted in provability logic (that is, its negation is a theorem of GL). The
Cooperation in Idea #1
Repeating Idea #1:
Negating both sides:
Actually I don't see it. Really I want to get to the next one,
Cooperation in Idea #2
which was
Negating both sides,
I've previously called this condition "betrayal": I defect if it's possible that you betray me, that is, defect even though you can prove I cooperate. That was in my post trying to walk through the reasoning in plain English.
Back to modal logic. We only need one substitution with
Again, the right-hand side is refutable;
Conclusion
Idea #2 was exciting to me because this "I imagine you imagining me" reasoning cuts off after just a few steps. It was my first hint that cooperation in provability logic might not be so mysterious.
Now I get that you can cut off infinite regresses with the contrapositive of Löb's theorem:
In provability logic with Löb's theorem, these reformulations simply follow from there.
Of course the point of the reformulations is that they don't require Löb's theorem. It's like we "already used" Löb's theorem in rewriting the condition, and no longer need it to prove cooperation.
I don't know the ultimate significance of that. But I've at least shared something of personal significance. Once I learned why every question "bottoms out" in provability logic, I had to bring it back around to the first time I saw something like that.