transhumanist_atom_understander

Karma: 668

transhumanist_atom_understander 1 Sep 2026 13:11 UTC
1 point
0
in reply to: Zac Hatfield-Dodds’s comment on: Is there only one FairBot?
Cool.

I was hoping there was some way to enumerate inequivalent bots. I guess by modal depth within a rank, then by rank.

is an interesting bot to consider.

The way I would put the match with PrudentBot is this. It takes to prove that FairBot defects against DefectBot, so that’s what PrudentBot uses to test that match. But this isn’t actually enough to show this new bot defects against DefectBot.

Which is related to unexploitability. The new bot is unexploitable. But if you can’t prove it defects against DefectBot, then you can’t prove it’s unexploitable. So it’s not provably unexploitable in .

transhumanist_atom_understander 30 Aug 2026 19:12 UTC
2 points
0
in reply to: Pawn’s comment on: Tales of rebellion against externally-opaque meritocracies
You know, it occurs to me that the Barcan formula is by Ruth Barcan Marcus, who is mentioned in the post, in the Dennet quote:

There were nominating speeches and rebuttals, the most memorable of which was by Ruth Marcus, whose Yale colleague John Smith, a philosopher of religion and a theologian, was the pluralists’ candidate. She explicitly trashed his whole career, his character, his books. I had never heard a philosopher speak so ill of a colleague in public, and seldom in private.

So not just a (minor) example of the significance of modal logic from the perspective of mathematics, but from specifically the person Dennet was talking about.

transhumanist_atom_understander 30 Aug 2026 18:29 UTC
1 point
0
in reply to: Pawn’s comment on: Tales of rebellion against externally-opaque meritocracies
Maybe I didn’t get across the connection to Zeilberger, it’s not that he’s doing or opining about logic, it’s that he’s developing decision procedures, so the disappointing yield from that research program suggests that maybe decision procedures aren’t so important. Like, reaching to something more basic than Zeilberger’s work for an example, there’s Gosper’s algorithm—Gosper’s paper was called “Decision procedure for indefinite hypergeometric summation”. Symbolic computation in the Zeilberger style is developing decision procedures for narrow classes of mathematical questions. The connection to irrationality isn’t about logic, it’s Zeilberger’s thought that since we have decision procedures for questions about hypergeometric sums, we should be able to use them somehow to search for hypergeometric sums to use in irrationality proofs (inspired by how Apéry used handmade hypergeometric sums to prove irrationality of ζ(3)).

transhumanist_atom_understander 30 Aug 2026 17:14 UTC
3 points
2
in reply to: Pawn’s comment on: Tales of rebellion against externally-opaque meritocracies
They’re decidable fragments.

It seems to me that should make a big difference, but apparently that doesn’t count for as much as I thought, because symbolic computation (also really a collection of decision procedures) hasn’t lived up to the grand promise that Zeilberger sold us. (A modest example: computer algebra systems have been used to do Apéry’s proof of the irrationality of ζ(3), but despite Zeilberger’s efforts I can’t think of any big irrationality proofs that were discovered with symbolic computation.)

transhumanist_atom_understander 29 Aug 2026 22:56 UTC
5 points
0
in reply to: Canaletto’s comment on: Is there only one FairBot?
The definitions of “modal agent”, “rank”, and “unexploitable” are in the paper.

transhumanist_atom_understander 29 Aug 2026 22:55 UTC
1 point
0
on: Tales of rebellion against externally-opaque meritocracies

Likewise, I suspect that the analytic philosophers of 1979 could trounce the continental philosophers at, I dunno, externally-legible tests vaguely related to philosophical reasoning, like the LSAT. If so, the rebels didn’t care.

Maybe an example is the use of logic in computer science.

I keep thinking the deep theory of modal logic developed in philosophy departments should have some impact on math, but it doesn’t seem to have happened yet, as far as I know.

Is there only one FairBot?

transhumanist_atom_understander29 Aug 2026 20:56 UTC

40 points

11 comments1 min readLW link

transhumanist_atom_understander 21 Aug 2026 13:27 UTC
1 point
0
in reply to: transhumanist_atom_understander’s comment on: A failed solution to open-source game theory
I was thinking about how to make an analogue of the betrayal-based FairBot definition from the provability setting.

I think it requires being able to condition on the results of particular matches. We could do that in Python with a Judge object. The Judge runs matches, like this:
```
class EpsilonGroundedFairBot:
    def __call__(self, opponent, judge):
        if random.random() < ε:
            return C
        return judge.run(opponent, self)
```
judge.run checks some internal lookup table for a result for the match, and if it finds it, returns that result. Otherwise it actually runs the bot. In this case, we don’t add to the lookup table.

We only add to the lookup table to condition on results of particular matches. Using the conditioning idea to translate the idea of betrayal, I end up with something superficially like NiceProbeSimulator, but which I’ll call ConditioningFairBot:
```
class ConditioningFairBot:
    def __call__(self, opponent, judge):
        newJudge = judge.condition(self, opponent, C)
        return newJudge.run(opponent, self)
```
judge.condition(x, y, r) returns a new Judge, which will always say that x does r against y, just by checking its lookup table.

Seems to me like ConditioningFairBot should achieve efficient cooperation with another ConditioningFairBot. After two recursions, we hit the lookup table.

transhumanist_atom_understander 21 Aug 2026 1:52 UTC
3 points
0
in reply to: Andrew_Critch’s comment on: Modal Fixpoint Cooperation without Löb’s Theorem
Can’t believe I just noticed this comment thread… yeah, I got stuck for a while when doing the same thing because I had and needed . Wish I could say I at least had the satisfaction of figuring it out myself, but in reality Claude pointed out to me that follows.

Anyway, can go in the other direction too: if PA derives , it also derives , for any PA formulas and . The modal logic derivation actually starts from , but that’s fine; our premise is that PA derives it, so PA also derives that it’s provable.

transhumanist_atom_understander 20 Aug 2026 14:25 UTC
3 points
0
in reply to: James Payor’s comment on: Inside the mind of a fair player cooperating
It’s weird for me to think of betrayal as entirely my opponent’s choice, since it’s a conjunction of two things, their decision to defect, and a proof of my cooperation (which I suppose that I control, not them). Like… yeah it’s up to them to betray me, but it’s up to me whether they have the opportunity.

Thinking of time… if you’re fair and you defect, that’s because yesterday I betrayed you. So yesterday, there was a proof of your cooperation and I defected.

What’s it mean that yesterday there was a proof of your cooperation? Well I’m treating yesterday as what’s possible, so let’s translate “you provably cooperate” to “it’s not possible you defect”. So if there was a proof of your cooperation yesterday, that just means it’s not the case that you defected the day before yesterday.

That actually gives a “dynamic” proof of cooperation when we’re both fair (in the betrayal sense). It’s a proof by contradiction, starting by assuming you defect. Why did you defect? Because yesterday, I betrayed you—I defected, even though you hadn’t defected the day before. So why did I defect? Because the day before that, you betrayed me. So we have a contradiction: did you defect two days ago or not? This is a straight translation of the proof using possible world semantics.

I originally wanted to translate “provably cooperate” as “had always previously cooperated”. This would correspond to transitivity in possible world semantics. I guess you could translate provability in terms of the word “before”, which could either mean “immediately before” (not transitive), or “any time before” (transitive). We have transitivity in provability logic but don’t actually need it for this proof about betrayal. With transitivity, original FairBot is not Tit-For-Tat but an unforgiving bot that, once someone defects against it, defects back forever.

transhumanist_atom_understander 19 Aug 2026 19:28 UTC
1 point
0
on: A failed solution to open-source game theory
What I call “the new definition of fairness” seems like the provability version of what you call “niceness”.

What a coincidence that we made these posts within two hours of each other.

Inside the mind of a fair player cooperating

transhumanist_atom_understander19 Aug 2026 14:53 UTC

40 points

2 comments3 min readLW link

transhumanist_atom_understander 13 Aug 2026 17:23 UTC
3 points
0
on: Free will is like temperature
Lately I’ve been thinking about proof-based agents: agents that search for proofs in Peano Arithmetic of the consequences of their actions, and decide based on that.

I think when you formulate them right (which would be very different from the last attempt), they have a kind of “free will” that comes from this kind of underspecification.

Specifically: the proof system used to derive stuff like “if I take action A, then the environment will be in state S” cannot derive stuff like “I take action A”.

The model of the agent where I think this works out is it is doing a random proof search. Or a pseudorandom proof search, and “I take action A” means “I take action A regardless of the seed for the random number generator”. That is, the proofs are actually about an ensemble of agents with different RNG seeds.

Since the proof system can’t prove its consistency, it can’t prove that all proof searches will come up with the same result.

This incompleteness about the antecedents of our counterfactuals looks a bit like free will, but it requires considering this ensemble of agents, where we specify they’re doing a proof search but leave out the “microscopic” detail of the RNG seed.

This is in contast to functional decision theory, where we work with a complete specification of the agent, and thus need counterpossible implications, where the antecedent is provably false.

I’m hoping to work out the details and post more about it soon. For now you can believe me or not that this is a coherent theory.

But yeah, I think underspecifying “microscopic” details in a “macroscopic” description is where you get something like free will.

People always say randomness doesn’t help with free will, but it seems to me there’s this weird middle path, where your actions are not determined (in PA), but still not arbitrary (becaue they’re determined in PA+consistency of PA).

An argument of Parfit’s reconsidered with logical decision theory

transhumanist_atom_understander5 Aug 2026 20:47 UTC

12 points

14 comments5 min readLW link

transhumanist_atom_understander’s Shortform

transhumanist_atom_understander24 Jul 2026 18:16 UTC

5 points

1 comment1 min readLW link

transhumanist_atom_understander 24 Jul 2026 18:16 UTC
3 points
0
on: transhumanist_atom_understander’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: Payorian cooperation 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 “Payorian FairBot” was just the original 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 “Payorian FairBot” was just the original 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 “Payorian FairBot” was just the original 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

Is there only one FairBot?

In­side the mind of a fair player cooperating

An ar­gu­ment of Parfit’s re­con­sid­ered with log­i­cal de­ci­sion theory

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

Inside the mind of a fair player cooperating

An argument of Parfit’s reconsidered with logical decision theory

transhumanist_atom_understander’s Shortform