Axioms for modal logics based upon counterfactuals

Question

Suppose we have a logic for counterfactuals as with David Lewis. I here use ⇛ for the counterfactual conditional. So suppose we have:

Rules:

(1) If A and A→B are theorems, then B is a theorem.

(2) If (B₁∧...)→C is a theorem, then so is ((A⇛B₁)∧...)→(A⇛C)

Axioms:

(1) All truth functional tautologies

(2) A⇛A

(3) ((A⇛B)∧(B⇛A))→((A⇛C)↔(B⇛C))

(4) (((A∨B)⇛A)∨((A∨B)⇛B))∨(((A∨B)⇛C)↔((A⇛C)∧(B⇛C))

(5) (A⇛B)→(A→B)

(6) (A∧B)→(A⇛B)

Given Lewis's semantics so that α⇛β holds iff β holds in all closest possible worlds where α holds, we may define the modal operator for necessity

Definition

□α:=¬α⇛α.

Question

How do I most elegantly get modal logics in the hierarchy up to S5 on the basis of axiomatic principles for ⇛ while presupposing the Definition.

Initial example:

Given the Definition and the instance of axiom (5) that (¬α⇛α)→(¬α→α), we immediately get the T-axiom: □α→α.

Answer 1

Based on Joseph Jay Zeman's book Modal Logic: The Lewis-Modal Systems (see the Lemon-style bases in the Appendix), you can prove S5 from L3, RL, L2 and L6. Since you've proven L3 (T), and your Rule 2 implies RL (N), that leaves L2 (K), and L6 (5). Ordinarily, K and 5 are axioms, so it's not obvious that they are provable from the syntax of counterfactuals. I might use a semantic justification for an axiom for 5 or S5 semantics from which K should follow.

If the axiomatization is complete with respect to S5 necessity semantics, you can prove L6.

L6) ¬(A⇛¬A)→((A⇛¬A)⇛¬(A⇛¬A))

For additional information, see mathoverflow answer