 Although ID is unacceptable as a system of deontic logic, it does make sense as a system of lax logic, as we will now show. Lax logic is used in the areas of hardware verification in digital circuits and access control in secure systems, where ! expresses a notion of correctness up to constraints. The term “lax” was chosen “to indicate the looseness associated with the notion of correctness up to constraints” (Fairtlough and Mendler 1997, p. 3). There is a considerable literature on lax logic (Goldblatt 2011).