These notes are from discussions with Kuba Stechly at the Summer Fellows Program, on the topic of infinite modal combat, previously discussed here. In that post, Victoria proved that non-wellfounded infinite modal agents called ProcrastinationBots cooperate with each other.

We extend these results to a more general case and then show how the most general case breaks. We also show that there exist polynomial time computable bots that are not equivalent to standard bots.

The Trivial Case

Suppose we build an infinite family of modal agents ${\text{InfiniTeamBot}}_1,{\text{InfiniTeamBot}}_2,\dots$ with ${\text{InfiniTeamBot}}_i\left(X\right):=\Psi (X,{\text{InfiniTeamBot}}_{a_{i1}},{\text{InfiniTeamBot}}_{a_{i2}},\dots ,{\text{InfiniTeamBot}}_{a_{ik}})$, where $\Psi$ is a fully modalized formula ($\Psi$ may also refer to other modal agents); for example, the ${\text{ProcrastinationBot}}_N$s from the earlier post are of this form. Can the results of modal combat with such agents be computed?

For comparison, consider ${\text{InfiniTeamBot}}_0\left(X\right):=\Psi (X,{\text{InfiniTeamBot}}_0,\dots ,{\text{InfiniTeamBot}}_0)$, which is a finite modal agent.

If we look at these agents in GL’s Kripke frames, we find that ${\text{InfiniTeamBot}}_i\left(X\right)={\text{InfiniTeamBot}}_0\left(X\right)$ and $X\left({\text{InfiniTeamBot}}_i\right)=X\left({\text{InfiniTeamBot}}_0\right)$ in every frame, which suggests the bots are just equivalent to ${\text{InfiniTeamBot}}_0$. To show that the bots are is true, we can use Löb’s Theorem in PA: if we had $\square \left(\forall i\right({\text{InfiniTeamBot}}_i\left(X\right)\leftrightarrow {\text{InfiniTeamBot}}_0\left(X\right)\wedge X\left({\text{InfiniTeamBot}}_i\right)\leftrightarrow X\left({\text{InfiniTeamBot}}_0\right)\left)\right)$ then PA could prove $\forall i\left({\text{InfiniTeamBot}}_i\right(X)\leftrightarrow {\text{InfiniTeamBot}}_0(X)\wedge X({\text{InfiniTeamBot}}_i)\leftrightarrow X({\text{InfiniTeamBot}}_0\left)\right)$, so Löb’s Theorem implies all of these bots are equivalent to ${\text{InfiniTeamBot}}_0$.

(We’re eliding the way the bots are actually specified in PA; the fixed point construction in the previous post can be extended to our setting.)

Some Impossibility Results

We wish to extend to allow other, more interesting bots. However, if we allow arbitrary infinite bots, then we run into some issues. We now prove some impossibility results to start delineating the edge beyond which bots are not easily computable.

def CollatzBot_N(X):
  if N == 1:
    return C
  if N is even and [] X(CollatzBot_{N/2})=D:
    return D
  if N is odd and [] X(CollatzBot_{3N+1})=D:
    return D
  return C

def ProveCollatzBot_N(X):
  if []CollatzBot_N(X) = C:
    if []ProveCollatzBot_{N+1}(X) = C:
      return C
  return D

ProveCollatzBot${}_1$ only cooperates with itself if it can prove the Collatz conjecture is true. Since we don’t know the answer to whether it is or is not true (and it might even be independent of PA), we cannot actually calculate what ProveCollatzBot${}_1$ will do, so we wish to reject bots of this form from our framework.

One natural thing to want to build is a true TitForTatBot, one that will see what its opponent does in every Kripke frame and defect only if the opponent defected in the previous frame (or, at least, defect a limited number of times for each defection it receives). More generally, it’s desirable to build a bot that will eventually just cooperate against an opponent that eventually just cooperates, but not otherwise. (We could call this “TailBot”, “BestBot” or “JusticeBot”). This seems like the holy grail of modal combat. And, as the superlative suggests, this can’t be done.

Suppose it could - then we could build “EpimenidesBot”, whose defection condition is exactly TailBot’s cooperation condition. Pitting two EpimenidesBots against each other, we’ll see that they can never stabilize on cooperation or defection, so the combat can’t be decided. (If we’re imaginative we can see what happens in $PA+\omega$ and beyond; this probably reduces to a competition between the combatants and the decision algorithm over access to higher ordinals.)

Discussion / Future work

However, we can construct polynomial time computable bots that are extensionally different from standard finite bots. An example is EvenBot, which only cooperates with X if X cooperated first on an even frame. (Note that there are some conditions on X. EvenBot is not yet polished to do exactly what we claim. However, by looking at its performance versus various WaitCooperateBots, we can see that it performs differently than any possible standard bot. Also, EvenBot might really be OddBot, depending on notational convention.) We can also modify EvenBot to only cooperate if someone cooperates first on a prime frame.

def EvenBot_N(X):
  if [2N]F:
    return C
  if [2N+1]F:
    if [](X(EvenBot_N)=C or [2N-1]F):
      return C
    return D
  if []EvenBot_N(X)=C or
      (<>(EvenBot_(N)(X)=C and <>EvenBot_(N)(X)=D)):
    return C
  if []EvenBot_{N+1}(X)=C or
      (<>(EvenBot_{N+1}(X)=C and <>EvenBot_{N+1}(X)=D)): 
    return C
  return D

We don’t yet know whether there is a natural extension to the existing modal combat framework that allows for novel infinite bots like EvenBot without admitting difficult-to-compute bots like CollatzBot; but this may be interesting to investigate further.