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 p and p → q, then q	(MP)
	R2′.	If p ↔ q, then OBp ↔ 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 p and p → q then q	(MP)
	R2.	If p then 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. By OB-NEC, OB (p → q), and then by OB-K, OBp → OBq.
Corollary: If p ↔ q then OBp ↔ OBq (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: OB(p & q) → (OBp & OBq) (A2′ or OB-M)
Proof: By PC, (p & q) → p. So by OB-RM OB(p & q) → OBp. In the same manner, we can derive OB(p & q) → OBq. From these two, by PC, we then get OB(p & q) → (OBp & OBq).

Show: (OBp & OBq) → OB(p & q) (A3′ or OB-C)
Proof: By PC, p → (q → (p & q)). So by OB-RM OBp → OB(q → (p & q)). But by OB-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′ or OB-OD)
Proof: (By reductio) Assume OB⊥. Since by PC, ⊥ ↔ (p & ~p), by OB-RE, we get 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 ~OB⊥.

Show: OB (A5′ or OB-N)
Proof: By PC, . So By OB-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: 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: OB(p → q) → (OBp → OBq) (A2 or OB-K)
Proof: By PC, ((p → q) & p) → q. So by OB-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 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 p then OBp (R2 or OB-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 p then OBp.

Return to Deontic Logic.