Deontic logic often contains the axiom
□(p → q) → (□p → □q)
where □ is being used for "it is obligatory that".
This axiom strikes me as odd. It reads "If it is obligatory that p implies q, then if it is obligatory that p, then it is obligatory that q. For example, let
p = X has the ability to save Y's life
q = X saves Y's life
With these definitions, we haves for the premise of the axiom:
A. It is obligatory that if X has the ability to save Y's life, then x saves Y's life.
According to the axiom, A implies B:
B. If it is obligatory that X has the ability to save Y's life, then it is obligatory that X saves Y's life.
Isn't that an odd conclusion? In this case, □p doesn't even make sense, and in general the obligatoriness of a the premise of an implication doesn't seem related to the obligatoriness of the conclusion. From A, shouldn't we instead conclude C?
C. If X has the ability to save Y's life, then it is obligatory that X saves Y's life.
This corresponds not to
□(p → q) → (□p → □q)
but to
□(p → q) → (p → □q)
which strikes me as a much more intuitive axiom. I'm certain that this has been explored by someone, but the SEP article on deontic logic doesn't mention it (although it does discuss problems with this axiom and other solutions). Can anyone else explain why my suggestion doesn't work or give me references to discussions?