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.
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.