[eli_gottlieb]

Fair enough, and that's been one of the approaches to paraconsistency and inconsistency in modal logic, too. Of course, from a theorem-proving perspective, it's utterly useless, as with a proof-checker, at some point I need to escape the monadic container and get back into `Prop`.