Supplement to Deontic Logic

Two Simple Proofs in Kd

First consider the very simple proof of OBd:

By PC, we have dd as a theorem. Then by R2, it follows that □(dd), that is, OBd.

Next consider a proof of NC, OBp → ~OB~p. As usual, in proofs of wffs with deontic operators, we make free use of the rules and theorems that carry over from the normal modal logic K. Here it is more perspicuous to lay the proof out in a numbered-lined stack:

1. ~(OBp → ~OB~p). (Assumption for reductio)
2. ~(□(dp) → ~□(d → ~p)) (1, Def of “OB”)
3. So □(dp) & □(d → ~p). (2, by PC)
4. So □(d → (p & ~p)). (3, derived rule of modal logic, K)
5. But ◊d (A3)
6. So ◊(p & ~p). (4 and 5, derived rule of modal logic, K)
7. But ~◊(p & ~p). (a theorem of modal logic, K)
8. So OBp → ~OB~p (1-7, PC)

Return to Deontic Logic.

Copyright © 2010 by
Paul McNamara <>

Open access to the SEP is made possible by a world-wide funding initiative.
Please Read How You Can Help Keep the Encyclopedia Free

The SEP would like to congratulate the National Endowment for the Humanities on its 50th anniversary and express our indebtedness for the five generous grants it awarded our project from 1997 to 2007. Readers who have benefited from the SEP are encouraged to examine the NEH’s anniversary page and, if inspired to do so, send a testimonial to