Here's my meager attempt at contribution. And my apologies for not knowing LaTeX.

if exists a,b: provable([A(U,i)=C implies pi(i)(U())=a] and [A(U,i)=D implies pi(i)(U())=b] and [a>b]):
C
else:
D

You can do a lot better than this. Consider, for instance:

if exists a: provable([A(U,i)=C implies p(i)(U())>=a] and [A(U,i)=D implies pi(i)(U())<=a]):
C
else:
D

Consider the set S of all sets S(k) such that provable(A(U,i)=C implies pii(U()) is in S(k)). Then A(U,i)=C implies pii(U()) is in intersection(S). I don't know much about formal arithmetic, so I couldn't say whether it is necessary true that provable(A(U,i)=C implies pi(i)(U()) is in intersection(S)). But if that is true, then intersection(S)) is in S, and thus there exists a unique most specific S(k) such that provable(A(U,i)=C implies pi(i)(U()) is in S(k)). If it is possible in formal arithmetic to identify this set, then you can establish a utility function over such minimal sets of possible values of pi(i)(U()) implied by A(U,i)=C. For example, if that set is finite, the its utility could just be the average of its members. And then you could do the same sort of thing for A(U,i)=D and compare the utilities of the resulting sets of possibilities. This would essentially give you a single utility value for each choice, and you wouldn't get stuck if you can't prove that each output of A implies some unique value of pi(i)(U()).

What is the correct generalization of that can choose between n actions, and not just two? How about infinitely many actions?

For finite sets of actions, one possibility is that you can compare every pair of actions, giving you a partial ordering of the set, and then you could choose a maximal element. Alternatively, if my earlier idea for improving on the comparisons works, you can assign a utility to each possible action, so you can just choose the best one. If you have infinitely many possible actions, this will of course give you problems, since it can turn into a "name the biggest number" contest.

Note that we are intending to talk about agents that optimize over how U() works, but your framework also allows the creation of agents that optimize over how pi(i)(_) works. For instance, consider the following scenario:
U(): return (0, 0)
pi(i)(a,b): return 1 if A(U,i)=C, else 0
In this case, A(U,i) would output C, but not because it would imply anything about U. It might make sense to have some computability restriction on pi so that all such agents will actually be optimizing the world function rather than their own utility functions.