 Assume again that we have a language of classical propositional logic (PC) with an infinite set of propositional variables, the truth functional operators \(\neg\) and \(\rightarrow\) (and perhaps any of &amp;, \(\vee\) and \(\leftrightarrow\) as well), and the operator, \(\OB\). SDL is then often axiomatized as  follows:[17]