It looks like you’re investigating an angle that I can’t follow, but here’s my two cents re bounded agents:
My main idea to port this to the bounded setting is to have a bot that searches for increasingly long proofs, knowing that if it takes longer to find a proof then it is itself a bit harder to reason about.
We can instantiate this like:
Ak(B)↔∃i≤k.□i(□i+CAk(B)→B(Ak))
The idea is that if there is a short way to prove that the opponent B would cooperate back, then it takes just a constant C steps more to prove that we cooperate. So it doesn’t open us up to exploitation to assume that our own cooperation is provable in i+C steps.
The way in which this works at all is by cutting the loop at the point where the opponent is thinking about our own behaviour. This bot cuts it rather aggressively: it assumes that no matter the context, when B thinks about whether A cooperates, it’s provable that A does cooperate. (I think this isn’t great and can be improved to a weaker assumption that would lead to more potential cooperation.)
If you construct Bn similarly, I claim that Ak and Bn mutually cooperate if k and n are large enough, and mutually defect otherwise.
Similarly, I claim Ak can mutually cooperate with other bots like Bn(A)=□nA(Bn).
I’m working on it :) At this point what I think is true is the following:
If ShortProof(x \leftrightarrow LongProof(ShortProof(x) \to x)), then MediumProof(x).
Apologies that I haven’t written out calculations very precisely yet, but since you asked, that’s roughly where I’m at :)
It looks like you’re investigating an angle that I can’t follow, but here’s my two cents re bounded agents:
My main idea to port this to the bounded setting is to have a bot that searches for increasingly long proofs, knowing that if it takes longer to find a proof then it is itself a bit harder to reason about.
We can instantiate this like: Ak(B)↔∃i≤k.□i(□i+CAk(B)→B(Ak))
The idea is that if there is a short way to prove that the opponent B would cooperate back, then it takes just a constant C steps more to prove that we cooperate. So it doesn’t open us up to exploitation to assume that our own cooperation is provable in i+C steps.
The way in which this works at all is by cutting the loop at the point where the opponent is thinking about our own behaviour. This bot cuts it rather aggressively: it assumes that no matter the context, when B thinks about whether A cooperates, it’s provable that A does cooperate. (I think this isn’t great and can be improved to a weaker assumption that would lead to more potential cooperation.)
If you construct Bn similarly, I claim that Ak and Bn mutually cooperate if k and n are large enough, and mutually defect otherwise.
Similarly, I claim Ak can mutually cooperate with other bots like Bn(A)=□nA(Bn).