# Axioms for modal logics based upon counterfactuals

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 (B1∧...)→C is a theorem, then so is ((A⇛B1)∧...)→(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: □α→α.

• Unfortunately, Philosophy SE doesn't render LaTeX. If you could translate that to unicode symbols it'd make for an easier read. Jun 21, 2018 at 11:40
• Why should it be possible to prove K syntactically? It seems like proving it would depend on S5 semantics. Jun 22, 2018 at 7:12
• @Schiphol Yes, unfortunately Philosophy SE does not offer the option to write in LaTex. Maybe I will translate this tomorrow. Nevertheless, those that know Latex may just copy my posting into a latex editor and so access a quite readable version. Jun 22, 2018 at 18:04
• @Greg S To prove a statement - as K - syntactically does not rely upon any particular semantics, but upon the axioms and rules of the system presupposed. Jun 22, 2018 at 18:06
• Those who want to scrutinise some of these matters may access a compiled text here: mathoverflow.net/questions/302877/… Jun 24, 2018 at 22:30