I finally had time to read this, and I must say, that’s an extremely creative premise. I’m puzzled by the proof of theorem 3.1, however. It claims “By inspection of FairBot, PA⊢◻(FB(FB) = C)-->FB(FB=C).”
However, by inspection of fairbot, the antecedent of the conditional should be FB(FB) = C rather than ◻(FB(FB) = C). The code says “if it’s a theorem of PA that X cooperates with me, then cooperate.” It doesn’t say “if it’s a theorem of PA that it’s provable in PA that X cooperates with me, then cooperate.” So I don’t believe you can appeal to Lob’s theorem in this case.
.
They applied Lob’s theorem correctly. “X is a theorem of PA” and “X is provable in PA” mean the same thing, and both are represented by ◻X. The antecedent of “if it’s a theorem of PA that it’s provable in PA that FB cooperates with me, then cooperate” would be represented as ◻(◻(FB(FB) = C)), but this never appears either in the code or in the antecedent for Lob’s theorem. “FB(FB) = C” on its own, without the box, would mean it is true that fairbot cooperates with itself, not that PA can prove that fairbot cooperates with itself.
I finally had time to read this, and I must say, that’s an extremely creative premise. I’m puzzled by the proof of theorem 3.1, however. It claims “By inspection of FairBot, PA⊢◻(FB(FB) = C)-->FB(FB=C).”
However, by inspection of fairbot, the antecedent of the conditional should be FB(FB) = C rather than ◻(FB(FB) = C). The code says “if it’s a theorem of PA that X cooperates with me, then cooperate.” It doesn’t say “if it’s a theorem of PA that it’s provable in PA that X cooperates with me, then cooperate.” So I don’t believe you can appeal to Lob’s theorem in this case. .
They applied Lob’s theorem correctly. “X is a theorem of PA” and “X is provable in PA” mean the same thing, and both are represented by ◻X. The antecedent of “if it’s a theorem of PA that it’s provable in PA that FB cooperates with me, then cooperate” would be represented as ◻(◻(FB(FB) = C)), but this never appears either in the code or in the antecedent for Lob’s theorem. “FB(FB) = C” on its own, without the box, would mean it is true that fairbot cooperates with itself, not that PA can prove that fairbot cooperates with itself.