transhumanist_atom_understander comments on Payorian cooperation is easy with Kripke frames

[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.