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.
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.