Payorian cooperation is easy with Kripke frames

[transhumanist_atom_understander]

The context is MIRI’s twist on Axelrod’s Prisoner’s Dilemma tournament. Axelrod’s competitors were programs, facing each other in an iterated Prisoner’s Dilemma. MIRI’s tournament is a one-shot Prisoner’s Dilemma, but the programs get to read their opponent’s code. Or, rather, a description of the behavior of the code in Gödel-Löb provability logic, which turns out to be enough to determine their behavior in the setup.

One fun result, right in the beginning of the paper, is about a program, FairBot, whose behavior is specified by “I’ll cooperate with you if you (provably) cooperate with me”. Despite the appearance of circularity, FairBot cooperates with itself. The proof involves Löb’s theorem, so we call this Löbian cooperation.

Andrew Critch has suggested another way of proving self-cooperation. Instead of Löb’s theorem, we use what he calls “Payor’s lemma”. It suggests a different way of defining a FairBot, something more like “If, when I hypothetically cooperate with you, you would cooperate with me, then I really will cooperate.”

This post is my attempt to explain why I think this approach is more promising, or at least why I like it more.

When thinking through these kinds of reflection problems with modal logic, I use Kripke frames, which are directed graphs of possible worlds. My fantasy is that when we’ve figured out this logical decision theory stuff, the reasoning will involve Kripke frames that are intuitively interpretable as something like a game tree, or paths through a game tree. Like, “if I do this, he’ll do that, because he knows I would do the other thing. But if I do that...”

With Löbian cooperation, I got nowhere with this. But Critch’s post was the first glimmer of the fulfillment of my fantasy. The only way to communicate to you what I see in it, though, is to walk you through a proof of self-cooperation with Kripke frames.

Löbian FairBot

First, reviewing the Löbian FairBot and Löbian cooperation, without Kripke frames.

We consider a program that takes another program as input, and outputs True to cooperate with it or False to defect. So, means that cooperates when the opponent is .

For FairBot, we have

That is, FairBot cooperates if and only if its opponent provably cooperates.

For an example of Löbian cooperation, consider FairBot playing against itself. Replacing with :

This is a Henkin sentence, that is, a sentence asserting its own provability:

Such sentences are in fact provable. This was established by Löb, in the paper that proved what we now call Löb’s theorem (some history from SEP). It gets more interesting when considering two FairBots with distinct code, which turn out to also cooperate with each other, but let’s move on to another kind of FairBot.

Payorian FairBot

Let’s call what we were discussing before a “Löbian FairBot”, and next, we’ll consider a “Payorian FairBot”. I still want to call it a “FairBot”, since I think the following does express a kind of fairness:

Actually, I’d rather drop all these parentheses, and say that means the FairBot cooperates, and means its opponent cooperates. If you like, and . Then the condition is:

Instead of checking whether the opponent cooperates, we check whether FairBot’s provable cooperation implies the opponent cooperates. But be careful about “implies”; it’s material implication, and doesn’t denote real dependence. For example, if the opponent unconditionally cooperates, then this implication is trivially true—we’ll cover this case in more detail later.

The Payorian FairBot looks more complicated. But reasoning about it is much simpler, at least with Kripke frames.

Kripke frames

In fact, it’s easy enough that I think it’s a suitable first exercise in using Kripke frames. So I hope you’ll keep reading even if you’ve never used them before, and this post can serve as a tutorial. To sell them a bit, I think of them as a tree data structure for tracking quotation levels. In the prisoner’s dilemma tournament, these are base reality, you imagining your opponent, you imagining your opponent imagining you, and so on. They end up at different depths of the tree.

The way they come up in the prisoner’s dilemma tournament is that we resolve matches using provability logic. But instead of writing proofs, we’re going to use the semantics. If you don’t know what I mean by semantics, I hope it helps to say that it’s analogous to resolving questions in propositional logic using truth tables. The semantics of propositional logic are that a sentence can be satisfied or not by a row in a truth table. Or, put another way, a row in a truth table can be a model for a sentence in propositional logic. So what does a model for a sentence of modal logic look like? (Really we’ll be applying this to a collection of sentences, but they can be combined to a single sentence by conjunction).

We’ll start with a Kripke frame, which is a set of possible worlds and a relation on that set. I had always heard this called an “accessibility” relation, but the Arbital page calls it a “visibility” relation, so I’ll stick with that.

In the special case of provability logic, the visibility relation must be transitive. When I draw a Kripke frame like , I’m not going to draw an arrow from to , but is visible from . So the diagrams will be directed graphs, and visibility is reachability following the arrows. The directed graph is I suppose not necessarily a tree, but it’s only in the case of a tree that I have some intuition, where a possible world deeper in the tree is more deeply nested in whatever kind of quotation we’re considering.

A Kripke model is a Kripke frame, plus an assignment of which sentences are true at each possible world. Our strategy for disproving a sentence of provability logic will be to show that it cannot be satisfied by any Kripke model. (And to prove a sentence, we’ll disprove the negation.)

The sentences that we assign to the possible worlds are not just “elementary” sentences of propositional logic, but can include modal sentences (those including or ). Modal sentences at one world have implications for what sentences must be true at other worlds. A claim of possibility requires that be true in a visible world; in a tree, at a node requires at some descendant node (not necessarily a direct child). A claim of necessity requires that be true in all visible worlds; in a tree, at a node requires in all descendants.

Worlds are not necessarily visible from themselves, because this is provability logic so we can’t in general go from to .

Well, that’s not the best beginner’s guide to Kripke frames. If you want a more complete explanation, check out the Arbital page or the SEP. But at least I’ve repeated the facts that I’m going to actually use, so let’s move on to applying these ideas to the Payorian FairBot.

Proving cooperation with Kripke frames, and CooperateBot

Our strategy for proving cooperation is to assume FairBot defects, write down what conditions this puts on a Kripke model, and look for a contradiction. A contradiction means no Kripke model can satisfy the premises, so FairBot must cooperate.

To assume FairBot defects means to assume

Or equivalently,

A statement of possibility. We’ll call the world in which this statement is true , and write what this implies about other possible worlds as so:

We satisfied the proposition that this stuff is possible at the root world by making it true in a visible world.

Anyway, now we can prove that FairBot cooperates with CooperateBot. CooperateBot always cooperates, meaning that is true. The assumption we will add, therefore, is , that is, that is provable. FairBot’s behavior depends upon what it can prove about its opponent, so we will always wrap the description of the opponent’s behavior like this.

at implies in all downstream worlds, which contradicts with at . So there cannot be a Kripke model that simultaneously satisfies FairBot’s non-cooperation and , so FairBot must cooperate.

This behavior justifies the name “FairBot”. It plays fair by cooperating with CooperateBot, rather than playing to win by exploiting it.

Writing this out more carefully. Let’s put these propositions at the root. First, the behavior of our FairBot:

Next, the behavior of its opponent CooperateBot, but wrapped as a statement of provability:

Finally, our assumption that FairBot defects:

I hope you’ll agree that the first statement and the third together are equivalent to what we were putting at the root before.

So to model these statements, we would need a Kripke model where they’re all true at the root:

Since this implies the possibility statement from before, we put in the implied visible world:

Since we have at the root, that implies downstream:

There’s our contradiction. No Kripke model can satisfy the requirements.

One Payorian FairBot will cooperate with another

Now, let’s assume both players are FairBots. Before we play them against each other, let’s just write down what their non-cooperation implies for a Kripke model, as before. Two separate Kripke frames, side by side:

Now, considering a FairBot whose opponent is a FairBot. It’s going to look like grafting the second Kripke frame above onto the first. To set it up, as in the previous section, we put three premises at the root world: the behavior of our FairBot, the behavior of its opponent (wrapped in a provability modality), and the assumption that our FairBot defects.

Contradiction at . That’s our proof that a FairBot cooperates with another FairBot.

But let’s slow down and look at what happened. At , we “unwrapped” the description of the other FairBot. Because we also have at , this world now looks like our from before. So at , we have everything from our previous . But because we had at , we unwrap that at , resulting in a contradiction.

Why this procedure feels right to me

I think of as a world our FairBot is simulating. It’s asking, “if I provably cooperate, what will my opponent do?” When the opponent is itself a FairBot, is familiar: it looks just like when we considered FairBot vs CooperateBot, but with and switched.

I imagine as a simulation done by the simulated opponent FairBot. We avoid an infinite regress, because we have assumed that in this simulation, the simulated opponent finds that the first FairBot cooperates.

This feels like the right depth to me. I imagine you imagining me, and we’re done. That feels like what I actually do when I’m thinking through Newcomb-like problems. In Newcomb’s problem, I think about Omega’s simulation of me, which I suppose is in , if my mental “simulation” of Omega is in .

The sense in which this is simpler than Löbian cooperation

But I feel I haven’t really indicated the appeal until I contrast this to the complexity I encountered with Löbian cooperation. Before I knew about Payorian cooperation, I tried putting these premises at the root world:

I didn’t like having to introduce the Löb sentence . I felt like I was putting it in by hand, and I wanted everything to be automatic. But with these premises, I could just mechanically hang requirements on a Kripke frame until I found a contradiction—in .

In Critch’s post, he also notes that a Payorian approach avoids the auxiliary sentence. And he argues that it is simpler, by counting lines of his proof in a “natural deduction”-type system.

The Kripke frame approach suggests a different way of quantifying complexity: how deep in the Kripke frame do you have to go, before you rule out a consistent Kripke model? For Payorian cooperation, you go two worlds deep, which feels right. For Löbian cooperation, you go four worlds deep, which feels wrong.

I titled this post “Payorian cooperation is easy with Kripke frames”. You could also say that proving cooperation with Kripke frames is easy, once you use Payorian cooperation. On a personal level, that’s the significance. When I first started doing these kinds of proofs a few years ago, I was optimistic about doing logical decision theory this way. I thought proving FairBot cooperates with itself would be the tutorial level, but with a Löbian FairBot, it felt more like a final boss. Stumbling across Critch’s post has restored my confidence in the potential of this approach.

[joseph_c]

I think this can also be used to make a smarter version of PrudentBot. If I remember right, PrudentBot is defined as that is, it cooperates if and only if it can prove that (1) its opponent cooperates with it, and (2) there is some world its opponent defects against DefectBot.

To me, the part about choosing DefectBot in particular to compare with seems a little hacked. What you’re really interested in is seeing if it will defect against you, even if you defect against them. Thus, I propose SharkBot, which I label . SharkBot is defined as It’s like your version of FairBot, but adds another condition, that it’s possible that its opponent’s cooperation leads to the possibility of mutual cooperation. Equivalently, it’s possible that provable defection will lead to the opponent defecting. Thus, SharkBot exploits opponents that don’t change their behavior even when they should know better.

I’m pretty sure this cooperates with itself and FairBot, but defects against CooperateBot and a larger share of stupid agents than PrudentBot does.

[James Payor]

(EDIT: focusing here on PrudentBot. Fwiw I like the idea you have in SharkBot use the weaker diamond when evaluating whether to defect! I’m less well equipped to analyze it at this time, still just grappling with how to handle diamonds at all in my usual proof search ontology.)

I’m less familiar with the diamond modality; but if I can correctly translate “exists some world that satisfies X” as “not every world satisfies not-X”, we get the following:

This will run into some trouble in the unbounded-proof-length provability logic model; since generally you can’t prove in some fixed length that there will be no proofs of any length of , on pain of unsoundness via a Lobian fixed point. So the version in the paper runs (I believe) as follows:

This is handling the part where might be FairBot and require “proving that there are no proofs” by checking the defection part under the assumption of one level of soundness. (I remember this gotcha because when I try to write down the PrudentBot that lives in my heart I end up with something closer to your version, but then the paper was doing this carefully different thing...)

Insofar as it’s really the proof lengths fighting that is the problem, I think something like the following might just work instead:

Anyway this is all to say that:

1. I agree that the original PrudentBot definition seems hacky, both in the DefectBot aspect (we can replace this with “doesn’t cooperate with every bot” if that helps), and also in the assuming exactly one level of soundness regard. It is ofc a nice POC given that it does manage to cooperate with itself with this machinery.

2. In terms of caching the diamond definitions out into provability logic some care seems to be required, and I’m interested in a well-behaved translation. The “not box not” translation doesn’t actually stay very faithful to the intent.

3. It might be that messing around with proof bounds is sufficient to get there, so you don’t end up with an inner proof length being able to diagonalize an outer proof length.

[transhumanist_atom_understander]

If I’m the Payorian FairBot and you’re my opponent, I simulate you under the assumption that there’s a proof I cooperate; this is .

So, to stay in the Payorian spirit, I could also simulate you under the assumption that there’s a proof I defect.

That makes me think that a Payorian PrudentBot would satisfy

Since there’s no third program involved, I can just define and to clean this up a bit:

The reason this looks right to me is because when we start drawing Kripke frames it does look like I (PrudentBot) am doing two simulations of you (my opponent), to see what you do assuming my provable cooperation and defection. Let’s assume . Then (and yes, is ),

I’ll cooperate if this can’t be satisfied, meaning we need to show contradictions in two different sets of requirements on the Kripke model. The first is the one from my post:

That’s the one where I simulate you assuming there’s a proof that I cooperate. We rule this out if, in that world, you cooperate (contradicting the in ).

The other:

This is the one where I simulate you assuming there’s a proof I defect. We rule this one out if, in that world, you defect (contradicting the in ).

So, if you cooperate in the simulation where there’s a proof I cooperate, and defect in the simulation where there’s a proof I defect, we rule these both out. That means we can’t satisfy the conditions imposed by my defection, meaning I cooperate.

That sounds prudent.

As for the Löbian PrudentBot testing its opponent on DefectBot and how that seems arbitrary. I mentioned in the FairBot vs FairBot section of my post that looks suspiciously like I’m simulating you facing CooperateBot. This was troubling to me because I shouldn’t care whether my opponent exploits CooperateBot. Similarly, in this proposed Payorian PrudentBot, looks suspiciously like simulating my opponent against DefectBot.

However, I think it’s not really? Although that brings to mind something missing from my post. In my post, when I’m simulating you, I never actually give you the full description of myself. I think a general version of this method requires an additional premise, repeating the description of myself but wrapped in a provability modality so it’s accessible in the simulations. Then my simulated opponent in doesn’t see a CooperateBot; rather, it sees whatever bot I am, but we assume there’s a proof I cooperate. Well… I hope this is different than just running my opponent against a CooperateBot, but I’m worried.

I’m not really sure how any of this will turn out, and I don’t have time to try it on paper right now or learn to use any of the automated tools. But in any case I think it’s good to record what seems like the obvious Payorian PrudentBot, at least to me, even if, as before, the solution ends up non-obvious.

[James Payor]

(Thanks for the post btw! My comments on this comment below.)

This PrudentBot def does feel in-spirit to me. I also agree with your analysis that it doesn’t fall for the pitfall of “I assumed in my hypothetical that you thought I would unconditionally cooperate with you, but then no fair you defected on me in my hypothetical! I defect!”

For instance this happens if you try, as I was inclined to try, . This quickly becomes “false” i.e. “defect” if you have a lying around.

With your definition, we have , and assuming we have a around I think that simplifies to . (I’m not sure I have that right!)

That’s… better behaved! It will run into the same Lobian difficulties as usual if we directly translate this as a provability bot. So imo we still need some better answer as to how we should interpret these as programs that more faithfully represents what we want in terms of their reasoning.

Also fwiw, I run with the model that the simulated opponent has access to both a description of your full behaviour and a shortcut proof that you cooperate with just them. (In the cooperation branch hypothetical.) So when your simulations have the cooperation proof in scope, you’re just saying that the behaviour is equivalent to CooperateBot in this very matchup. And it happens that this is often a sufficient condition for cooperation. (And if your opponent runs you on a different bot like DefectBot, the cooperation proof doesn’t apply there.)

So there’s some question here like “well what’s the point of simulating under the assumption of the narrow cooperation proof if we’re keeping the full description as a fallback?”

Part of what your post points at is an answer which is that, well, it works out more cleanly if you do! Specifically that reasoning is easier if, for the purposes of deciding to cooperate, you assume the decision is made and check that it’s stable/​good.

As for why that is the case, I have a more philosophical take that it’s about encoding choice, and the better mechanics we see are downstream of encoding this better. I’ll go into more detail in this collapsed section (you may well wish to gather your own thoughts first).

on encoding choice

We can think of the bot as containing some mechanisms that lead to certain actions, with conditions for firing.

The FairBot variant described in this post is a simple instance, with a default action of defection and a single mechanism that leads to coooperation when it fires.

I have some idea that the choice-y mechanisms are of the form “if I activate, will the outcome satisfy some property? if so I activate”.

So for a given mechanism we can have a widget with a goal target . We want a way of saying “if were to fire this would lead to ” as our condition for . And there’s a question of how to encode this in a program or in our modal logic setting.

Straight up trying won’t work, since and you won’t be able to form a statement like this. This was omitting the part where is using some model of consequences to make its choice.

So next up is , in which fires if our modelling shows that if fires this will lead to . You can in fact show that here!

The other option is ; this doesn’t assume ” fires” but rather “someone has a model that fires”, and is actually a bit more brittle. The reason this form can be preferable in the modal logic bots is that you are sidestepping the complexity of showing that you will need to check your opponent can tell that has fired. But I think this may be a bit of a hack relative to the version.

My reasoning here suggests for that if you have multiple conditions for action, you may factor out //​ that are each self-referential, and build your high level agent as trying each in sequence. I haven’t fully cached out yet what this looks like, and whether it e.g. gives you a meaningfully different PrudentBot.

I note that this picture doesn’t provide a convenient answer for the problem where in provability land your action “defect” may cause someone to need to prove . But as I guess I keep mentioning I view this as a bug in the provability encoding.

[transhumanist_atom_understander]

When I wrote this post, I did not yet appreciate the issue you’re talking about here: why we need consistency assumptions. To use the terms you used, a FairBot has some mechanism where finding a proof triggers cooperation, with defection as a default. I hadn’t appreciated the issues this introduces, because when I wrote this post, it had somehow not occurred to me to try the simple exercise of playing the FairBot in a match where it should obviously defect: the match against DefectBot.

Let be DefectBot and be the Payorian FairBot. I was actually surprised to realize that to prove , I needed a consistency assumption. But in retrospect it’s obvious―I require the nonexistence of a proof, but from an inconsistency everything can be proved.

This seems fatal for my proposed PrudentBot. Let be the PrudentBot. I want to prove , cooperation with the FairBot. The PrudentBot tests what the FairBot does with . As in the match against DefectBot, we can prove that FairBot defects, using a consistency assumption. But, in Kripke frame terms, I need this consistency assumption at , in the world where I simulate my opponent.

To prove , I just needed consistency at , in the “real world”. But to prove , I need to do that exact same derivation, but at , in the simulated world where PrudentBot considers what its opponent would do. So even a consistency assumption isn’t enough (at ).

I guess this gives me some intuition for why the PrudentBot in the original modal combat paper needs to check something in PA+1.

Leaving aside the details of these particular bots, and considering encoding choice. Or, really, encoding statements like “action has consequence ”. To borrow notation from the FDT paper, we can write that as , and consider different definitions of it.

However we define it, it seems like the right move is to cooperate if and , where and are my cooperation and defection, and and are my opponent’s cooperation and defection. Note that these two statements together are a “complete report”; that is, they specify the consequences of all of my available actions. The right move with any other report is to defect.

I did indeed take some time to gather my thoughts, and what I want is to understand how to encode reports. I think of an agent as consisting of a “quant” and a “manager”. The quant makes reports, and the manager acts on them. If I’m a PrudentBot, then my manager module will cooperate when given a report saying my opponent will do whatever I do, and will defect when given any other report.

If the quant writes reports by searching through proofs, then without a consistency assumption, the manager could do anything in real life. I think of the quant as searching through all proofs with an unknown random seed, and giving the manager the first report it finds. Given any random seed, we can just run the agent to see what it does; but to prove that it takes an action regardless of the random seed, we need a consistency assumption, so we know that only one report can come up in a proof search.

I’m pretty hopeful about the provability model, but I’m not going to try just writing down modal agents anymore. I think the right answer will come from trying to describe this quant/​manager framework in provability logic. As much as I like modal logic, I agree with Yudkowsky in Against Modal Logics: we need to start with an algorithm. Then, maybe, the behavior of the algorithm will be describable in modal logic.

What I like about the Kripke model approach is that it makes modal logic feel like running an algorithm. And what I like about Payor’s Lemma is not really that it encodes choice the right way, but rather that it showed me that it’s possible to have cooperation proofs that make intuitive sense when considering the Kripke model like an algorithm: is simulating what my opponent does given a proof of my cooperation, is my simulated opponent simulating me with a proof of their cooperation, and we’re done.

[James Payor]

Writing to say that I quite like and agree with the perspective here! I have been continuing to do my own puzzling about what would be a more wholesome instantiation would be than the “exists finite length proof” modality, as part of a project to ground things out better, though even absent that I feel confident that the intuition stands up and the processes above you’re outlining in Kripke terms should be realizable.

I also have two rambly thoughts to offer here, which I’ve included below if they’re of interest:

1. Fwiw in the first place I arrived at “” by thinking about what the algorithm steps should be in the modelling-my-prisoners-dilemma-opponent. I was very bothered by the part where we get to “I notice they are checking ” and then fail to shorcut! That’s a quantity directly under our control, why not counterfact on it? I was then kinda surprised to find this directly encodes in modal provability logic with reasonable behaviour even though “” feels very much like a poor imitation of a counterfactual.
   
   ...I thought that then obviously we should be able do the “real” PrudentBot. The naive encoding for that would be like “defect if , otherwise cooperate if , otherwise defect”. (This is a little different than your setup I think. I’m trying to ask “does defecting lead to (defect, cooperate)? if so defect; otherwise if cooperating leads to (cooperate, cooperate) then cooperate; otherwise defect”.) But yep this runs directly afoul of the consistency problem, inner “counterfactuals” do nothing to save it from that problem. And to be clear the problem is that it’s hard for itself and other agents to model that it won’t find some clever reason to activate the defect branch. And the OG PrudentBot is… uh… carefully skirting around this. I still expect there’s a nice answer waiting here; provability should be expressive enough to capture the limit of a relevant algorithm in a clean way. The translation is still eluding me.

2. When I think about the ontology that underlies the way the boxes work in the provability bot setting, I get a picture like the following:
   - Every box like in refers to one day earlier in time
   - From the perspective at the beginning of time, everything is “true”, i.e. holds
   - Things yesterday’s perspective considers true are must also be considered true on the day before by internal necessitation (ala ). the contrapositive () tells us that anything that becomes false stays false forever.
   - Lob’s therom says that , which I read as “the things that our perspective says must remain true are exactly the things that our perspective considers true”, so what ends up being provable/​”considered true” are exactly the things that we can see must remain true
   
   So this suggests a picture where the modal agents when interacting with each other are popping open a dimension of “discursive time” (thanks Sam Eisenstat for that term) along which to have a dialogue about what actions they’ll take. The particular chosen dimension is this peculiar provability box, with the property that on a given day you “might” have , or just one or the other, or none. Then the agents are set up with rules like “I will cooperate today if you cooperated with me yesterday” (FairBot) or “I will cooperate today if you didn’t cooperate with DefectBot yesterday and, if yesterday wasn’t the beginning of time, you cooperated with me” (OG PrudentBot).
   
   Then the stability machinery runs to determine the actual output. And while my story is a bit incomplete it still clarifies some of the mechanics for me.
   
   In likelihood though you may recognize the stability-over-time picture as performing the same/​isomorphic movements as the Kripke analysis! Which yeah I was not familiar with Kripke frames at the time. But still.
   
   My make takeaway from this is that it’s cool that the provability agents are able to pop open a dimension along which they can discuss and potentially bargain, without needing a physical clock, with its own pecularial lattice dynamics (you keep shrinking the space until it’s stable) that are handy in some ways but abysmal in others lol. So there’s a wide open question about what other alternatives there are, do those alternatives compose with each other (like does your alternative discursive time behave nicely if put up against a proof-search algorithm?), and what those alternatives look like described in logic.

[James Payor]

Man, okay I’m now wondering if the following works for a PrudentBot implementation? Calling our PrudentBot and our opponent in the encounter, let or something that grows a bit bigger than :

• Let be the length of the shortest proof that

• Let be the length of the shortest proof that

• If and then cooperate, otherwise defect

In symbols,

This is derived from the limit of an algorithm that searches for increasingly long proofs that we can obtain the opponent’s cooperation one way or another, with some budget for looking harder for a (defect, cooperate) proof should we find a (cooperate, cooperate) proof first.

The point of looking harder for the (defect, cooperate) option is that you don’t want to cooperate with a CooperateBot (or some complicated code version of CooperateBot) just because the mutual-cooperation proof was the easiest to find. And the point of having some budget that is not unlimited for searching harder for the (defect, cooperate) outcome is that once your opponent can see that you can find a (cooperate, cooperate) proof, they then get an upper limit on how much further they need to search to check you won’t throw that away in favor of a (defect, cooperate) proof.

And fwiw I haven’t properly vetted this idea yet, could easily break or be unsatisfying in a number of ways!

[transhumanist_atom_understander]

It’s interesting to learn why you first used as a decision trigger, because it sounds like you wanted to think of resolving these matches in terms of “well if I do this, then my opponent will...” type reasoning. I don’t know what to call it. “Mechanistic”… ?

But it’s interesting because even though that kind of reasoning wasn’t really in Andrew Critch’s write-up, it’s what popped out when I applied possible world semantics. And that’s just because I had been applying possible world semantics to everything, by writing out tableaux. The message got through.

Yes, “discursive time” sounds like what I see in the Kripke frames, though I have to qualify that by saying that Kripke frames don’t have to be linear. You can create a branch with sorry, I meant . I’ve never seen that come up in these kinds of games though.

It’s definitely appealing to have finite discursive time. I guess you have the “everything is true from the beginning of time” rule to deal with infinite discourse. Like, if we have ( could be that FairBot cooperates with itself), then we have , an infinite chain.

In modal logic, ruling out infinite chains corresponds to using GL instead of K4. See the zoo of modal logics and their corresponding requirements on Kripke frames.

I would rather not prove things by saying “this would lead to infinite discourse, so it doesn’t happen”. Lately I’ve been thinking of the condition as a sort of transformation of the condition. For provability in PA, it turns out we have an equivalence: PA proves if and only if it proves . Proving that equivalence requires Löb’s theorem, but once we’ve done it, we can resolve matches without ever encountering infinite frames. In the zoo of modal logics, that means we have to use GL to prove the equivalence, but then we only need K4 to resolve matches. (Irresponsibly generalizing from examples here.)

Of course I like resolving matches with finite discourse, because then I can just imagine the discourse step by step. It sounds like that was your original intention, and it was certainly the significance to me: once I used the condition and saw these finite frames, that’s what showed me that you can have interpretable mechanistic reasoning about this seemingly infinitely reflective problem.

[programjames]

I was talking with Joseph, and I think I like his SharkBot more because it fails more gracefully. Suppose (1) “proof” has an upper bound in computation cycles, and (2) people occasionally make mistakes in their logic. A good prover might spend more computation cycles in error correction. What happens if they do not have enough time to prove cooperation leads to cooperation, or defection leads to defection?

If Joseph’s bot stalls out on the second half of its computation, it concludes, “I couldn’t prove they would cooperate if I’m caught (provably) defecting,” and cooperates. If your bot stalls out on the second half of its computation, it concludes, “I couldn’t prove being caught (provably) defecting would lead to them also defecting,” and thinks it can get away with defection.

Another way of putting it: dumber bots are more likely to think they can get away with defection when they really can’t, and defect against bots smarter than them. If a bot is going to try to take advantage of rocks ^[1] , it better well make sure it is actually playing against a rock, and not just making a stupid mistake that hurts everyone.

Also, as an aside, I think making mistakes (logical bit flips some percent of the time) naturally penalizes high-complexity policies. This is why you might expect societies to begin with mostly cooperate/​defect bots, then transition to citizen/​police bots, and slowly build complexity where each individual’s policy is relatively simple, but society as a whole gets more complex interactions. I think this would be an interesting area of research.

1. ↩︎

   From the phrase, “how do you play a Prisoner’s Dilemma against a rock?” Rocks are bots that cooperate even if it is proven you are going to defect.

[James Payor]

Thanks, this is a solid point that choosing the defect-cooperate outcome should really be based on constructive knowledge, and the fallback shouldn’t be “definitely defect!” if you can’t obtain that.

So that makes me more think that is the sort of term that is legit in a PrudentBot, since “we can’t find a proof that if we provably defect then they cooperate” is what we actually wanted. And sure the naive translation into provability logic won’t like this, and I think this means we should look for a nicer translation, probably starting with getting a bounded proof-search bot correct.

I’m wondering about what the SharkBot term is doing, compared to my (probably broken) idea of using . If I converting this one to diamonds I get:

• (“it’s possible that I necessarily defect while my opponent defects”)

• (“it’s possible that my opponent defects while it is not possible that I cooperate”)

This seems potentially more restrictive than it needs to be? Well, restrictive can be good here, since what we are targeting is defecting as often as we can while guaranteeing a defect-cooperate outcome. But also as pointed out elsethread this PrudentBot approach may have trouble cooperating with itself.

Anyway this leaves me more ready to unpack the SharkBot condition, which is . This is a bit different than what I landed at, reading “it’s possible that my opponent defects or it is possible that I cooperate”.

Converting the SharkBot condition back to squares I get:

Ah okay, so I think this is caching out the version that’s like “I defect if it is stable that my opponent cooperates while I provably defect”. (I think this may be equivalent in strength to my condition under Lob’s theorem?)

Btw on the theory that “” was a bit of a mistake relative to “” as a basic approach, we could simplify a bunch of the language above to “it’s possible that my opponent defects while I defect” (my one) or “it’s possible that my opponent defects or I defect” (SharkBot). I’m taking this as some evidence that it would be better to go with the forms.

[transhumanist_atom_understander]

I don’t think was a mistake.

This gets at the deeper issue: how do we represent an action having a consequence? I don’t think it’s .

In the Prisoner’s Dilemma tournament, you don’t respond to my action, you respond to what you can prove about my action, so it’s really that’s important.

But I think that even in single player games, we should think of the environment as containing an implementation of us which takes an action when it can prove it’s the “right” action, so even then it’s provability that has consequences.

This may seem unnatural, but that’s just because considered decisions are unnatural, and mostly we just do stuff. But I think it’s a good model of thinking with a notebook open and plenty of time. That is, our model is that the consequences in the environment trace back to the existence of a proof in Peano Arithmetic.

My only reservation really is that I think maybe it should be , where means provable with a consistency assumption. Otherwise, how do I know that my implementation in the environment (for a single-player game) or my opponent’s simulation of me (in the Prisoner’s Dilemma) will actually find a proof of before a proof of ? Even if is provable, the implementation or simulation could get to a contradiction first.