Suppose we have a logic for counterfactuals as with David Lewis. I here use $\Rrightarrow$ for the counterfactual conditional. So suppose we have:
Rules:
(1) If $A$ and $A\rightarrow B$ are theorems, then $B$ is a theorem.
(2) If $(B_1\wedge ...)\rightarrow C$ is a theorem, then so is $((A\Rrightarrow B_1)\wedge ...)\rightarrow (A\Rrightarrow C)$
Axioms:
(1) All truth functional tautologies
(2) $A\Rrightarrow A$
(3) $((A\Rrightarrow B)\wedge(B\Rrightarrow A))\rightarrow ((A\Rrightarrow C)\leftrightarrow (B\Rrightarrow C))$
(4) $(((A\vee B)\Rrightarrow A)\vee ((A \vee B)\Rrightarrow B))\vee (((A\vee B)\Rrightarrow C)\leftrightarrow((A\Rrightarrow C)\wedge(B\Rrightarrow C))$
(5) $(A\Rrightarrow B)\rightarrow(A\rightarrow B)$
(6) $(A\wedge B)\rightarrow(A\Rrightarrow B)$
Given Lewis's semantics so that $\alpha\Rrightarrow\beta$ holds iff $\beta$ holds in all closest possible worlds where $\alpha$ holds, we may define the modal operator for necessity
$\mathbf{Definition}$
$\Box \alpha :=\lnot\alpha\Rrightarrow\alpha$.
$\mathbf{Question}$
How do I most elegantly get modal logics in the hierarchy up to $S5$ on the basis of axiomatic principles for $\Rrightarrow$ while presupposing the Definition.
$\mathbf{Initial \ example}$:
Given the Definition and the instance of axiom (5) that $(\lnot\alpha\Rrightarrow\alpha)\rightarrow(\lnot\alpha\rightarrow\alpha)$, we immediately get the $T$-$axiom$: $\Box\alpha\rightarrow\alpha$.
