Above, action and utility are defined separately, with axioms that generally don't refer to each other. Axioms that define action don't define utility, and conversely. Moral arguments, on the other hand, define utility in terms of action. If we are sure that one of the moral arguments proved by the agent refers to the actual action (without knowing which one; if we have to choose an actual action based on that set of moral arguments, this condition holds by construction), then actual utility is defined by the axioms of action (the agent) and these moral arguments, without needing preference (axioms of utility).

I'm a little confused here. Here is my understanding so far:

The agent has an axiom-set S and rules of inference, which together define the agent's theory. Given S and some computational constraints, the agent will deduce a certain set M of moral arguments. The moral arguments contain substrings of the form "U = U1". The largest constant U1* appearing in such substrings of the moral arguments in M is, by definition, the actual utility. The definition of "actual utility" that I just wrote (which is in the metalanguage, not the agent's language) is the preference.

In this sense, preference and actual utility are defined by all the axioms in S taken together. Similarly, the actual action is defined by all of S. So, what are you getting at when you talk about having one set of axioms define action while another set of axioms defines utility?