An intuitionistic reformulation of Mally's deontic logic (Q373016)

\textit{E. Mally}'s [Grundgesetze des Sollens: Elemente der Logik des Willens. Graz: Leuschner und Lubensky (1926)] original axioms for a deontic logic failed because, being based on classical logic, \(OA\leftrightarrow A\) is derivable. This paper considers adding those axioms to a base of intuitionistic logic, along with another axiom (A6), \(O(A\vee\neg A)\), to form the system ID. This is equivalently axiomatized by adding just the axiom \(OA\leftrightarrow\neg\neg A\) to Heyting's H. ID too fails as a deontic logic. Although \(OA\leftrightarrow A\) is not derivable, \(OA\leftrightarrow\neg\neg A\) is, as is \(OA\leftrightarrow PA\), with \(P\) the dual of \(O\), and also \(A\to OA\), and (not mentioned by the author) \(O\neg A\leftrightarrow \neg A\). The author likewise does not consider that neither (A6) nor \(OA\leftrightarrow\neg\neg A\) would seem to have any intuitionistic credentials, if \(O\) were interpreted as a deontic operator. The author does think ID has some interest as a lax logic.