The following variant of modal UDT seems to satisfy the notion of injectivity by using the “time of decidability”, but I’m not sure if it will work:
Consider a sequence of possible actions an and utilities un. At stage n, the agent sees if PA proves □n(U()≥un)∧¬□n−1(U()≥un), and returns an if it succeeds.
I haven’t yet tried this out with the model checker, but it’s an intriguing idea; you don’t even need to explicitly include the proposed action in the thing you’re trying to prove!
The following variant of modal UDT seems to satisfy the notion of injectivity by using the “time of decidability”, but I’m not sure if it will work:
Consider a sequence of possible actions an and utilities un. At stage n, the agent sees if PA proves □n(U()≥un)∧¬□n−1(U()≥un), and returns an if it succeeds.
I haven’t yet tried this out with the model checker, but it’s an intriguing idea; you don’t even need to explicitly include the proposed action in the thing you’re trying to prove!