A closer look at modal bargaining agents

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 $a_n$ and utilities $u_n$. At stage $n$, the agent sees if PA proves ${\square }_n\left(U\right()\ge u_n)\wedge \neg {\square }_{n-1}\left(U\right()\ge u_n)$, and returns $a_n$ 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!