Let OB p denote "p is obligatory". Axiom OB-RE is (p ↔ q) → (OB p ↔ OB q). This axiom seems false to me (under the interpretation of obligation). For example, let p denote "don't lie to me" and q denote "hurt me". Suppose p Λ q, that is, you're not lying to me but you are hurting me. Then it is true that p ↔ q, since ⊤ ↔ ⊤. Suppose furthermore that OB p, that is, you're obligated not to lie to me. Then OB-RE would imply OB q, that is, you're obligated to hurt me. This clearly doesn't seem right. Am I interpreting this axiom incorrectly?
OB-RE: If p ↔ q is a theorem, then so is OBp ↔ OBq.
In other words, if p and q have the same truth value in each world, and each model, then they're basically the same proposition, and so one is obligatory iff the other is.
This holds in classical systems and almost characterizes them. Classical systems correspond to minimal models, those where what is necessary in a world x is just some collection of sets of world. Here a sets of worlds corresponds to a proposition p which holds in exactly those worlds.