New Comment
1 comment, sorted by Click to highlight new comments since: Today at 11:33 PM

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 and utilities . At stage , the agent sees if PA proves , and returns 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!