A point of confusion: is it enough to prove that A→□B? What about A→B? I’m not sure I can say this well, but here goes:
We might not be able to prove A→B in the theory, or even that ¬□⊥ (which would mean “there are no proofs of inconsistency”). But if we believe our theory is sound, we believe that it can’t show that a copy of itself proves something false.
So A→□B tells us that if A is true, the theory would show that a copy of itself proves B is true. And this is enough to convince us that we can’t simultaneously have A true and B false.
This is cool (and fwiw to other readers) correct. I must reflect on what it means for real world cooperation… I especially like the
A <-> []X → [][]X <-> []A
trick.
Also, here’s a proof that a bot A↔□(□A→B) is never exploited. It only cooperates when its partner B provably cooperates.
First, note that A→□A, i.e. if A cooperates it provably cooperates. (Proof sketch: A↔□X→□□X↔□A.)
Now we show that A→□B (i.e. if A chooses to cooperate, its partner is provably cooperating):
We get A→(□□A→□B) by distributing.
We get A→□□A by applying internal necessitation to A→□A.
By (1) and (2), A→□B.
(PS: we can strengthen this to A↔□B, by noticing that □B→□(□A→B)↔A.)
A point of confusion: is it enough to prove that A→□B? What about A→B? I’m not sure I can say this well, but here goes:
We might not be able to prove A→B in the theory, or even that ¬□⊥ (which would mean “there are no proofs of inconsistency”). But if we believe our theory is sound, we believe that it can’t show that a copy of itself proves something false.
So A→□B tells us that if A is true, the theory would show that a copy of itself proves B is true. And this is enough to convince us that we can’t simultaneously have A true and B false.
This is cool (and fwiw to other readers) correct. I must reflect on what it means for real world cooperation… I especially like the A <-> []X → [][]X <-> []A trick.