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
InfiniTeamBot1,InfiniTeamBot2,… with
InfiniTeamBoti(X):=Ψ(X,InfiniTeamBotai1,InfiniTeamBotai2,…,InfiniTeamBotaik),
where Ψ is a fully modalized formula (Ψ may also refer to
other modal agents); for example, the ProcrastinationBotNs
from the earlier post are of this form. Can the results of modal combat
with such agents be computed?

For comparison, consider
InfiniTeamBot0(X):=Ψ(X,InfiniTeamBot0,…,InfiniTeamBot0),
which is a finite modal agent.

If we look at these agents in GL’s Kripke frames, we find that
InfiniTeamBoti(X)=InfiniTeamBot0(X) and
X(InfiniTeamBoti)=X(InfiniTeamBot0) in every
frame, which suggests the bots are just equivalent to
InfiniTeamBot0. To show that the bots are is true, we can
use Löb’s Theorem in PA: if we had
□(∀i(InfiniTeamBoti(X)↔InfiniTeamBot0(X)∧X(InfiniTeamBoti)↔X(InfiniTeamBot0)))
then PA could prove
∀i(InfiniTeamBoti(X)↔InfiniTeamBot0(X)∧X(InfiniTeamBoti)↔X(InfiniTeamBot0)),
so Löb’s Theorem implies all of these bots are equivalent to
InfiniTeamBot0.

(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

ProveCollatzBot1 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 ProveCollatzBot1 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+ω 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.

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 InfiniTeamBot1,InfiniTeamBot2,… with InfiniTeamBoti(X):=Ψ(X,InfiniTeamBotai1,InfiniTeamBotai2,…,InfiniTeamBotaik), where Ψ is a fully modalized formula (Ψ may also refer to other modal agents); for example, the ProcrastinationBotNs from the earlier post are of this form. Can the results of modal combat with such agents be computed?

For comparison, consider InfiniTeamBot0(X):=Ψ(X,InfiniTeamBot0,…,InfiniTeamBot0), which is a finite modal agent.

If we look at these agents in GL’s Kripke frames, we find that InfiniTeamBoti(X)=InfiniTeamBot0(X) and X(InfiniTeamBoti)=X(InfiniTeamBot0) in every frame, which suggests the bots are just equivalent to InfiniTeamBot0. To show that the bots are is true, we can use Löb’s Theorem in PA: if we had □(∀i(InfiniTeamBoti(X)↔InfiniTeamBot0(X)∧X(InfiniTeamBoti)↔X(InfiniTeamBot0))) then PA could prove ∀i(InfiniTeamBoti(X)↔InfiniTeamBot0(X)∧X(InfiniTeamBoti)↔X(InfiniTeamBot0)), so Löb’s Theorem implies all of these bots are equivalent to InfiniTeamBot0.

(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.

ProveCollatzBot1 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 ProveCollatzBot1 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+ω 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.

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.