Your third question is the most interesting one. Many variants of UDT require logical counterfactuals, but nobody knows how to make them work reliably. MIRI folks are currently looking into logical inductors, exploration and logical updatelessness, so maybe Abram or Alex or Scott could explain these ideas. I’ve done some past work on formalizing logical counterfactuals in toy settings, like proof search or provability logic, which is quite crisp and probably the easiest way to approach them.
Your third question is the most interesting one. Many variants of UDT require logical counterfactuals, but nobody knows how to make them work reliably. MIRI folks are currently looking into logical inductors, exploration and logical updatelessness, so maybe Abram or Alex or Scott could explain these ideas. I’ve done some past work on formalizing logical counterfactuals in toy settings, like proof search or provability logic, which is quite crisp and probably the easiest way to approach them.