I'm wondering if you're assuming soundness relative to the natural semantics about A

You're right. Misha already pointed that out and I edited the post.

For all actions a, if there is some u such that [A() = a ⇒ U() = u] and u > 0, else add [A() = a ⇒ U() = 0] to the axioms of S

Yeah, such a variation would work, but I'm uncomfortable calling A the optimal algorithm in a universe where some actions don't have provable utility. Such universes often arise from non-symmetric multiplayer games and I'd rather not insinuate that I have a good solution for those.