transhumanist_atom_understander

tran­shu­man­ist_atom_un­der­stan­der’s Shortform

• transhumanist_atom_understander 24 Jul 2026 18:16 UTC

  3 points

  0

  on: tran­shu­man­ist_atom_un­der­stan­der’s Shortform

  Does anyone have software they like for doing provability logic? Two use cases:

  • Deciding theorems of GL. I recently made a post which had two derivations in GL. GL is decidable, so I should be able to write them as material implications and run some program to check if they’re theorems. I have no idea what program people would actually use for this though.

  • Computing fixed points. For that post, I would want to input the “equation” , and get as output the “solution” for , which is . That’s all you need for a much shorter proof than the one I did. Does the MIRI provability repo do this somehow? Or is there some standard tool?

• transhumanist_atom_understander 19 Jul 2026 14:51 UTC

  3 points

  0

  in reply to: James Payor’s comment on: Payo­rian co­op­er­a­tion is easy with Kripke frames

  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.

• transhumanist_atom_understander 19 Jul 2026 1:24 UTC

  1 point

  0

  in reply to: joseph_c’s comment on: My “Payo­rian FairBot” was just the origi­nal FairBot

  No problem, I edited and it looks a lot better now.

  With that cleared up I do want to get back to the root of this thread, because it’s genuinely weird that the FairBot pseudocode in the paper has a branch where it says “if there’s no proof, return D”. But it’s getting late here so I’ll have to do that another day.

• transhumanist_atom_understander 19 Jul 2026 0:44 UTC

  5 points

  1

  in reply to: joseph_c’s comment on: My “Payo­rian FairBot” was just the origi­nal FairBot

  Okay, that I can answer. It’s derived from the previous theorem, as follows.

  The following means that is a thereom of PA, which by definition means there’s a proof of it:

  Let be the sentence in PA that asserts is provable, that is, that asserts there exists a number which is a Gödel number of a proof of the sentence with Gödel number .

  Take the proof of and convert it to its Gödel number. That satisfies the existence statement , so we have a constructive proof of it. So we have:

  And I’m using the box to represent PA’s provability predicate, so that’s:

  Does that make sense?

  I should definitely edit the post. I at least need to clearly claim it follows from the previous theorem.

  I wonder if there’s a short way to indicate this whole line of reasoning. I guess if I just want to point to the principle, it’s the first of the Löb provability conditions, but I’d rather indicate why it’s true.

• transhumanist_atom_understander 18 Jul 2026 23:40 UTC

  1 point

  0

  in reply to: joseph_c’s comment on: My “Payo­rian FairBot” was just the origi­nal FairBot

  No, we’re not on the same page. You’re still repeating that we agree about the validity of the GL derivation.

  The question is what the validity of the GL derivation implies about PA. What I’m saying is that the validity of the GL derivation implies that the Löbian FairBot (as defined in PA) satisfies the Payorian FairBot’s condition (as defined in PA). This works even though the GL derivation has two premises. That’s why I’m “allowed” to have both premises: because the validity of the GL derivation with two premises is sufficient for the desired conclusion about PA.

  This is what I establish in the section How the GL proofs we’ll do translate to PA. Unless you either read that section and are convinced by it, or read that section and identify some mistake (there is none), how can this thread go anywhere?

• transhumanist_atom_understander 18 Jul 2026 23:20 UTC

  1 point

  0

  in reply to: joseph_c’s comment on: My “Payo­rian FairBot” was just the origi­nal FairBot

  Right, I know the question isn’t whether the GL derivation is correct.

  This is what I want to get on the same page about: do you agree that the GL derivation, with both those premises, establishes that the Löbian FairBot, as defined at the top of my post, must satisfy the condition of a Payorian FairBot, as defined at the top of my post?

  This is what I establish in the section How the GL proofs we’ll do translate to PA. The answer to your question is in that section. I use both the premises, because the GL implication using both the premises is sufficient to establish that if we have the PA theorem from the definition of Löbian fairness, then we must also have the PA theorem from the definition of Payorian fairness.

• transhumanist_atom_understander 18 Jul 2026 22:23 UTC

  1 point

  0

  in reply to: joseph_c’s comment on: My “Payo­rian FairBot” was just the origi­nal FairBot

  Regarding (1), you can do it that way if you want. If (the form of the implications I prove), then . So my post does add up to a proof that the boxed forms of the fairness conditions are equivalent to each other. In fact, that’s how I justified it in a previous draft.

  But then I decided that’s extraneous, because I realized that my implications already say what I want them to say about PA, and wrote that up in the section How the GL proofs we’ll do translate to PA. I guess that’s how I address (2): I’m not doing anything illegal or mistaken in that section. I suppose you can object to representing the fairness conditions in terms of provability in PA, which strictly speaking is an objection to the definition of a modal agent in the original paper rather than an objection to the arguments in this post. But you can’t deny that my GL derivations imply those conditions are equivalent.

  Part of the reason I’m so sure is because of the fact about GL I mentioned earlier. That implies is the expression in GL that you can set up implications the way I did. This is chapter 1 theorem 10 of Boolos by the way, and looking it up I’m reminded that it’s actually true in K4 and any logic that extends it, not just GL.

  Regarding (3), it does get weird when we try to talk about computer programs rather than just formulas of Peano Arithmetic. But I don’t really want to get into it until we’ve ruled out any objection to applying the GL implications to the fairness conditions as stated at the top of the post, in terms of theorems of PA.

• transhumanist_atom_understander 18 Jul 2026 19:22 UTC

  1 point

  0

  in reply to: joseph_c’s comment on: My “Payo­rian FairBot” was just the origi­nal FairBot

  FairBot is some PA formula such that, for each , we can prove:

  That’s the specialization of the modal agent definition on page 11 of the paper to .

  Are you saying we can’t actually prove this PA theorem about FairBot (for each )? Or are you saying this isn’t enough to apply the GL derivations, because if so I think I addressed that in the section How the GL proofs we’ll do translate to PA.

My “Payo­rian FairBot” was just the origi­nal FairBot

How to read tableaux, a for­mal sys­tem for modal logic with Kripke models

• transhumanist_atom_understander 30 Jun 2026 18:16 UTC

  6 points

  0

  on: Func­tional De­ci­sion The­ory: Not Even Wrong, Also Wrong

  Back when the FDT paper came out, I considered counterpossibles an inherently interesting question.

  For example, I wondered, is there a Bayesian formulation of probabilistic primality testing? Well, there is, as Gaifman explains, but can we compute P(x is prime|witnesses) for a particular x and particular witnesses? That seems to require counterpossibles: even if the number is prime, we have to consider the probability that these would have been witnesses if it were not.

  Maybe back then, it didn’t seem so strange to me to say, oh by the way when we figure out counterpossibles we can plug that solution into a decision theory.

  Now though, I’m more interested in decision theory than in counterpossibles. And I don’t think counterpossibles are essential to decision theory, so saying you’ll solve counterpossibles as a subproblem seems like a distraction.

  It would be one thing if counterpossibles were easy, so whatever you think of counterpossibles, it’s just the best way to solve decision theory. But… well, October 2027 will be the ten-year anniversary of the FDT paper.

  Who knows what I would have thought of this post if you had made it when FDT first came out. I mean, a lot of your post is just repeating the unsolved subproblems in the FDT paper itself. But many years later, my response to hearing that is not “yes, we know, that’s right in the paper” but “yes, that’s why FDT was a disappointment and I’m thinking about the next thing”.

• transhumanist_atom_understander 29 Jun 2026 16:46 UTC

  2 points

  0

  in reply to: Cole Wyeth’s comment on: The ar­ith­metic hi­er­ar­chy of real functions

  Okay. I’m just trying to get a sense of what kind of questions all of this is meant to answer. It sounds like we start with “SI is uncomputable, but is computable relative to some oracle”. Now we want to say “this machine I have built out of SI is still computable relative to that same oracle”. That kind of thing? And you’re saying here that while the machine built out of SI is not a function from reals to reals, we can prove these statements by classifying functions from reals to reals involved in its construction.

• transhumanist_atom_understander 29 Jun 2026 12:20 UTC

  2 points

  0

  on: The ar­ith­metic hi­er­ar­chy of real functions

  I’m not an AI researcher, and I haven’t studied AIXI, but I have read part of Hutter’s Universal Artificial Intelligence, enough to cover Solomonoff induction. Yet I’m feeling kind of lost as to the context where you would want to know where a function is in this hierarchy. Is it… like… when you do Solomonoff induction but the environment is something quantitative like physics?

  Oh, I see you cite this paper called “On the computability of Solomonoff induction and AIXI”. So I shouldn’t be thinking of “a function such as one used in Solomonoff induction’s environment”, I should be thinking of “a function such as Solomonoff induction”? But Solomonoff induction maps binary strings to rational probabilities… so should I be thinking of something like Solomonoff induction but getting real numbers as input? Oh, no, we want to characterize whether Solomonoff induction is computable assuming we have oracles for certain types of functions in this hierarchy. Right?

• transhumanist_atom_understander 26 Jun 2026 17:24 UTC

  LW: 5 AF: 3

  2

  AF

  in reply to: James Payor’s comment on: Payo­rian co­op­er­a­tion is easy with Kripke frames

  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.

• transhumanist_atom_understander 25 Jun 2026 19:58 UTC

  3 points

  0

  on: The worth­less­ness of vi­tamin D is mildly exaggerated

  According to Luxwolda et al.’s 2012 paper, “Traditionally living populations in East Africa have a mean serum 25-hydroxyvitamin D concentration of 115 nmol/​L”, traditionally living populations in East Africa have a mean serum 25-hydroxyvitamin D concentration of 115 nmol/​L.

  You go on to say that pale skin is evidence of selection pressure in favor of keeping vitamin D at this high level, suggesting health issues at lower levels. That seems plausible to me, but I want to consider another possibility, which is that issues from lower vitamin D levels may occur specifically in pregnancy.

  Looking at Luxwolda et al 2013, it’s 107 nmol/​L among non-pregnant adults, and 136 nMol/​L among pregnant women. Confidence intervals are wide, though pregnancy was significant in their regression, with an effect of +40 nmol/​L, confint (29, 52).

  I guess we already know it’s more important in pregnancy. I just bring it up because it may undermine the evolutionary speculation. You do mention:

  Some might argue that the purpose of fortification is to reach the severely deficient, or children, the elderly or pregnant mothers. Maybe!

  The same reasoning you’re applying to whoever’s fortifying food, apply it to natural selection. The need for very high levels in pregnancy may be sufficient to explain adaptations for keeping levels high (such as pale skin), even in the absence of harms at lower levels in non-pregnant adults.

  Of course this is itself just more evolutionary speculation, but it’s good to keep multiple possibilities in mind while speculating; the absence of evidence that would uniquely pin down one possibility is what makes it speculation.

• transhumanist_atom_understander 22 Jun 2026 20:36 UTC

  6 points

  0

  on: So­cial Dark Matter

  But it’s likely that even gay people in the 1950’s wouldn’t have guessed “one in every thirty adults,” which was the rate of self-report in Gallup polls in 2012, or “one in every fourteen adults” (!) which was the rate in 2022. In 1950, if you had told someone that the would likely pass within nodding distance of multiple non-straight people every single time they went to the grocery store, they would have assumed you were either crazy or slandering their hometown.

  Obligatory historical note that the Kinsey Report came out 1948. It gave the now widely quoted number that one in ten men are homosexual (and more bisexual). So it depends who in 1950 you’re talking to.

  I’m basing this on Wikipedia knowledge, I haven’t read Kinsey’s book.

  I also haven’t read the reactions to the Kinsey report. I suppose we don’t have to guess to what degree people were surprised or disbelieving; we could check.

• transhumanist_atom_understander 19 Jun 2026 0:09 UTC

  3 points

  0

  on: Lies, Damn Lies, and Fabri­cated Options

  Veldrina: Look at the sun! We need to hurry, it’s almost noon!

  Wrecan: It’d be better to go slowly and not break our necks.

  Veldrina: And it’d be even better to go really fast and still not break our necks, so let’s do that one.

  Order of the Stick

• transhumanist_atom_understander 18 Jun 2026 14:07 UTC

  2 points

  0

  on: Guardian An­gels: LLM Per­son­al­iza­tion for Pro­duc­tivity and Security

  I’ve been thinking something similar, but calling it an “exoself”, like from the Greg Egan novels.

• transhumanist_atom_understander 13 Jun 2026 21:22 UTC

  1 point

  0

  on: Tak­ing woo se­ri­ously but not literally

  This is a tangent, but regarding the meta-analysis you linked saying that open-label placebos still work, what do you think of the interpretation (which I favor) that they don’t work but the patients think they do? I think this is supported by the comparison of self-reported vs objective outcomes in the study.