The modal combat paper defined FairBot. If I'm FairBot, I cooperate in the prisoner's dilemma if and only if there's a proof that you cooperate:
F(X) ↔ □X(F)
I cooperate with a replica of myself, because that's a Henkin sentence, asserting its own provability:
F(F) ↔ □F(F)
Replacing F(F) with H:
H ↔ □H
And that's true by Löb’s theorem.
Andrew Critch made a post suggesting a different way to prove self-cooperation, from a different condition. Instead of Löb’s theorem, he used what he called Payor's lemma.
I made a post applying this to modal combat by defining what I called a Payorian FairBot:
F'(X) ↔ □(□F'(X) → X(F'))
Playing this against its replica:
F'(F') ↔ □(□F'(F') → F'(F'))
Replacing F'(F') with P:
P ↔ □(□P → P)
And that's true by Payor's lemma.
Okay, here's my question. Are these actually different bots? Or do we have F(X) ↔ F'(X) for all X?
They are the same.
MIRI's proof-based prisoner's dilemma tournament defined agents encoded as formulas of Peano arithmetic (PA) with one free variable. means t
