#### Supplement to Deontic Logic

## 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′. OB⊤( OB-N)R1. If ⊢ pand ⊢p→q, then ⊢q(MP) R2′. If ⊢ p↔q, thenOBp↔OBq( OB-RE)

We recall SDL for easy comparison:

SDL: A1. All tautologous wffs of the language (TAUT) A2. OB(p→q) → (OBp→OBq)( OB-K)A3. OBp→ ~OB~p( OB-D)MP. If ⊢ pand ⊢p→qthen ⊢q(MP) R2. If ⊢ pthen ⊢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 ⊢p→q, then ⊢OBp→OBq. (OB-RM)

Proof: Assume ⊢p→q. ByOB-NEC, ⊢OB(p→q), and then byOB-K, ⊢OBp→OBq.

Corollary: If ⊢p↔qthen ⊢OBp↔OBq(R2′ orOB-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: ⊢OB(p&q) → (OBp&OBq) (A2′ orOB-M)

Proof: By PC, ⊢ (p&q) →p. So byOB-RM ⊢OB(p&q) →OBp. In the same manner, we can derive ⊢OB(p&q) →OBq. From these two, by PC, we then getOB(p&q) → (OBp&OBq).

Show: ⊢ (OBp&OBq) →OB(p&q) (A3′ orOB-C)

Proof: By PC, ⊢p→ (q→ (p&q)). So byOB-RM ⊢OBp→OB(q→ (p&q)). But byOB-K, we have ⊢OB(q→ (p&q)) → (OBq→OB(p&q)). So from these two, by PC, ⊢OBp→ (OBq→OB(p&q)), which is equivalent by PC to ⊢ (OBp&OBq) →OB(p&q).

Show: ⊢ ~OB⊥ (A4′ orOB-OD)

Proof: (By reductio) AssumeOB⊥. Since by PC, ⊢ ⊥ ↔ (p& ~p), byOB-RE, we get ⊢OB⊥ ↔OB(p& ~p). So from this and our assumption, we getOB(p& ~p). GivenOB-M, this yieldsOBp&OB~p, and then from A3 of SDL, we getOBp& ~OB~p, a contradiction. So ⊢ ~OB⊥.

Show: ⊢OB⊤ (A5′ orOB-N)

Proof: By PC, ⊢ ⊤. So ByOB-NEC, we have ⊢OB⊤.

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 ⊢p→q, then ⊢OBp→OBq. (OB-RM)

Proof: Assume ⊢p→q. By PC, it follows that ⊢p↔ (p&q). So by R2′, ⊢OBp↔OB(p&q), and so by PC, ⊢OBp→OB(p&q). But by A2′, ⊢OB(p&q) → (OBp&OBq). So from the last two results, by PC, ⊢OBp→ (OBp&OBq), and thus ⊢OBp→OBq.Corollary:

Show: ⊢OB-RM is inter-derivable withOB-RE +OB-M.

This follows from the preceding proof and the first proof showing that SDL contains SDL′.OB(p→q) → (OBp→OBq) (A2 orOB-K)

Proof: By PC, ⊢ ((p→q) &p) →q. So byOB-RM, ⊢OB((p→q) &p) →OBq. But by A2′ conjoined with A3′, we get ⊢OB((p→q) &p) ↔ (OB(p→q) &OBp). So from the last two results, by PC, we get ⊢ (OB(p→q) &OBp) →OBq, and thus ⊢ (OB(p→q) → (OBp→OBq).^{[2]}

Show: ⊢OBp→ ~OB~p(A3 orOB-D)

Proof: (Reductio) Assume ~(OBp→ ~OB~p). By PC, (OBp&OB~p). So by A3′,OB(p& ~p), which is equivalent, by R2′ toOB⊥, which contradicts A4′.

Show: If ⊢pthen ⊢OBp(R2 orOB-NEC)

Proof: Assume ⊢p. From this by PC, it follows that ⊢p↔ ⊤. So by R2′, ⊢OBp↔OB⊤. But then from A5′, we get ⊢OBp. So if ⊢pthen ⊢OBp.

Return to Deontic Logic.