Your proposal seems to be equivalent to something I proposed a while ago: have A try to find a function U’ such that U() is provably equal to U’(A()), then return argmax(U’). By itself this doesn’t even solve Newcomb’s problem (never mind ASP), because there are many possible U’ satisfying the above condition, and no easy way to guarantee that the right one will be found first. There could be nasty Loebian traps. For example, if your order of proof enumeration is unlucky enough, you could find U’=”return 1000″ with no dependence on A at all, then two-box and make that equation true.
You mean, the U’, for which U’(A()) is provably equal to U() depends on the order in which you enumerate U’-s? Hmm, counterintuitive, but it makes sense… A() with a different order would be a different A(), so it would produce a different U’...
Just as a wild shot, what would happen if you try every possible ordering of U’-s and then choose the ordering that produces the best result? Let’s say there is a maximal length for U’ that you are willing to consider, and you have a loop iterating over all possible orderings of U’-s of up to that length. In each iteration of the loop you try to prove things in the specific order, find the argmax, store it, restore the proof system back to its initial state, and go to the next iteration. When everything finishes, use the best found ordering.
I expect, the results will now depend on the order in which the orderings are considered...
For example, if your order of proof enumeration is unlucky enough, you could find U’=”return 1000″ with no dependence on A at all, then two-box and make that equation true.
I wonder if reflection on your own inference system could make things like this go away...
You need to find a simple U’, such that you can construct its argmax. The wrong/useless U’ are just those you can’t compute argmax of (except for the cases like one you point out, which is the same problem for normal ADT, losing control over U). U’ is what I called “utility function” (inferred from definition of utility value U) in this post. Finding moral arguments [A=A1 ⇒ U=U1] is specifically a method for inferring a utility function, but the goal is to find argmax-able U’ (dependence of utility value on your decision).
Your proposal seems to be equivalent to something I proposed a while ago: have A try to find a function U’ such that U() is provably equal to U’(A()), then return argmax(U’). By itself this doesn’t even solve Newcomb’s problem (never mind ASP), because there are many possible U’ satisfying the above condition, and no easy way to guarantee that the right one will be found first. There could be nasty Loebian traps. For example, if your order of proof enumeration is unlucky enough, you could find U’=”return 1000″ with no dependence on A at all, then two-box and make that equation true.
You mean, the U’, for which U’(A()) is provably equal to U() depends on the order in which you enumerate U’-s? Hmm, counterintuitive, but it makes sense… A() with a different order would be a different A(), so it would produce a different U’...
Just as a wild shot, what would happen if you try every possible ordering of U’-s and then choose the ordering that produces the best result? Let’s say there is a maximal length for U’ that you are willing to consider, and you have a loop iterating over all possible orderings of U’-s of up to that length. In each iteration of the loop you try to prove things in the specific order, find the argmax, store it, restore the proof system back to its initial state, and go to the next iteration. When everything finishes, use the best found ordering.
I expect, the results will now depend on the order in which the orderings are considered...
[EDIT: Yes, this is stupid. Please disregard]
I wonder if reflection on your own inference system could make things like this go away...
That would be cool. How?
You need to find a simple U’, such that you can construct its argmax. The wrong/useless U’ are just those you can’t compute argmax of (except for the cases like one you point out, which is the same problem for normal ADT, losing control over U). U’ is what I called “utility function” (inferred from definition of utility value U) in this post. Finding moral arguments [A=A1 ⇒ U=U1] is specifically a method for inferring a utility function, but the goal is to find argmax-able U’ (dependence of utility value on your decision).