I think I missed the indirection required to use Lob's theorem (which I thought was about not being able to prove that a statement is unprovable, not about proving false things - that is, for our formal systems, we accept incompleteness but not incorrectness).

Mainly I don't see where you have the actual proposition setup in your "proof" - the knowledge that you're choosing between $5 and $10, not between $5 and "something else, which we are allowed to assume is $0". If you don't know (or your program ignores) that you will be offered $10 iff you reject the $5, you'll OF COURSE take the $5. You can test this in real humans: go offer someone $5 and don't say anything else. If they turn it down, congratulate them on their decision-making and give them $10. If they take the $5, tell them they fell victim to the 5-10 problem and laugh like a donkey.

FactorialCode's comment _is_ an application that shows the problem - it's clearly "among things I can prove, pick the best", not "evaluate the decision of passing up the $5". I'd argue that it's _ALSO_ missing the important part of the setup - you can prove that taking $10 gives you $10 as easily as that $5 gives you $5, and the "look for proof" is handwaved (better than absent) without showing why the proof.

I suggested a similar approach in deconfusing logical counterfactuals [LW · GW] where we erase information about the agent so that we end up with multiple possible agents, though I wouldn't be surprised if other people have also tried asking their agent to ask about how other agents reason. Your approach is different in that the original agent isn't included among the set of agents considered and that seems like a useful adaption that I hadn't considered as long as we can provide appropriate justification. I also provide some more just

Anyway, it's good to see someone else thinking along a similar (but different) track and I'd be curious to hear what you think about my approach.

If I can try and make your solution concrete for the original 5-10 problem. Would it look something like this?

A() := 
    let f(x) :=
         Take A() := x as an axiom instead of A() := this function
         Take U() := to be the U() in the original 5-10 problem
         Look for a proof of "U() = y"
         return y
    in 
         return argmax f(x) 
    where x in {5,10}

A() := 10
U() := 
     if A() = 10
         return 10
     if A() = 5
         return 5

U() = 0

[A() = 10 -> U() = x] & [A() = 5 -> U() = y ]

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.

What was wrong with specifying an agent that uses "[decision theory] unless it's sure it'll make a decision, then it makes the opposite choice"?