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.