Suppose we have a logic for counterfactuals as with David Lewis. I here use ⇛ for the counterfactual conditional. So suppose we have:
(1) If A and A→B are theorems, then B is a theorem.
(2) If (B1∧...)→C is a theorem, then so is ((A⇛B1)∧...)→(A⇛C)
(1) All truth functional tautologies
Given Lewis's semantics so that α⇛β holds iff β holds in all closest possible worlds where α holds, we may define the modal operator for necessity
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.
Given the Definition and the instance of axiom (5) that (¬α⇛α)→(¬α→α), we immediately get the T-axiom: □α→α.