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

Stanford Encyclopedia of Philosophy
Supplement to Deontic Logic
Citation Information


Alternative Axiomatization of SDL

The following alternative axiom system, which is provably equivalent to SDL, “breaks up” SDL into a larger number of “weaker parts” (SDL a la carte, as it were). This has the advantage of facilitating comparisons with other systems that reject one or more of SDL's theses.[1]

SDL′: A1. All tautologous wffs of the language (TAUT)
A2′. OB(p & q) → (OBp & OBq) (OB-M)
A3′. (OBp & OBq) → OB(p & q) (OB-C)
A4.′ ~OB (OB-OD)
A5′. OBtop (OB-N)
R1. If proves p and proves pq, then proves q (MP)
R2′. If proves pq, then OBpOBq (OB-RE)

We recall SDL for easy comparison:

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

Below is a proof that these two system are “equipollent”: any formula derivable in the one is derivable in the other.

I. First, we need to prove that each axiom (scheme) and rule of SDL can be derived in SDL. A1 and R1 are common to both systems, so we need only show that A2′-A5′ and R2′ are derivable.

Recall that OB-RM, and OB-RE (i.e. R2′) are derivable in SDL:

Show: If proves pq, then proves OBpOBq. (OB-RM)
Proof: Assume proves pq. By OB-NEC, proves OB (pq), and then by OB-K, proves OBpOBq.
Corollary: If proves pq then proves OBpOBq (R2′ or OB-RE)

So it remains to show A2′-A5’ are derivable in SDL, and to do so we make free use of our already derived rules, OB-RM and OB-RE.

Show: proves OB(p & q) → (OBp & OBq) (A2′ or OB-M)
Proof: By PC, proves (p & q) → p. So by OB-RM proves OB(p & q) → OBp. In the same manner, we can derive proves OB(p & q) → OBq. From these two, by PC, we then get OB(p & q) → (OBp & OBq).

Show: proves (OBp & OBq) → OB(p & q) (A3′ or OB-C)
Proof: By PC, proves p → (q → (p & q)). So by OB-RM proves OBpOB(q → (p & q)). But by OB-K, we have proves OB(q → (p & q)) → (OBqOB(p & q)). So from these two, by PC, proves OBp → (OBqOB(p & q)), which is equivalent by PC to proves (OBp & OBq) → OB(p & q).

Show: proves ~OB⊥ (A4′ or OB-OD)
Proof: (By reductio) Assume OB⊥. Since by PC, proves ⊥ ↔ (p & ~p), by OB-RE, we get proves OB⊥ ↔ OB(p & ~p). So from this and our assumption, we get OB(p & ~p). Given OB-M, this yields OBp & OB~p, and then from A3 of SDL, we get OBp & ~OB~p, a contradiction. So proves ~OB⊥.

Show: proves OBtop (A5′ or OB-N)
Proof: By PC, proves top. So By OB-NEC, we have proves OBtop.

II. It remains for us to show that each axiom (scheme) and rule of SDL can be derived in SDL′. Again, A1 and R1 are common to both systems, so we need only show that A2, A3 and R2 of SDL are in SDL′. It will be useful (but not necessary) to first show that OB-RM is derivable in SDL′, and then show the remaining items.

Show: If proves pq, then proves OBpOBq. (OB-RM)
Proof: Assume proves pq. By PC, it follows that proves p ↔ (p & q). So by R2′, proves OBpOB(p & q), and so by PC, proves OBpOB(p & q). But by A2′, proves OB(p & q) → (OBp & OBq). So from the last two results, by PC, proves OBp → (OBp & OBq), and thus proves OBpOBq.

Corollary: OB-RM is inter-derivable with OB-RE + OB-M.
This follows from the preceding proof and the first proof showing that SDL contains SDL′.

Show: proves OB(pq) → (OBpOBq) (A2 or OB-K)
Proof: By PC, proves ((pq) & p) → q. So by OB-RM, proves OB((pq) & p) → OBq. But by A2′ conjoined with A3′, we get proves OB((pq) & p) ↔ (OB(pq) & OBp). So from the last two results, by PC, we get proves (OB(pq) & OBp) → OBq, and thus proves (OB(pq) → (OBpOBq).[2]

Show: proves OBp → ~OB~p (A3 or OB-D)
Proof: (Reductio) Assume ~(OBp → ~OB~p). By PC, (OBp & OB~p). So by A3′, OB(p & ~p), which is equivalent, by R2′ to OB⊥, which contradicts A4′.

Show: If proves p then proves OBp (R2 or OB-NEC)
Proof: Assume proves p. From this by PC, it follows that proves ptop. So by R2′, proves OBpOBtop. But then from A5′, we get proves OBp. So if proves p then proves OBp.

Return to Deontic Logic.

Copyright © 2006
Paul McNamara
mcnamara.p@comcast.net

Supplement to Deontic Logic
Stanford Encyclopedia of Philosophy