So, this post only deals with agent counterfactuals (not environmental counterfactuals), but I believe I have solved the technical issue you mention about the construction of logical counterfactuals as it concerns TDT. See: https://www.alignmentforum.org/posts/TnkDtTAqCGetvLsgr/a-possible-resolution-to-spurious-counterfactuals
I have fewer thoughts about environmental counterfactuals but think a similar approach could be used to make statements along those lines, i.e. construct alternate agents receiving a different observation about the world. I’m not sure any very specific technical problem exists with that, though—the TDT paper already talks about world model surgery.
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? :)