As far as I can tell, this problem is an exercise in logical uncertainty. Consider an example agent A which makes a decision between, say, options a and b, with possible outcomes U=0, U=5, and U=10. In general, the agent uses its logical uncertainty estimator to compare the expected utilities 0*P(U=0|a)+5*P(U=5|a)+10*P(U=10|a) to 0*P(U=0|b)+5*P(U=5|b)+10*P(U=10|b). Of course, this causes a divide by zero error if A is certain of which action it will take. To avoid this, if A ever proves that it will take an action, it will immediately take a different action, regardless of the expected utility assigned to that action. So, if A ever proves what action it takes in advance of taking it, it will be wrong, and unsound. Thus if A is sound it cannot prove in advance what action it will take. In the $5 and $10 game, A will correctly assess the expected values, and choose the $10 because it is higher. It will be able to correctly assess the expected value of the $5 because it will hold nonzero probability of taking the $5 before it makes its decision. Why will it hold this nonzero probability, when $10 is the obvious choice? Because, since by Lob's theorem A can't prove itself sound, and if it is unsound, it might prove in advance that it will take the $10, and therefore take the $5 instead.
I don't know if this was clear but this is not a full answer, because logical uncertainty is hard and I'm just assuming agent A is somehow good at it.
Edit: How does A calculate the expected utility of another agent being in its position, when it is nontrivially embedded in its environment? Of course, if the agent is not embedded, the 5-10 problem ceases to be an issue(AIXI is not bothered by it), for precisely this reason: it's easy to see what the counterfactual world where the agent decided to take another action looks like, rather than in this case where that counterfactual world might be logically impossible or ill-defined.
5 dollars is better than 10 dollars
The 5-10 Problem is a strange issue in which an agent reasoning about itself makes an obviously wrong choice.
Our agent faces a truly harrowing choice: it must decide between taking $5 (utility 5) or $10 (utility 10).
How will our agent solve this dilemna? First, it will spend some time looking for a proof that taking $5 is better than taking $10. If it can find one, it will take the $5. Otherwise, it will take the $10.
Fair enough, you think. Surely the agent will concede that it can't prove taking $5 is better than taking $10. Then, it will do the sensible thing and take the $10, right?
Wrong.
Our agent finds the following the following proof that taking $5 is better:
Let's go over the proof.
Line 1: Taking $5 gives you $5.
Line 2: If F is true, then ~F->x is true for any x.
Line 3: If you find a proof that taking $5 gives you $5 and take $10 gives you $0, you'd take the $5.
Line 4: Combine the three previous lines
Line 5: Löb's Theorem
Line 6: Knowing that taking $5 gives you $5 and taking $10 gives you $0, you happily take the $5.
Simplified Example
To understand what went wrong, we'll consider a simpler example. Suppose you have a choice between drinking coffee (utility 1) and killing yourself (utility -100).
You decide to use the following algorithm: "if I can prove that I will kill myself, then I'll kill myself. Otherwise, I'll drink coffee".
And because a proof that you'll kill yourself, implies that you'll kill yourself, by Lob's Theorem, you will kill yourself.
Here, it is easier to see what went wrong-proving that you'll kill yourself is not a good reason to kill yourself.
This is hidden in the original 5-10 problem. The first conditional is equivalent to "if I can prove I will take $5, then I'll take $5".
Hopefully, it's now more clear what went wrong. How can we fix it?
Solution?
I once saw a comment suggesting that the agent instead reason about how a similar agent would act (I can't find it anymore, sorry). However, this notion was not formalized. I propose the following formalization:
We construct an agent A. Each time A makes a decision, it increments an internal counter n, giving each decision a unique identity. A uses the following procedure to make decisions: for each action a, it considers the agent Aa,n. Aa,n is a copy of A (from when it was created), except that if Aa,n would make a decision with id n, it instead immediately takes action a. Then, if A can prove any of these agents has the maximum expected utility, it chooses the action corresponding to that agent.