 Call the resulting system “SDL+” for easy reference in this section. This says (roughly) that it is required that obligations be fulfilled. This is not a theorem of SDL (as we will see in  Section 2.3),  so SDL+ is a genuine strengthening of SDL. Furthermore, it makes a logically contingent proposition (i.e., that \(\OB p \rightarrow p)\) obligatory as a matter of deontic logic. SDL does not have this feature. With this addition to SDL, it is easy to prove \(\OB \OB p \rightarrow \OB p\), a formula involving an iterated occurrence of our main  operator.[23]  This formula asserts that if it is obligatory that \(p\) be obligatory, then \(p\) is obligatory. (Cf. “the only things that are required to be obligatory are those that actually  are”).[24]  It should be noted that these are often given an impersonal ought reading, so that \(\OB\)-U would be read as “It ought to be the case that if it ought to be the case that \(p\) then it  is)”.[25]