 In identifying the Traditional Definitional Scheme (TDS) in  Section 1.2,  we noted that it was widely recognized that we could have taken another notion than obligation from our first four primary normative statuses and defined the rest in terms of that one. So it is expected that we should be able to generate the corresponding equivalences derivatively from the scheme we did settle on, where \(\OB\) is taken as primitive. For example, it is obviously desirable to have \(\OB p \leftrightarrow \neg \PE \neg p\) as part of the Traditional Scheme, as this expresses the equivalence between what would have been definiens and definiendum had “\(\PE\)” been taken as primitive. However, this equivalence is not thus far derivable. For \(\OB p \leftrightarrow \neg \PE \neg p\) is definitionally equivalent to \(\OB p \leftrightarrow \neg \neg \OB \neg \neg p\), that is, \(\OB p \leftrightarrow \OB \neg \neg p\), but the latter formula is not a tautology, so we cannot in turn derive \(\OB p \leftrightarrow \neg \PE \neg p\). So more is presupposed in the Traditional Scheme than what has been noted above. A natural thought is a rule of inference needs to be added, one allowing for the replacement of provably equivalent formulas in the context of “\(\OB\)”, namely \(\OB\)-RE in Corollary 2 above Let’s take this to be tacitly part of the Traditional Scheme.