(If optimal utility is irrational, there doesn’t exist highest rational utility value u in valid statements of the form A()=a ⇒ U()≥u, in which case the time limitation must be used, and action won’t necessarily be optimal.)
Rationals are dense in the reals so there are always a rational value between any two real numbers. So for example, if it can be proven in your formal system that A()=1 ⇒ U()=π and this happen to be the maximal utility attainable, there will be a rational number x greater than the utility that can be achieved by any other action and such that x≤π, so you will be able to prove that A()=1 ⇒ U()≥x and so the first action will end up being taken because by definition of x it is greater than the utility that can be obtained by taking any other action.
I see. Still, time limit is not the criterion you want to use here, it would be better to establish rational interval bounds for utility of each possible action, and once the intervals are disjoint, you act. This way, the action is always optimal if all utilities are different, while if you just use the time limit, it could arrive before different actions could be evaluated with enough precision.
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 generates an infinite sequence of statements of the form A()=1 ⇒ U()≥Si with sequence {Si} tending to, say, 100, but with all Si<100, so that A()=1 loses to A()=2 no matter how large the timeout is.
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.
This is incorrect, as Zeno had shown more than 2000 years ago. It could be that your inference system generates an infinite sequence of statements of the form A()=1 ⇒ U()≥Si with sequence {Si} tending to, say, 100, but with all Si<100, so that A()=1 loses to A()=2 no matter how large the timeout is.
That’s why you enumerate all proofs of statement of the form A()=a ⇒ U()≥u (where u is rational number in canonical form). It’s a well known fact that it is possible to enumerate all the provable statements in a given formal system without skipping any.
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.
There are some subtleties about doing this in the interval setting which made me doubt that it could be done, but after thinking about it some more I must admit that it is possible.
But I think that my algorithm for the non-oracle setting is still valuable.
But I think that my algorithm for the non-oracle setting is still valuable.
I think it’s a useful trick not so much because it doesn’t require oracles, but because it doesn’t require a Goedel statement (chicken rule), even though it depends on choosing a time limit, while the algorithm with Goedel statement doesn’t.
(If optimal utility is irrational, there doesn’t exist highest rational utility value u in valid statements of the form A()=a ⇒ U()≥u, in which case the time limitation must be used, and action won’t necessarily be optimal.)
Rationals are dense in the reals so there are always a rational value between any two real numbers. So for example, if it can be proven in your formal system that A()=1 ⇒ U()=π and this happen to be the maximal utility attainable, there will be a rational number x greater than the utility that can be achieved by any other action and such that x≤π, so you will be able to prove that A()=1 ⇒ U()≥x and so the first action will end up being taken because by definition of x it is greater than the utility that can be obtained by taking any other action.
I see. Still, time limit is not the criterion you want to use here, it would be better to establish rational interval bounds for utility of each possible action, and once the intervals are disjoint, you act. This way, the action is always optimal if all utilities are different, while if you just use the time limit, it could arrive before different actions could be evaluated with enough precision.
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.)
Not if we use a Goedel statement/chicken rule failsafe like the one discussed in Slepnev’s article you linked to.
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 generates an infinite sequence of statements of the form A()=1 ⇒ U()≥Si with sequence {Si} tending to, say, 100, but with all Si<100, so that A()=1 loses to A()=2 no matter how large the timeout is.
That’s why you enumerate all proofs of statement of the form A()=a ⇒ U()≥u (where u is rational number in canonical form). It’s a well known fact that it is possible to enumerate all the provable statements in a given formal system without skipping any.
There are some subtleties about doing this in the interval setting which made me doubt that it could be done, but after thinking about it some more I must admit that it is possible.
But I think that my algorithm for the non-oracle setting is still valuable.
I think it’s a useful trick not so much because it doesn’t require oracles, but because it doesn’t require a Goedel statement (chicken rule), even though it depends on choosing a time limit, while the algorithm with Goedel statement doesn’t.
You’re right, there is no problem here, as long as you enumerate everything.