That doesn't actually work. Take the Newcomb's problem. Suppose that your formal system quickly prove that A()≠1. Then it conclude that A()=1 ⇒ U()∈[0,0], on the other it end up concluding correctly that A()=2 ⇒ U()∈[1000,1000] so it end up two boxing. This is a possible behavior, even if the formal system used is sound, if one use rational intervals as you recommend. On the other hand, as I have shown, if you chose t sufficiently large the algorithm I recommend in my post will necessarily end up one boxing if the formal system used is sound. (using intervals was actually the first idea I had when coming to term with the problem detailed in the post, but it simply doesn't work.)
This is a possible behavior, even if the formal system used is sound, if one use rational intervals as you recommend.
Not if we use a Goedel statement/chicken rule failsafe like the one discussed in Slepnev's article you linked to.
On the other hand, as I have shown, if you chose t sufficiently large the algorithm I recommend in my post will necessarily end up one boxing if the formal system used is sound.
Edit: This part of my comment is wrong.
This is incorrect, as Zeno had shown more than 2000 years ago. It could be that your inference system genera...
In this article cousin_it describes an algorithm, using a Turing Oracle, which gives a working model of UDT. This algorithm seems to work well in the case of a utility function which takes natural numbers or rationals as values but, as I will explain, the algorithm doesn't actually work for utilities given by real numbers; I will also propose an algorithm which doesn't use an oracle and which seems to wield the correct answer given sufficient computing time.
One of the hidden assumptions in the initial post is that comparison of utilities is decidable (at least decidable with a Turing oracle): in step 3 of the algorithm you are supposed to return the action that corresponds to the highest utility found on step 2 of the algorithm, but if comparison of utilities isn't actually decidable you won't be able (in the general case) to do that and as it happens that equality of real numbers isn't decidable (even using an oracle). Also there are no canonical forms for real numbers like there are for natural or rational numbers so you can have a situation where the order relationship between different real numbers depends on the value of A().
A simple modification of the original algorithm can deal with this problem:
Why does this works? Because if the formal system used is sound, when the formal system proves that A()=a ⇒ U()≥u where a is the action which ends up actually being taken then U() must actually end up being at least u.
So for example, in the case of Newcomb's problem if t is sufficiently high it will eventually be proven that A()=1 ⇒ U()≥1 000 000 and so, if the formal system used is sound, the utility which ends up being received by the agent will have to be at least 1 000 000 which is of course only possible if the agent one boxes so that's what it will end up doing.