The interesting thing about this—beyond showing that going probabilistic allows the handshake to work with somewhat unreliable bots—is that proving ⊢□wE rather than ⊢E is a lot different. With ⊢E, we’re like “And so Peano arithmetic (or whatever) proves they cooperate! We think Peano arithmetic is accurate about such matters, so, they actually cooperate.”
With the conclusion ⊢□wE we’re more like “So if the agent’s probability estimates are any good, we should also expect them to cooperate” or something like that. The connection to them actually cooperating is looser.
The interesting thing about this—beyond showing that going probabilistic allows the handshake to work with somewhat unreliable bots—is that proving ⊢□wE rather than ⊢E is a lot different. With ⊢E, we’re like “And so Peano arithmetic (or whatever) proves they cooperate! We think Peano arithmetic is accurate about such matters, so, they actually cooperate.”
With the conclusion ⊢□wE we’re more like “So if the agent’s probability estimates are any good, we should also expect them to cooperate” or something like that. The connection to them actually cooperating is looser.