Per AlexMennen, I’d rename CarefulBot-as-formulated to something like BoldBot, and apply the name CarefulBot to “swerve unless it’s proven the other bot swerves.”
I think (I’m an amateur here, full disclosure; could be mistakes) we can capture some of the behavior you’re interested in by considering bots with different levels of proof system. So e.g. CBn swerves unless it can prove, using PA+n, that the opponent swerves.
Then we see that for n > m, CBn(CBm) = D. Proof: Suppose CBn doesn’t swerve. In PA+n, it is an axiom that provability in PA+m implies truth. Therefore PA+m cannot prove that CBn swerves. In a contest between CarefulBots, the stronger proof system wins.
Now consider BoldBot. We can see that BBn does not swerve against BBn, because by symmetry both agents prove the same thing; and if they both proved their opponent does not swerve, they would both swerve, and both have proven a falsehood.
Analyzing BBn vs. BBm is proving difficult, but I’m going to try a bit more.
Actually, I notice that BBn vs. BBm is isomorphic to CBn vs. CBm! Just interchange ‘swerve’ and ‘don’t swerve’ in the specification of one to convert it into the other. This implies that BBn swerves against BBm, and BBm does not swerve, if my proof about CBn vs. CBm is valid. I’m no longer so sure it is...
Per AlexMennen, I’d rename CarefulBot-as-formulated to something like BoldBot, and apply the name CarefulBot to “swerve unless it’s proven the other bot swerves.”
I think (I’m an amateur here, full disclosure; could be mistakes) we can capture some of the behavior you’re interested in by considering bots with different levels of proof system. So e.g. CBn swerves unless it can prove, using PA+n, that the opponent swerves.
Then we see that for n > m, CBn(CBm) = D. Proof: Suppose CBn doesn’t swerve. In PA+n, it is an axiom that provability in PA+m implies truth. Therefore PA+m cannot prove that CBn swerves. In a contest between CarefulBots, the stronger proof system wins.
Now consider BoldBot. We can see that BBn does not swerve against BBn, because by symmetry both agents prove the same thing; and if they both proved their opponent does not swerve, they would both swerve, and both have proven a falsehood.
Analyzing BBn vs. BBm is proving difficult, but I’m going to try a bit more.
Actually, I notice that BBn vs. BBm is isomorphic to CBn vs. CBm! Just interchange ‘swerve’ and ‘don’t swerve’ in the specification of one to convert it into the other. This implies that BBn swerves against BBm, and BBm does not swerve, if my proof about CBn vs. CBm is valid. I’m no longer so sure it is...