Something I'm now realizing, having written all these down: the core mechanism really does echo Löb's theorem! Gah, maybe these are more like Löb than I thought.

(My whole hope was to generalize to things that Löb's theorem doesn't! And maybe these ideas still do, but my story for why has broken, and I'm now confused.)

As something to ponder on, let me show you how we can prove Löb's theorem following the method of ideas #3 and #5:

• $\square A\to A$ is assumed
• We consider the loop-cutter $X\leftrightarrow \square (X\to A)$
• We verify that if $X$ activates then $A$ must be true:
  • $X\to (\square X\to \square A)$
  • $X\to \square X$
  • $X\to \square A$
  • $X\to A$
• Then, $X$ can satisfy $\square (X\to A)$ by finding the same proof.
• So $X$ activates, and $A$ is true.

In english:

• We have $A$ who is blocked on $\square A$
• We introduce $A$ to the loop cutter $X$, who will activate if activation provably leads to $A$ being true
• $A$ encounters the argument "if $X$ activates then $A$ is true, and this causes $X$ to activate"
• This satisfies $A$'s requirement for some $\square A$, so $A$ becomes true.

Also Plan B is currently being used to justify accelerating various danger tech by folks with no solid angles on Plan A...

My troll example is a fully connected network with all zero weights and biases, no skip connections.

This isn't something that you'd reach in regular training, since networks are initialized away from zero to avoid this. But it does exhibit a basic ingredient in controlling the gradient flow.

To look for a true hacker I'd try to reconfigure the way the downstream computation works (by modifying attention weights, saturating relus, or similar) based on some model of the inputs, in a way that pushes around where the gradients go.

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: $$A_k\left(B\right)\leftrightarrow {\exists }_{i\le k}.{\square }_i\left({\square }_{i+C}{A}_k\right(B)\to B(A_k\left)\right)$$

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 $B_n$ similarly, I claim that $A_k$ and $B_n$ mutually cooperate if $k$ and $n$ are large enough, and mutually defect otherwise.

Similarly, I claim $A_k$ can mutually cooperate with other bots like $B_n\left(A\right)={\square }_{n}A\left(B_n\right)$.

A point of confusion: is it enough to prove that $A\to \square B$? What about $A\to B$? I'm not sure I can say this well, but here goes:

We might not be able to prove $A\to B$ in the theory, or even that $\neg \square \perp$ (which would mean "there are no proofs of inconsistency"). But if we believe our theory is sound, we believe that it can't show that a copy of itself proves something false.

So $A\to \square B$ tells us that if $A$ is true, the theory would show that a copy of itself proves $B$ is true. And this is enough to convince us that we can't simultaneously have $A$ true and $B$ false.

Also, here's a proof that a bot $A\leftrightarrow \square (\square A\to B)$ is never exploited. It only cooperates when its partner $B$ provably cooperates.

First, note that $A\to \square A$, i.e. if $A$ cooperates it provably cooperates. (Proof sketch: $A\leftrightarrow \square X\to \square \square X\leftrightarrow \square A$.)

Now we show that $A\to \square B$ (i.e. if $A$ chooses to cooperate, its partner is provably cooperating):

1. We get $A\to (\square \square A\to \square B)$ by distributing.
2. We get $A\to \square \square A$ by applying internal necessitation to $A\to \square A$.
3. By (1) and (2), $A\to \square B$.

(PS: we can strengthen this to $A\leftrightarrow \square B$, by noticing that $\square B\to \square (\square A\to B)\leftrightarrow A$.)

If I follow what you mean, we can derive: $\square \left(\square A\right)\to \square B\to \square \left(\square B\right)\to \square A$

So there's a Löbian proof, in which the provability is self-fulfilling. But this isn't sufficient to avoid this kind of proof.

(Aside on why I don't like the Löbian method: I moreso want the agents to be doing "correct" counterfactual reasoning about how their actions affect their opponent, and to cooperate because they see that mutual cooperation is possible and then choose it. The Löbian proof style isn't a good model of that, imo.)

(In fact, I think "assume they will think I cooperate" turns out to be too strong, and leads to unnecessary defection. I'm still working through the details.)

Thanks! I also wrote up my proof in another comment, which should help triangulate intuition.

In case this helps folks' intuition, my generating idea was something like: "look at what my opponent is thinking, but assume that whenever they check if I cooperate, they think the answer is yes". This is how we break the loop.

This results in a proof of the lemma like thus:

1. $x\leftrightarrow \square (\square x\to x)$ (given)
2. $x\leftrightarrow \square (\square x\to \square (\square x\to x\left)\right)$ (unrolling one step)
3. $\square x\to \square (\square x\to x)$ is straightforward intuitively, and we can get there by applying box-distributivity to $\square (x\to (\square x\to x\left)\right)$

(EDIT: This is basically the same proof as in the post, but less simple. Maybe the interesting part is the "unroll once then break the loop" intuition.)

Relatedly, with two agents $A$ and $B$, we can have:

1. $A\leftrightarrow \square (\square A\to B)$ (given)
2. $B\leftrightarrow \square (\square B\to A)$ (given)
3. $A\leftrightarrow \square (\square A\to \square (\square B\to A\left)\right)$ (substituting $B$ into $A$)
4. $\square A\to \square (\square B\to A)$ is straightforward as before