Yes, logical uncertainty clearly needs to be dealt with, although I'd be interested in seeing a proper statement of the problem in its general form. Diagrams like this are a useful tool because you can give an uncontroversial correct answer to "what is the optimal strategy for diagram X?" but they don't answer the underlying questions unless you also have a theory that says the diagram should be drawn THIS way and not THAT way.
I think the diagrams I made are valid; the ASP one in particular is justified pretty well by the exact same reasoning that goes into Eliezer's TDT. The LCM one relies pretty heavily on being able to assign a prior probability of 0.5 to both possibilities, but without justification for something else I see little other choice than to go for a 50/50 split.
Also, yes; I do think that ASP in its standard form is underspecified, unlike Gary's transparent Newcomb's problem.
In terms of the proof-searching formalism you bring up in your post on ASP, you have these issues:
1) If proofs of one-boxing and two-boxing are both valid, which one gets found first?
2) If no proof can be found at all, what does the predictor do?
I think the straightforward way to resolve this issue with ASP is to state that the predictor only searches for proofs up to length N that the agent one-boxes, and fills both boxes if and only if it finds such a proof. This resolves the issue in the exact same way that "FairBot" does in the "Robust Cooperation" paper, right? Also, it's essentially analogous to Gary's transparent Newcomb's, because searching for a proof that the agent one-boxes is pretty much the same idea as simulating what they would do if both boxes were filled.
Of course, it's sufficiently well-specified in your original ASP post because you also specified an algorithm for the agent; in this case the agent happens to find a proof that two-boxing leads to $1000 and a "spurious" proof that one-boxing leads to $0, both of which do indeed turn out to be true because that agent ends up two-boxing.
If proofs of one-boxing and two-boxing are both valid, which one gets found first?
They can't be both valid, because only one of the two statements is true. We assume that the predictor's formal theory is sound (doesn't prove false statements).
If no proof can be found at all, what does the predictor do?
Right, that's the underspecified part. I guess the predictor should fill only one box in this case.
...I think the straightforward way to resolve this issue with ASP is to state that the predictor only searches for proofs up to length N that the agent on
This post was inspired by Benja's SUDT post. I'm going to describe another simplified model of UDT which is equivalent to Benja's proposal, and is based on standard game theory concepts as described in this Wikipedia article.
First let's define what is a "single player extensive-form game with chance moves and imperfect information":
Now let's try using that to solve some UDT problems:
Absent-Minded Driver is the simplest case, since it's already discussed in the literature as a game of the above form. It's strange that not everyone agrees that the best strategy is indeed the best, but let's skip that and move on.
Psy-Kosh's non-anthropic problem is more tricky, because it has multiple players. We will model it as a single-player game anyway, putting the decision nodes of the different players in sequence and grouping them together into information sets in the natural way. The resulting game tree is complicated, but the solution is the same as UDT's. As a bonus, we see that our model does not need any kind of anthropic probabilities, because it doesn't specify or use the probabilities of individual nodes within an information set.
Wei Dai's coordination problem is similar to the previous one, but with multiple players choosing different actions based on different information. If we use the same trick of folding all players into one, and group the decision nodes into information sets in the natural way, we get the right solution again. It's nice to see that our model automatically solves problems that require Wei's "explicit optimization of global strategy".
Counterfactual Mugging is even more tricky, because writing it as an extensive-form game must include a decision node for Omega's simulation of the player. Some people are okay with that, and our model gives the right solution. But others feel that it leads to confusing questions about the nature of observation. For example, what if Omega used a logical coin, and the player could actually check which way the coin came up by doing a long calculation? Paying up is probably the right decision, but our model here doesn't have enough detail.
Finally, Agent Simulates Predictor is the kind of problem that cannot be captured by our model at all, because logical uncertainty is the whole point of ASP.
It's instructive to see the difference between the kind of UDT problems that fit our model and those that require something more. Also it would be easy to implement the model as a computer program, and solve some UDT problems automatically. (Though the exercise wouldn't have much scientific value, because extensive-form games are a well known idea.) In this way it's a little similar to Patrick's work on modal agents, which made certain problems solvable on the computer by using modal logic instead of enumerating proofs. Now I wonder if other problems that involve logical uncertainty could also be solved by some simplified model?