I'm confused; does your definition of imply that it evaluates those conditionals in order? If so, consider the example of and DefectBot. The you construct will cooperate in world 0, and thus it will not get the cooperation of , while does. What am I missing?
Your confusion was justified. It was wrong before. I think it is fixed now.
The conditionals are checked in order. As it is written now, none of the conditionals except the last one should trigger until world .
The first only triggers against , the second only triggers against and the third only triggers against .
Post 2 in in Modal SAT series. In this post, we show that SC Modal SAT is equivalent to Modal SAT.
For this, we need just need to prove the following theorem:
Theorem: If there exists a modal agent M such that Ci cooperates with M for each Ci∈C and such that M defects against Di for each Di∈D, then there exists an M′ which satisfies the above properties and cooperates with itself.
Proof: Let n be greater than the total number of boxes in agents in C and D. Consider the agents Xn and Xn+1 defined by Xi(B)=C↔¬□i⊥.
We define M′ by
M′(B)=C if ¬□n+1⊥ and □(¬□n⊥→B(CooperateBot)=C) and ¬□(¬□n−1⊥→B(CooperateBot)=C)
M′(B)=D if ¬□n+2⊥ and □(¬□n+1⊥→B(CooperateBot)=C) and ¬□(¬□n⊥→B(CooperateBot)=C)
M′(B)=C if ¬□n+3⊥ and □(¬□n+1⊥→B(Xn)=C) and □(¬□n+2⊥→B(Xn+1)=D)
M′(B)=M(B) otherwise
Rule 1 says that M′ cooperates with Xn, rule 2 says that M′ defects against Xn+1, and rule 3 says that M′ cooperates with anyone who (provably assuming ¬□n+1⊥) cooperates with Xn and (provably assuming ¬□n+2⊥)defects against Xn+1. Thus, M′ cooperates with itself.
For any bot B with fewer than n boxes, the conditions of 1, 2, and 3 are all false. For 1 and 2, this is because the actions of such bots against CoopearteBot stabilize by the time you assume ¬□n−1⊥. For 3, this is because these bots cannot distinguish between Xn and Xn+1.
Therefore M′ behaves the same as M on all inputs with fewer than n boxes, so M′ cooperates with every bot in C and defects against every bot in D.
□
Note that I was lazy here, and took way more longer to cooperate with myself than I had to. In principle, if there are only k bots that I need to consider (including bots I need to consider because they are referenced by bots I care about), then regardless of how many boxes are in each bot, It should be possible to achieve self cooperation within 2log2k worlds of the Kripke frame. That is, log2k worlds to identify a single bot that is distinguishable from all other bots, and another log2k worlds to ensure that the actions of M′ differ on that bot from all other bots, so that M′ can identify itself without changing its behavior against any other bot.
EDIT: Actually, I think logk + a small constant should suffice, but it does not matter much.