This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Stanford Encyclopedia of Philosophy
Supplement to Deontic Logic
Citation Information

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 proves p and proves pq then proves q (MP)
R2: If proves p then proves 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 proves rs, then provesr → □s), is derivable in Kd, and so we rely on it in the second proof.[1]

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

Show: proves OB(pq) → (OBpOBq). (K of SDL)
Proof: Assume OB(pq) and OBp. From PC alone, proves (d → (pq)) → [(dp) → (dq)]. So by RM for □, we have proves □(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 © 2006
Paul McNamara

Supplement to Deontic Logic
Stanford Encyclopedia of Philosophy