Just leaving a sanity check, even though I’m not sure about what the people who were more involved at the time are thinking about the 5 and 10 problem these days:
Yes, I agree this works here. But it’s basically CDT—this counterfactual is basically a causal do() operator. So it might not work for other problems that proof-based UDT was intended to solve in the first place, like the absent-minded driver, the non-anthropic problem, or simulated boxing.
It seems like you could use these counterfactuals to do whatever decision theory you’d like? My goal wasn’t to solve actually hard decisions—the 5 and 10 problem is perhaps the easiest decision I can imagine—but merely to construct a formalism such that even extremely simple decisions involving self-proofs can be solved at all.
I think the reason this seems to imply a decision theory is that it’s such a simple model that there are some ways of making decisions that are impossible in the model—a fair portion of that was inherited from the psuedocode in the Embedded Agency paper. I have an extension of the formalism in mind that allows an expression of UDT as well (I suspect. Or something very close to it. I haven’t paid enough attention to the paper yet to know for sure). I would love to hear your thoughts once I get that post written up? :)
Just leaving a sanity check, even though I’m not sure about what the people who were more involved at the time are thinking about the 5 and 10 problem these days:
Yes, I agree this works here. But it’s basically CDT—this counterfactual is basically a causal do() operator. So it might not work for other problems that proof-based UDT was intended to solve in the first place, like the absent-minded driver, the non-anthropic problem, or simulated boxing.
It seems like you could use these counterfactuals to do whatever decision theory you’d like? My goal wasn’t to solve actually hard decisions—the 5 and 10 problem is perhaps the easiest decision I can imagine—but merely to construct a formalism such that even extremely simple decisions involving self-proofs can be solved at all.
I think the reason this seems to imply a decision theory is that it’s such a simple model that there are some ways of making decisions that are impossible in the model—a fair portion of that was inherited from the psuedocode in the Embedded Agency paper. I have an extension of the formalism in mind that allows an expression of UDT as well (I suspect. Or something very close to it. I haven’t paid enough attention to the paper yet to know for sure). I would love to hear your thoughts once I get that post written up? :)
Sure, I can promise you a comment or you can message me about it directly.