i am reginald reagan aka RAGIN' RAYGUNS

aka Dr. Molecules aka Mr. Statistical-Probabilities but you can call me Reggie (though it's a pseudonym)

[raginrayguns]

The modal combat paper defined FairBot. If I'm FairBot, I cooperate in the prisoner's dilemma if and only if there's a proof that you cooperate:

F(X) ↔ □X(F)

I cooperate with a replica of myself, because that's a Henkin sentence, asserting its own provability:

F(F) ↔ □F(F)

Replacing F(F) with H:

H ↔ □H

And that's true by Löb’s theorem.

Andrew Critch made a post suggesting a different way to prove self-cooperation, from a different condition. Instead of Löb’s theorem, he used what he called Payor's lemma.

I made a post applying this to modal combat by defining what I called a Payorian FairBot:

F'(X) ↔ □(□F'(X) → X(F'))

Playing this against its replica:

F'(F') ↔ □(□F'(F') → F'(F'))

Replacing F'(F') with P:

P ↔ □(□P → P)

And that's true by Payor's lemma.

Okay, here's my question. Are these actually different bots? Or do we have F(X) ↔ F'(X) for all X?

[raginrayguns]

They are the same.

My "Payorian FairBot" was just the original FairBot — LessWrong

MIRI's proof-based prisoner's dilemma tournament defined agents encoded as formulas of Peano arithmetic (PA) with one free variable. means t

[raginrayguns]

when ive been writing these LW posts about decision theory, I take for granted you know what the prisoner's dilemma is. That's probably been a good assumption for a while, because people have read other stuff that explains it. For example Parfit's Reasons and Persons explains it. And Axelrod's iterated prisoner's dilemma tournament was widely discussed; besides Hofstadter's articles (which are directly upstream of Yudkowsky's TDT), Dawkins added a chapter on it to later editions of The Selfish Gene. That means not just the prisoner's dilemma, but the concept of computer programs playing it against each other in some sort of formalized game, is widely known nerd knowledge, and was so even before LessWrong.

What about Newcomb's Problem? I don't explain Newcomb's Problem in a post about it. Looking at the wiki article, it seems it was popularized by Martin Gardner. By the way, Hofstadter took over Gardner's section in Scientific American for a while, and that's where he wrote about Axelrod's tournament. Still, I have the impression that the unversal knowledge I assume comes down to Eliezer Yudkowsky specifically, and I don't expect Newcomb's Problem to be widely known off LW in the same way as the prisoner's dilemma. Eliezer Yudkowsky first explained it in Newcomb's Problem and Regret of Rationality. Probably, when I mention Newcomb's problem with the assumption the reader is familiar, I should make it a link to that post. I guess I could link to the LW wiki page, but it just quotes the explanation from that post anyway.

I guess I see myself as writing in a sort of literary scene where Martin Gardner and Douglas Hofstadter are foundational. I can't assume familiarity with everything they wrote, but I can assume readers are familiar with certain classics, if not by reading them directly, then by hearing them summarized second-hand. You know the prisoner's dilemma, you know Newcomb's problem, you know Conway's Game of Life (also popularized by Gardner).

LessWrong says it's "an online forum and community dedicated to improving human reasoning and decision-making". But to me it is continuing this literary scene past the demise of print media. In 1970, Gardner wrote about Conway's life, Bill Gosper read it and figured out the glider gun and wrote a letter to Gardner, who wrote it up for his next article. What do we do now, without Scientific American? Well, when I had something to add about the modal agent prisoner's dilemma tournament, I made a LessWrong post.

While I'm sympathetic to their grander mission, the immediate importance of LessWrong to me is that it's part of how we're able to continue this computer nerd literary scene.

[raginrayguns]

saw this on LW...

Smart hard-working people are trying to make the OpenAI Huggingface hack into AI's Three Mile Island

maybe they're right to do so but i think that's going to help explain what we're going to be hearing about it

[argumate]

[well aware I could just find this out myself] Do these kinds of mind-reader's prisoners' dilemma tournaments get more interesting if you stop abstracting away all the real-world restrictions? E.g. programs can only be x bits long, and they only have y FLOPs to make a decision. (and maybe the output can be a probability distribution over {cooperate, defect})

honestly not sure if that makes it more interesting or less; like if programs are shorter and can do less then that might make it easier to prove facts about their behaviour but also makes it harder for you to do anything at all; I think sticking with the god's eye view of published simple strategies already gets quite twisty.

agents that have a probability distribution sounds more like that paper on how iterated prisoner's dilemma resolves to something like the ultimatum game I think, where it's less about proving what they will do and more about trying to infer whether they're following a strategy at all, i.e. can you negotiate with them or are they just a brick on the accelerator and you just have to take it.

[raginrayguns]

for whatever reason lesswrongers always post about provability with bounded proof length. I don't read any of it, not sure if I'm missing anything. There's even a paper I've never read.

I post about bounded proof lengths sometimes because I think Godel's speed-up theorem is cool. When you're thinking about what incompleteness means I think it helps to remember that "this statement has no proof of length N or less" has a (long) proof, but as long as N is larger than the size of proofs your computer can verify, you can assume the negation without inconsistency (that your computer can verify).

The point I'm trying to make there though is I'm trying to think of the platonic "provability" of metamathematics as a sort of limit of what real computers do, like as memory goes to infinity. And we do have good reason to take that limit. Like yeah in real life we can run out of memory checking a proof, but unless that's essential to what we're thinking about, just drop that from the model. Just like I assume the nucleus is a point in quantum chemistry, the population we're sampling from is infinite in survey statistics, etc.

[argumate]

Okay I'm trying to get how you're defining FairBot and I'm falling back on Haskell since that's the only time I've ever used a fixed point function

so FairBot is

f x = x f

which you can't define in Haskell but whatever. If I define

r f x = x f

then I can define

f x = r f x

then eliminate and I have

f = r f

so I have

f = fix r

(Haskell lets me define r, but gives me a type error on fix r)

Is this what you're doing?

I don't see an algorithm here... but I guess it's just lambda calculus... ?

let me use the other bot to answer this since I'm not a Haskell expert:

Yes — your derivation is exactly right: FairBot is fix (\f x -> x f). The type error is because Bot = Bot -> Bool is a recursive type; wrap it in a newtype and it typechecks:

newtype Bot = Bot { app :: Bot -> Bool } fairbot = fix (\f -> Bot (\x -> app x f))

Now run it: app fairbot (Bot (const True)) terminates (True), app fairbot fairbot loops forever. That divergence is real — two FairBots simulating each other unwind endlessly — and it's what Haskell's fix means: the least fixed point in the definedness order, where the undetermined entries come out ⊥.

My implementation changes this in two ways. First, extensionality with a finite population: a bot isn't code, it's a row of n booleans — so Bot -> Bool collapses from an infinite function space to a finite table, and the definitions compile to a finite system of boolean constraints over the n×n matrix entries (M[F,X] = M[X,F], and so on).

That's where the algorithm you're not seeing lives: build the constraint system, stratify it by dependency cycles, and solve each cycle by Knaster–Tarski iteration — start every unknown at True and iterate down until stable. It's the same shape as computing nullability of grammar nonterminals or a dataflow analysis, not the same shape as lazy unfolding.

Second, fix is a selection policy, not an evaluation strategy: the constraint system can have several solutions (your ⊥ entries are exactly the ones that are free), and ν-fix says "round the free ones up" (greatest fixed point in the truth order 0 ≤ 1), while lfix says "round them down". So where Haskell honestly reports ⊥ for FairBot-vs-FairBot, my fix declares cooperation by convention of greatest fixpoint — that convention is the Löbian handshake.

(Note that Haskell's fix is a least fixed point, but in the definedness order, not the truth order — lfix f. f is 0 in my implementation but still ⊥ in Haskell. "Least" without naming the order is ambiguous).

More jargon about the underlying model:

The denotation of a population is not a λ-term and there is no β-reduction anywhere. The model is a finite boolean matrix over the closed universe of reachable applications; the definitions induce a monotone operator on the lattice of matrices; the language's meaning is a designated solution of M = Φ(M), selected per-cycle by the ν/μ policy, with all/any quantifying over the entire solution set. The nearest established formalisms are boolean equation systems / the boolean μ-calculus (that's essentially what the solver implements, SCC-stratified with μ-priority nesting), and logic programming read over atoms coop(A,B) — where ν-fix is "cooperate unless refuted," μ-fix is the classic least-model semantics, and all/any are cautious/brave entailment from answer-set programming. λ-notation in the grammar is just a convenient surface syntax for generating those constraints; if you insist on giving it operational lambda semantics, you get divergence at precisely the entries where the constraint view has freedom — which is the whole point of having the conventions.

[raginrayguns]

thank you Claude for the journey from "Yes — your derivation is exactly right" to "The denotation of a population is not a λ-term and there is no β-reduction anywhere."

[raginrayguns]

i finally got @argumate to post about newcomb's problem again (if we believe David Lewis that prisoner's dilemma with yourself is Newcomb's problem) but he got me to type f x = x f into Haskell and see what happens

[cryptotheism]

>game is based on occult stuff

>they interpret it wong

[raginrayguns]

> works of historically central occultist are based on occult stuff

> they interpret it wrong

[cryptotheism]

It never FUCKING ends

[cryptotheism]

>game is based on occult stuff

>they interpret it wong

[raginrayguns]

> works of historically central occultist are based on occult stuff

> they interpret it wrong

[argumate]

a lot of commentary on the Odyssey seems to hinge on the belief that guilt didn't exist prior to Christianity, an assumption that has really weird implications for what those people must think of most of humanity.

(some people dress it up as an "honour/shame culture" thing but then imply that changed in 380AD without considering why dueling culture for example persisted over a thousand years after that).

[argumate]

raginrayguns said: maybe theyre paraphrasing nietzsche

maybe, or maybe they're paraphrasing people who are paraphrasing nietzsche, or maybe they're idiots

[raginrayguns]

i don't think it's something idiots independently reinvent. Nietzsche's starting point was that Homer reveals that morality used to be fundamentally different, along these lines. Genealogy of Morals starts there, and claims it was the starting point for the ideas in his previous books which don't emphasize this as much

[aorish]

yeah, across his works Nietzsche himself seems to waffle a bit on whether slave morality is Paul's fault, or Socrates, or the early church fathers. all of which i think massively overestimates the influence that intellectual culture has on society.

i do think it's a useful distinction to make, but probably not a historically accurate one; at any rate we have evidence of people as early as the 6th century BCE such as Xenophanes who are critical of the kind of "morals" that the Homeric poems might be instilling in people. And I'd posit that it's not particularly hard to find evidence of "slave moralisms" and ressentiment and such in the Presocratics or even Theognis, Nietzsche's favorite archaic poet.

In Nietzsche's defense he was trying to overturn Winckelmann's even less accurate picture of the Greeks as a pure and simple people obsessed with symmetry and perfection, which was uncritically believed by most classicists of the time. but his history is still mainly polemic, not scholarly.

[raginrayguns]

yeah, it's very much the fantasy of a specific 19th century philologist. If people saying that the Odyssey reveals pre-Christian morals on twitter or whatever they must be repeating Nietzsche's reading of it.

[argumate]

phaeton-flier said: so the best bot here, the one that maximizes its score in every possible tournament, is the one who Cooperates with bots who themselves only cooperate if their opponents cooperate. That is, it cooperates only when it definitely moves it from (D,D) to (C,C) and not otherwise, right?

close! there are some language constructs I didn't describe in the original post which allow defining bots like that.

the bot you describe sounds similar to what I've been calling BilateralPrudent, which evaluates counterfactuals:

let me break that syntax down:

[C] all(φ) is a modal counterfactual that says "in the worlds where condition C holds, does φ hold in all of them? (you can also say any(φ)).

so we're saying: BilateralPrudent cooperates with X if in all the worlds where it cooperates with X, X cooperates back, and in all the worlds where it defects against X, X defects back.

that is to say, BilateralPrudent cooperates with an opponent iff doing so would induce that opponent to cooperate with it: it will not cooperate against CooperateBot or DefectBot, it will cooperate with FairBot and PrudentBot, and it will not bother cooperating with a bot whose cooperation would not be affect by its choice.

is there actually an example in which BilateralPrudent differs from PrudentBot though? (reminder: PrudentBot is like FairBot but it doesn't bother cooperating with any bot that cooperates with CooperateBot).

we can definitely construct one using the richer language of global constraints I haven't discussed yet (argmax and argmin), but I haven't yet proven whether it's possible in the more restricted subset of the language considered thus far.

[argumate]

oh man it is possible!

C cooperates universally and D defects universally, F cooperates mutually, P cooperates mutually except with those that cooperate with D, Q cooperates with anyone who defects against D (including D!), BP is BilateralPrudent we defined earlier, R cooperates with anyone who cooperates with F and defects against D, S cooperates with anyone who cooperates with C.

phew, finally P cooperates with R but BP does not, as it's smart enough to see that R's cooperation does not hinge on it being mutual!

that's great but I cannot pretend this presentation is clear, it clearly needs some better explication! in the meantime, let's add up the scores each bot receives, using the standard Prisoner's Dilemma payoffs:

BilateralPrudent wins! solely for the extra two points it gets from R, unlike regular PrudentBot, nice.

[raginrayguns]

@argumate said:

@raginrayguns it’s like FDT! a little

and raises the same question as FDT: how do you run the opponent function in a possible world where the BilateralPrudent function has a different output than it does in the real world

[argumate]

a lot of commentary on the Odyssey seems to hinge on the belief that guilt didn't exist prior to Christianity, an assumption that has really weird implications for what those people must think of most of humanity.

(some people dress it up as an "honour/shame culture" thing but then imply that changed in 380AD without considering why dueling culture for example persisted over a thousand years after that).

[argumate]

raginrayguns said: maybe theyre paraphrasing nietzsche

maybe, or maybe they're paraphrasing people who are paraphrasing nietzsche, or maybe they're idiots

[raginrayguns]

i don't think it's something idiots independently reinvent. Nietzsche's starting point was that Homer reveals that morality used to be fundamentally different, along these lines. Genealogy of Morals starts there, and claims it was the starting point for the ideas in his previous books which don't emphasize this as much

[intimate-mirror]

If I knew I was dying soon, I think I would want to talk to lots of people and basically infodump my memories and ideas to them

I wonder if the reason nobody has done this with me is just they don't trust that I would listen, or if it actually matters less than I think to someone dying for their ideas and stories to be passed along

[raginrayguns]

my grandma seems to care way more about family property, a few apartments in new york city and a beach house we rent out.

Besides the legal effort of transferring those, there were some failed projects: she couldn't convince any of us to take her ancient car, or to live with her long enough to get on the lease and inherit her rent control.

i identify her to a great degree with her apartment, and i think she does too? She's been there for decades, and much of her daily effort goes into maintaining it. Her now-dead husband lived there since the '60s. She never purchased it, which for her lifetime may have been the right choice financially, because of the rent control. She did purchase an apartment down the hall, which she used to rent out, and which my aunt lives in now.

She tells me about her upbringing and parents and stuff, but mostly when I ask, whereas trying if possible to keep her current rented apartment in the family was something she initiated and pushed for (unsuccessfully).

In terms of cultural transmission, she seems very concerned that my newphews, her great grandchildren, should read. She reads constantly, and used to work for a company that published children's books. Obviouly she's happy that my brother and I read a lot, as does my father, but she's never been concerned that I read any specific book.

She actually did a bit of memoir writing, now that I think of it, short essays, which she did give me to read. I once asked her about doing more of it and she said it was just therapeutic after her husband died, she didn't particularly care to continue.

[raginrayguns]

im not rly interested in british royalty but princess d does have some significance to me because she kind of shows me how others could have been, 30 years ago. Like she seems to have had real star power.

i don't really get the current interest... these seem like placebo celebrities.

[argumate]

tell me oh muse, of that ingenious bot that cooperates with itself--

I was writing about FairBot, which cooperates with any bot that it can prove cooperates with it in a one-shot Prisoner's Dilemma tournament, and I said some stuff about hierarchical truth tables which didn't really make sense so I had to go back and work it out properly, or at least in a way that I like. So!

consider this square matrix, where each row represents a bot in the game and 1 is cooperation and 0 is defection; it's an adjacency matrix for a graph where the bots are nodes, rows are outgoing edges and columns are incoming edges, and the existence of a directed edge from one node to another represents cooperation:

C is CooperateBot, which cooperates with everyone, D is DefectBot, which cooperates with no one, and F is FairBot, which cooperates with every bot where the cooperation is mutual; note that the row and column for F are identical!

FairBot is pleasingly symmetrical and it certainly seems altruistic for it to reciprocate like that, but if we want to win this game we might note that it's not strictly necessary to cooperate with CooperateBot, given that it is happy to cooperate with everyone, even DefectBot! let's create a PrudentBot that is mostly fair but defects against oblivious bots:

you can see that PrudentBot wins more than any other bot so far given that it has two outgoing cooperation edges and three incoming; I haven't bothered calculating the actual score for these bots based on the game weights but it's clear that this strategy dominates FairBot and the others.

now we have four bots, but can we add more? and how many bots exist in total? an infinite number of them! in fact an uncountably infinite number of bots, as we can always add a new bot with unique behaviour by a process of diagonalisation similar to that used to prove the uncountability of the real numbers; thankfully we are going to start writing programs which are at least only countably infinite.

the matrix is growing unwieldy so let's switch to defining bots with simple expressions that apply constraints to matrix rows:

1 and 0 are the constant rows (cooperate/defect with everyone), while FairBot is defined by the recursive fixpoint F = Reflect(F), where the Reflect operator transposes a column into a row:

so FairBot(X) is just X(FairBot), the expected symmetry, and then PrudentBot breaks that symmetry by cooperating only with bots that cooperate with it and don't also cooperate with DefectBot, a clear sign that they are imprudent.

this gives us a nice little language for recursively defining bots in terms of functions over bots to booleans:

R is the expression language for bots, keep in mind that each term represents a function that is also an entire row of the matrix (the notation is simplified in the way that we've omitted all the indices, something that usually drives me nuts as a programmer, but it would clutter up the syntax to add them, so constants are actually constant functions and so on).

phi represents an individual boolean value, we will get to why we need that (and C conditions!) later, promise.

I'm going to assert without evidence at this time that there exists a decidable algorithm for taking a set of bot definitions and solving the constraints to calculate the adjacency matrix, although we do need to specify that fix denotes the greatest fixpoint, so any unspecified choice defaults to cooperation, which is needed to ensure FairBot cooperates with itself (the mythical attentive reader may have noticed that without this constraint it would be equally acceptable for FairBot to defect against itself and still satisfy mutuality).

we can explore more interesting possibilities than PrudentBot that I will hopefully get to tomorrow, but I think this formalism is a convenient and fun way of exploring the nature of this cooperation game.

[raginrayguns]

contrasting to the provability setup, you're putting the asymmetry between cooperating and defecting in the fixed point definition, but in the provability setup it was in the definition of the bots

FairBot was "I cooperate if and only if there's a proof that you cooperate"

This is not symmetrical between cooperation and defection. It's equivalent to "I defect if and only if there's no proof that you cooperate"

cooperate if there is a proof, defect if there's no proof (which is why it's amazing that the matches could be computed)

it's like, cooperation is a first preferred option, we're looking for a reason to do it. And defection is the default fallback option

If you flip the defaults you get what I call SpitefulBot, which says " i defect if and only if there's a proof you defect"

SpitefulBot defects on itself, but cooperates with CooperateBot, some might say fails to exploit CooperateBot. Its score is not looking so good

[argumate]

you can have a least fixpoint or greatest fixpoint, so you can define a variant of FairBot that doesn't cooperate with itself (and is still consistent, as F(F) = F(F) doesn't specify whether it cooperates or defects) and that's in the definition of the bot itself, technically not a default of the system; standard syntax is something like:

FairBot = ν x . Reflect(x) SpitefulBot = μ x . Reflect(x)

where nu/mu are greatest/least fixed point operators.

[raginrayguns]

i think self conscious people are disturbed by me cause im blunt and make a lot of negative affect facial expressions (i think im tuned for sensitive fear disgust annoyance etc). People that are less self conscious are able to notice that im actually very easy to please in a different sense. There was a phrase in Arrowsmith I can't find, i think it was something like "self-sufficient as a cat", describing his wife. The context was he was annoying his wife by trying to do stuff for her or something

[raginrayguns]

from Arbital's pop-level introduction to logical decision theory:

A: There's another reason FairBot1 is suboptimal. Can you imagine what happens if two copies of FairBot1 play each other...? Q: They go into an infinite loop of Fairbot A simulating Fairbot B simulating Fairbot A simulating Fairbot B until they both run out of time? A: Right. So a preliminary interesting technical result is, we fixed that--we described a simple and natural FairBot2 that does not run out of time if it bumps into itself. Q: Huh. How? A: Magic. Q: ...

see this kind of thing is why i want to write a non-mathematical version of my payorian cooperation post. Like, 6 months ago i couldn't have done any better than this for a plain language explanation. But it turns out that cooperation between proof-based FairBots is simple enough to keep in your head.

Define "possibility". Something is possible if there's no proof it won't happen.

For nested possibility, we'll have to think about possible worlds. A possible world is a state of affairs, including what's possible. So possible worlds are possible relative to other possible worlds.

Define "betrayal". To betray you is more than to just defect on you. It means I had a proof of your cooperation and defected on you anyway.

Suppose you're a FairBot. Your rule of behavior is you defect if and only if it's possible I betray you.

So let's suppose you defect, for a proof by contradiction that you cooperate. You defected, so it must be possible that I betray you.

Suppose I'm also a FairBot. Consider the possible world where I betray you. In this possible world, there's a proof you cooperate, and I defect. Since I defect and I'm a FairBot, it must be possible that you betray me. But it can't be, since the proof that you cooperate rules that out. There's our contradiction.

Not so deep right? Not "magic", that is, Löb's theorem.

It wasn't obvious because the original FairBot's rule was that, if you're a FairBot, you defect if and only if it's possible I defect. None of this about betrayal. But the condition is equivalent. Why? Magic.

Still it seems to me like a big deal that we could have just used a different equivalent definition of FairBot and then we wouldn't feel it's so non-obvious or mysterious that it cooperates with itself

[raginrayguns]

was looking through a Q&A book on magic, and I found that a lot of the questions were about the social aspect, like should I have a "master", or should I go to a workshop. Idk what i was expecting the answer to be but it makes a kind of sense: to decide whether to go to a workshop, do a tarot reading.