If I follow what you mean, we can derive:
□(□A)→□B→□(□B)→□A
So there’s a Löbian proof, in which the provability is self-fulfilling. But this isn’t sufficient to avoid this kind of proof.
(Aside on why I don’t like the Löbian method: I moreso want the agents to be doing “correct” counterfactual reasoning about how their actions affect their opponent, and to cooperate because they see that mutual cooperation is possible and then choose it. The Löbian proof style isn’t a good model of that, imo.)
So, ideally you would like to assume only
□A→B
□B→A
and conclude A and B ?
If I follow what you mean, we can derive: □(□A)→□B→□(□B)→□A
So there’s a Löbian proof, in which the provability is self-fulfilling. But this isn’t sufficient to avoid this kind of proof.
(Aside on why I don’t like the Löbian method: I moreso want the agents to be doing “correct” counterfactual reasoning about how their actions affect their opponent, and to cooperate because they see that mutual cooperation is possible and then choose it. The Löbian proof style isn’t a good model of that, imo.)