Supplement to Deontic Logic

SDL Containment Proof

Recall SDL:

A1: All tautologous wffs of the language (TAUT)
A2: OB(pq) → (OBpOBq) (OB-K)
A3: OBp → ~OB~p (OB-NC)
R1: If ⊢ p and ⊢ pq then ⊢ q (MP)
R2: If ⊢ p then ⊢ OBp (OB-NEC)

We have already shown OB-NC is derivable in Kd above, and TAUT and MP are given, since they hold for all formulas of Kd. So we need only derive OB-K and OB-NEC of SDL, which we will do in reverse order. Note that RM, if ⊢ rs, then ⊢ □r → □s), is derivable in Kd, and so we rely on it in the second proof.[1]

Show: If ⊢ p then ⊢ OBp. (OB-NEC)
Proof: Assume ⊢ p. It follows by PC that ⊢ dp. So by NEC for □, we get ⊢ □(dp), that is, OBp.

Show: ⊢ OB(pq) → (OBpOBq). (K of SDL)
Proof: Assume OB(pq) and OBp. From PC alone, ⊢ (d → (pq)) → [(dp) → (dq)]. So by RM for □, we have ⊢ □(d → (pq)) → □[(dp) → (dq)]. But the antecedent of this is just, OB(pq) in disguise, which is our first assumption. So we have □[(dp) → (dq)] by MP. Applying K for □ to this, we get □(dp) → □(dq). But the antecedent to this is just our second assumption, OBp. So by MP, we get □(dq), that is, OBq.

Metatheorem: SDL is derivable in Kd.

Note that showing that the pure deontic fragment of Kd contains no more than SDL is a more complex matter. The proof relies on already having semantic metatheorems available. An excellent source for this is Åqvist 2002 [1984].[2]

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