# Axioms for modal logics based upon counterfactuals

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$.

In "Completeness and decidability...", Lewis shows the system C1 to be decidable and complete with respect to the semantics of corresponding canonical $\alpha$-models (81-4). It seems that K holds in all relevant filtrations of standard $\alpha$-models, so there should exist a syntactic proof of K. I don't see an obvious reason why a comparatively elegant syntactic proof, i.e. one that doesn't effectively enumerate all relevant cases, should be possible though.
In "Counterfactuals and Comparative Possibility", Lewis uses the equivalent system VC, and proposes axiom U ($\Box A \rightarrow \Box\Box A$ and $\Diamond A \rightarrow \Box\Diamond A$) corresponding to a frame condition of (local) uniformity (442-4). Assuming K is valid, C implies T (and N), and U corresponds to 4+5, so VCU entails S5. However, U is independent of VC, since it corresponds to dropping accessibility relations from VC canonical models (445).
So, even with a syntactic proof for K in C1, you can only prove systems K and T. It is very simple though to prove K, 5, etc. by including an axiom for S5 semantics, e.g. as used by Donald Nute, MOD: $(\lnot A \Rrightarrow A) \rightarrow (B \Rrightarrow A)$.