Since the agent can deduce (by low-level simulation) what the predictor will do, the agent does not regard the prediction outcome as contingent on the agent’s computation.
What happens if the UDT agent generates a proof that using any proof longer than N results in only $1000? Is that level of self-reference allowed?
What happens if the UDT agent generates a proof that using any proof longer than N results in only $1000? Is that level of self-reference allowed?
Yes, but current versions of the decision theory can’t respond to this conclusion of the meta-proof by not generating the proof, and really the problem is not that the agent generates the proof, but that it uses it. It could generate it and then ignore the result (based on the meta-proof), which would result in success, but this level of decision rules is not currently supported.
I was thinking that if proofs are allowed to use their own length as a premise, then the expected payoff from each proof would depend on the length of that proof. Both agent and predictor can prove that any proof which is too long results in $1000 or $0, therefore the agent would choose a shorter proof that gives $1000000.
I’d really like to have a decision theory that would do such things automatically when the situation calls for it. Unfortunately, the one in my formalization doesn’t :-(
What happens if the UDT agent generates a proof that using any proof longer than N results in only $1000? Is that level of self-reference allowed?
Yes, but current versions of the decision theory can’t respond to this conclusion of the meta-proof by not generating the proof, and really the problem is not that the agent generates the proof, but that it uses it. It could generate it and then ignore the result (based on the meta-proof), which would result in success, but this level of decision rules is not currently supported.
I was thinking that if proofs are allowed to use their own length as a premise, then the expected payoff from each proof would depend on the length of that proof. Both agent and predictor can prove that any proof which is too long results in $1000 or $0, therefore the agent would choose a shorter proof that gives $1000000.
I have no idea whether that’s correct, though.
I’d really like to have a decision theory that would do such things automatically when the situation calls for it. Unfortunately, the one in my formalization doesn’t :-(